InformationTheory.Shannon.FisherInfo.DeBruijnHeatFlow

Imports 15

Fisher information V2 — de Bruijn heat flow #

Heat-flow scaffolding for the general-X de Bruijn identity (Cover–Thomas's differentiate-under-the-integral via heat equation plus integration by parts), built on the definitions of FisherInfo/DeBruijn.lean. The heat equation and the integration-by-parts step are exposed as predicates that compose into the de Bruijn statement.

Main definitions #

heatKernel t x — the Gaussian heat kernel (1/√(2π t)) exp(-x²/(2t)), defined as gaussianPDFReal 0 ⟨t, _⟩ x for t > 0 and 0 otherwise.
IsHeatFlowDensity X Z P p — p is a density family for X + √t · Z satisfying the heat equation ∂_t p = (1/2) Δ_x p, bundled in statement form.
IsIBPHypothesis X Z P p t — the integration-by-parts conclusion at time t.
IsRegularDeBruijnHypV2.ofHeatFlow — the constructor turning an IsHeatFlowDensity witness (plus a.c. and finite-second-moment regularity of X) into an IsRegularDeBruijnHypV2.

Main statements #

heatKernel_nonneg / measurable_heatKernel — basic regularity of the heat kernel.
deBruijn_identity_v2_of_heat_flow — the de Bruijn identity from IsHeatFlowDensity plus IsIBPHypothesis.

Implementation notes #

The predicate split follows the Mathlib-shape rule: the heat-equation field matches the conclusion of the convolution chain rule, while the integration-by-parts field matches the conclusion expected by HasDerivAt.congr_of_eventuallyEq, so the two compose with deBruijn_identity_v2 without bridging lemmas.

Heat kernel (Gaussian density with variance `t`) #

noncomputable def

InformationTheory.Shannon.FisherInfo.heatKernel

source

(t x : ℝ) :

ℝ

Gaussian heat kernel g_t(x) := (1/√(2π t)) exp(-x²/(2t)).

Defined as the standard centred Gaussian density with variance t > 0. This is the kernel of the Gaussian heat semigroup: for Z ∼ 𝒩(0, 1) and X independent of Z, the density of X + √t · Z is p_0 * g_t (convolution).

For t = 0 we return 0 as a syntactic placeholder; the meaningful case is t > 0 (the kernel does not extend continuously to t = 0).

Equations

InformationTheory.Shannon.FisherInfo.heatKernel t x = if h : 0 < t then ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩ x else 0

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.heatKernel_def_gaussianPDFReal

source

{t : ℝ} (ht : 0 < t) (x : ℝ) :

heatKernel t x = ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩ x

Unfold lemma for heatKernel when t > 0.

Used by

theorem

InformationTheory.Shannon.FisherInfo.heatKernel_nonneg

source

(t x : ℝ) :

0 ≤ heatKernel t x

The heat kernel is non-negative.

Used by

theorem

InformationTheory.Shannon.FisherInfo.measurable_heatKernel

source

(t : ℝ) :

Measurable fun (x : ℝ) => heatKernel t x

The heat kernel is measurable.

Used by

Heat-flow density predicate #

structure

InformationTheory.Shannon.FisherInfo.IsHeatFlowDensity

source

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

Prop

The heat-flow density predicate for the law of X + √t · Z: p t x is the density of P.map (gaussianConvolution X Z t) at x, satisfying the heat equation ∂_t p = (1/2) Δ_x p together with basic regularity.

Z_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1
Z is standard normal.
density_witness(t : ℝ) : 0 < t → ∀ (x : ℝ), 0 ≤ p t x
For each t > 0, p t is a density witness for P.map (X + √t · Z).
density_measurable(t : ℝ) : 0 < t → Measurable (p t)
The density family is measurable in x for each t > 0.
heat_equation : ∃ (Δp : ℝ → ℝ → ℝ), ∀ (t : ℝ), 0 < t → ∀ (x : ℝ), HasDerivAt (fun (s : ℝ) => p s x) (1 / 2 * Δp t x) t
The heat equation in statement form: there is a Δp : ℝ → ℝ → ℝ with (d/dt) p t x = (1/2) · Δp t x for each t > 0 and x.

Instances For

Used by

noncomputable def

InformationTheory.Shannon.FisherInfo.IsHeatFlowDensity.laplacian

source

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

ℝ → ℝ → ℝ

Accessor: the spatial laplacian witness from heat_equation.

Equations

h.laplacian = ⋯.choose

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.IsHeatFlowDensity.heat_equation_spec

source

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

0 < t → ∀ (x : ℝ), HasDerivAt (fun (s : ℝ) => p s x) (1 / 2 * h.laplacian t x) t

The laplacian witness satisfies the heat equation ∂_t p = (1/2) · Δp.

Used by

Integration-by-parts predicate #

def

InformationTheory.Shannon.FisherInfo.IsIBPHypothesis

source

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

Prop

The integration-by-parts conclusion at time t: the time-derivative of differentialEntropy (P.map (X + √s · Z)) at s = t equals (1/2) · fisherInfoOfDensityReal (p t). This is a predicate-form literal alias of that HasDerivAt statement, retained for caller compatibility; it lifts a conclusion type into a predicate and is a deletion candidate.

@audit:retract-candidate(name-laundering-alias)

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

Heat-flow discharge #

noncomputable def

InformationTheory.Shannon.FisherInfo.IsRegularDeBruijnHypV2.ofHeatFlow

source

{Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X Z : Ω → ℝ} (hX : Measurable X) (_hZ : Measurable Z) (_hXZ : ProbabilityTheory.IndepFun X Z P) (hX_ac : (MeasureTheory.Measure.map X P).AbsolutelyContinuous MeasureTheory.volume) (h_mom_X : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) P) {t : ℝ} (_ht : 0 < t) {p : ℝ → ℝ → ℝ} (h_heat : IsHeatFlowDensity X Z P p) :

IsRegularDeBruijnHypV2 X Z P t

The IsRegularDeBruijnHypV2 constructor from a heat-flow density. The two extra preconditions are regularity of X itself, which IsHeatFlowDensity (carrying only the path density) does not supply:

hX_ac : (P.map X) ≪ volume — X has a Lebesgue density, feeding pX_law via withDensity_rnDeriv_eq.
h_mom_X : Integrable (fun ω => (X ω)^2) P — X has finite second moment, feeding pX_mom via integrable_map_measure.

The density witness density_t is pinned to the smooth convolution convDensityAdd pX g_t, the genuine density of P.map (X + √t · Z), so density_t_eq holds by rfl.

@audit:ok

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.deBruijn_identity_v2_of_heat_flow

source

{Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X Z : Ω → ℝ) (hX : Measurable X) (hZ : Measurable Z) (hXZ : ProbabilityTheory.IndepFun X Z P) (hX_ac : (MeasureTheory.Measure.map X P).AbsolutelyContinuous MeasureTheory.volume) (h_mom_X : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) P) {t : ℝ} (ht : 0 < t) {p : ℝ → ℝ → ℝ} (h_heat : IsHeatFlowDensity X Z P p) (_h_ibp : IsIBPHypothesis X Z P p t) :

HasDerivAt (fun (s : ℝ) => differentialEntropy (MeasureTheory.Measure.map (gaussianConvolution X Z s) P)) (1 / 2 * fisherInfoOfDensityReal (IsRegularDeBruijnHypV2.ofHeatFlow hX hZ hXZ hX_ac h_mom_X ht h_heat).density_t) t

The de Bruijn identity from a heat-flow density family p (IsHeatFlowDensity) and the IBP hypothesis at t > 0 (IsIBPHypothesis), with the V2 Fisher information of the constructed density witness on the right. A pass-through to deBruijn_identity_v2 via IsRegularDeBruijnHypV2.ofHeatFlow; the _h_ibp argument is kept for caller compatibility but unused.

@audit:ok

Used by

InformationTheory.Shannon.FisherInfo.DeBruijnHeatFlow

Fisher information V2 — de Bruijn heat flow #

Main definitions #

Main statements #

Implementation notes #

Heat kernel (Gaussian density with variance t) #

Heat-flow density predicate #

Integration-by-parts predicate #

Heat-flow discharge #

Heat kernel (Gaussian density with variance `t`) #