InformationTheory

InformationTheory.Shannon.EPI.G2.HeatFlowContinuity

source

Imports 23

Heat-flow entropy-power continuity at the endpoint t = 0⁺ #

This file isolates the single analytic atom used by the EPI continuity consumer in EPI/Stam/ToBridge.lean: the continuity of t ↦ entropyPower (P.map (fun ω ↦ X ω + √t · Z ω)) at the endpoint t = 0⁺ along the heat-flow ray. The interior t > 0 continuity is supplied separately by csiszarLogRatioGap_differentiableOn_interior.

The endpoint atom is heatFlowEntropyPower_continuousWithinAt_zero, claiming only ContinuousWithinAt (Set.Ioi 0) 0 (the single endpoint limit t → 0⁺). The endpoint is re-attached to the interior with the OrderDual mirror AntitoneOn.insert_of_continuousWithinAt (added in this file).

Main statements #

Entropy finiteness of the limit density (a precondition) #

Integrable (negMulLog pX) (= h(X) < ∞, differential entropy of the limit density pX finite) is required as the limit-side Integrable input by the entropy-integral machinery. It does not follow from the L¹ + finite-second-moment regularity of pX (a concentrated density can have ∫ negMulLog pX = −∞). It is therefore carried as an explicit hpX_ent precondition: the input X has finite differential entropy. This is a regularity precondition on the input distribution, not a load-bearing conclusion.

theorem

InformationTheory.Shannon.convDensityAdd_negMulLog_integrable_pub

source
{pX : ℝ → ℝ} (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) (hpX_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * pX y) MeasureTheory.volume) {t : ℝ} (ht : 0 < t) :
MeasureTheory.Integrable (fun (x : ℝ) => (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x).negMulLog) MeasureTheory.volume

Per-time entropy-integrand integrability. For each t > 0, negMulLog (convDensityAdd pX g_t) is volume-integrable.

Delegates verbatim to the in-tree asset FisherInfo.convDensityAdd_negMulLog_integrable (same conclusion type); pure plumbing, no new analytic content. @audit:ok

Used by

    Two-sided sandwich for the entropy-integral limit #

    The lift from per-time entropy integrals to the endpoint entropy integral is a two-sided sandwich:

    • the (α) limsup upper bound — InformationTheory.EPIG2KLFatou.negMulLog_convDensity_limsup_le (Fatou / KL lower-semicontinuity): limsup (∫ negMulLog f_n) ≤ ∫ negMulLog pX.
    • the (β) per-n lower bound — negMulLog_convDensity_entropy_ge_density (conditioning reduces entropy): ∫ negMulLog pX ≤ ∫ negMulLog f_n.
    • the uniform upper bound — negMulLog_convDensityAdd_gaussian_entropy_upper (Gaussian maximum-entropy): a per-n bound with a uniform variance majorant (the v n are bounded since v n → 0), supplying the IsBoundedUnder (· ≤ ·) witness for the squeeze.

    The squeeze tendsto_of_le_liminf_of_limsup_le then gives ∫ negMulLog f_n → ∫ negMulLog pX along sequences, lifted to 𝓝[Ioi 0] 0 via Filter.tendsto_iff_seq_tendsto.

    theorem

    InformationTheory.Shannon.differentialEntropy_convDensity_integral_tendsto

    source
    {pX : ℝ → ℝ} (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) (hpX_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * pX y) MeasureTheory.volume) (hpX_ent : MeasureTheory.Integrable (fun (x : ℝ) => (pX x).negMulLog) MeasureTheory.volume) :
    Filter.Tendsto (fun (t : ℝ) => ∫ (x : ℝ), (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 t.toNNReal) x).negMulLog) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : ℝ), (pX x).negMulLog))

    Entropy-integral convergence. Given the regularity of pX and the entropy-finiteness precondition hpX_ent (= h(X) < ∞, a regularity precondition on the input), the differential-entropy integrals of the heat-smoothed densities converge to the entropy integral of pX as t → 0⁺:

    ∫ negMulLog (convDensityAdd pX g_t) ∂volume → ∫ negMulLog pX ∂volume. @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.heatFlowDifferentialEntropy_continuousWithinAt_zero

      source
      {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX_meas : Measurable X) (hZ_meas : Measurable Z) (hXZ_indep : ProbabilityTheory.IndepFun X Z P) (v_Z : NNReal) (hv_Z_pos : 0 < v_Z) (hZ_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 v_Z) (pX : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_law : MeasureTheory.Measure.map X P = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (pX x)) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) (hpX_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * pX y) MeasureTheory.volume) (hpX_ent : MeasureTheory.Integrable (fun (x : ℝ) => (pX x).negMulLog) MeasureTheory.volume) :
      ContinuousWithinAt (fun (t : ℝ) => differentialEntropy (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + √t * Z ω) P)) (Set.Ioi 0) 0

      Heat-flow differential-entropy endpoint continuity. With explicit regularity preconditions on X, Z (measurability, independence, Gaussian noise law P.map Z = 𝒩(0, v_Z)) and a Real density witness pX for P.map X, the inner differential entropy of the heat-flow path is ContinuousWithinAt (Set.Ioi 0) 0:

      t ↦ differentialEntropy (P.map (X + √t·Z)) is continuous at t = 0⁺.

      The density identification pPath_eq_convDensityAdd turns the pushforward density into convDensityAdd pX (gaussianPDFReal 0 ⟨t·v_Z,_⟩) for each t > 0, the differential entropy becomes ∫ negMulLog (convDensityAdd …), the entropy-integral convergence differentialEntropy_convDensity_integral_tendsto (reparameterised t' := t·v_Z) supplies the limit, and ContinuousWithinAt is recovered with the endpoint value differentialEntropy (P.map X) = ∫ negMulLog pX. All fields are preconditions (regularity / input-distribution data); no continuity conclusion is bundled. @audit:ok

      Used by
        theorem

        AntitoneOn.insert_of_continuousWithinAt

        source
        {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] {f : α → β} {s : Set α} {x : α} (hf : AntitoneOn f s) (hx : ClusterPt x (Filter.principal s)) (h'x : ContinuousWithinAt f s x) :
        AntitoneOn f (insert x s)

        AntitoneOn endpoint-insert, the OrderDual mirror of MonotoneOn.insert_of_continuousWithinAt. If f is AntitoneOn s and left-continuous-within-s at a cluster point x, then f is AntitoneOn the augmented set insert x s. Used to re-attach the endpoint t = 0 to the genuine interior AntitoneOn (Set.Ioi 0).

        Mathlib has the monotone version only; this is its dual via OrderDual.toDual (an order-reversing homeomorphism on β), which sends AntitoneOn f s to MonotoneOn (toDual ∘ f) s and preserves ContinuousWithinAt. @audit:ok

        Used by
          structure

          InformationTheory.Shannon.IsHeatFlowEndpointRegular

          source
          {Ω : Type u_1} [MeasurableSpace Ω] (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] :
          Type

          The heat-flow endpoint regularity bundle (a precondition consumed by the EPI continuity assembly in EPI/Stam/ToBridge.lean).

          Carries exactly the regularity / input-distribution data the density-identification bridge (pPath_eq_convDensityAdd) and the entropy-integral machinery (differentialEntropy_convDensity_integral_tendsto) require, at the endpoint t = 0⁺:

          • hX_meas / hZ_meas / hXZ_indep — measurability + independence of the de Bruijn pair X ⊥ Z (Cover–Thomas standing assumptions).
          • v_Z / hv_Z_pos / hZ_law — the Gaussian noise law P.map Z = 𝒩(0, v_Z) (general variance, so the sum instance Z_X+Z_Y ∼ 𝒩(0,2) fits).
          • pX / hpX_nn / hpX_meas / hpX_law — a Real density witness for P.map X.
          • hpX_int / hpX_mass / hpX_mom — pX is a probability density with finite second moment.
          • hpX_ent — negMulLog pX is volume-integrable, i.e. the input differential entropy h(X) is finite (a regularity precondition on the input distribution, not derivable from L¹ + second moment).

          Every field is a precondition (regularity / input-distribution data); none is a continuity / L¹-convergence / density-identification conclusion. This is not a load-bearing hypothesis bundle — the analytic content is discharged genuinely by heatFlowDifferentialEntropy_continuousWithinAt_zero, which only consumes these fields as inputs.

          Instances For
            Used by
              theorem

              InformationTheory.Shannon.heatFlowEntropyPower_continuousWithinAt_zero

              source
              {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (h_endpt : IsHeatFlowEndpointRegular X Z P) :
              ContinuousWithinAt (fun (t : ℝ) => EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + √t * Z ω) P)) (Set.Ioi 0) 0

              Heat-flow entropy-power endpoint continuity.

              t ↦ entropyPower (P.map (fun ω ↦ X ω + √t · Z ω)) is ContinuousWithinAt (Set.Ioi 0) 0 (the limit t → 0⁺). The consumer (csiszarLogRatioGap_continuousWithinAt_zero) reduces to three instances of this single endpoint term; the interior t > 0 continuity is supplied separately from csiszarLogRatioGap_differentiableOn_interior (.continuousOn).

              The endpoint is discharged via the inner differential-entropy continuity heatFlowDifferentialEntropy_continuousWithinAt_zero (density identification pPath_eq_convDensityAdd + reparameterised entropy-integral convergence differentialEntropy_convDensity_integral_tendsto), with entropyPower = exp ∘ (2·differentialEntropy) lifting it via Real.continuous_exp.

              The signature takes IsHeatFlowEndpointRegular X Z P, whose fields are all preconditions (regularity / input-distribution data); no continuity / density-identification conclusion is bundled. @audit:ok

              Used by