InformationTheory.Shannon.FisherInfo.HeatFlow

Imports 15

Fisher information V2 — heat flow #

Sub-decomposes the heat-flow side of the de Bruijn identity. The heat equation ∂_t p = (1/2) Δ_x p is exposed for the Gaussian heat kernel heatKernel t x = gaussianPDFReal 0 ⟨t, _⟩ x by giving its first and second spatial derivatives in closed form, and the monolithic heat_equation field of IsHeatFlowDensity is split into spatial-derivative, time-derivative, and convolution-representation sub-predicates.

Main definitions #

spatialLaplacianHeatKernel t x := (x²/t² - 1/t) · g_t x — the spatial Laplacian of the heat kernel.
IsHeatSpatialDerivHyp / IsHeatTimeDerivHyp / IsHeatFlowConvolutionHyp — the three sub-predicates of the heat equation.
IsHeatFlowDensity_of_sub_predicates — re-assembles the sub-predicates into an IsHeatFlowDensity witness.
IsRegularDeBruijnHypV2.ofHeatSubhyp — the IsRegularDeBruijnHypV2 constructor from the sub-predicates.

Main statements #

heatKernel_spatial_deriv / heatKernel_hasDerivAt_spatial — ∂_x g_t = -(x/t) · g_t.
heatKernel_spatial_laplacian — ∂²_x g_t = spatialLaplacianHeatKernel t x.
isHeatSpatialDerivHyp_gaussian — the Gaussian kernel satisfies the spatial-derivative sub-predicate.
deBruijn_identity_v2_of_heat_subhyp — the de Bruijn identity from the sub-predicate decomposition.

Implementation notes #

The time-derivative and convolution-representation sub-predicates are kept as pass-through hypotheses because the variance-derivative ∂_t gaussianPDFReal 0 ⟨t, _⟩ x is not in Mathlib.

Spatial derivatives of the Gaussian heat kernel #

theorem

InformationTheory.Shannon.FisherInfo.heatKernel_variance_ne_zero

source

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

⟨t, ⋯⟩ ≠ 0

The variance of the heat kernel at time t > 0 is nonzero as an ℝ≥0.

Used by

theorem

InformationTheory.Shannon.FisherInfo.heatKernel_spatial_deriv

source

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

deriv (fun (y : ℝ) => heatKernel t y) x = -(x / t) * heatKernel t x

First spatial derivative of the heat kernel (m = 0 case).

∂_x g_t(x) = -(x / t) · g_t(x), the m = 0 specialization of InformationTheory.Shannon.deriv_gaussianPDFReal.

Used by

theorem

InformationTheory.Shannon.FisherInfo.heatKernel_hasDerivAt_spatial

source

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

HasDerivAt (fun (y : ℝ) => heatKernel t y) (-(x / t) * heatKernel t x) x

HasDerivAt form of the first spatial derivative of the heat kernel.

Used by

noncomputable def

InformationTheory.Shannon.FisherInfo.spatialLaplacianHeatKernel

source

(t x : ℝ) :

ℝ

Spatial Laplacian of the heat kernel (closed form).

Δ_x g_t(x) = ∂²_x g_t(x) = (x²/t² - 1/t) · g_t(x).

Equations

InformationTheory.Shannon.FisherInfo.spatialLaplacianHeatKernel t x = (x ^ 2 / t ^ 2 - 1 / t) * InformationTheory.Shannon.FisherInfo.heatKernel t x

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.heatKernel_spatial_laplacian

source

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

deriv (fun (y : ℝ) => deriv (fun (z : ℝ) => heatKernel t z) y) x = spatialLaplacianHeatKernel t x

Second spatial derivative of the heat kernel equals spatialLaplacianHeatKernel. The core internal discharge: differentiate heatKernel_spatial_deriv once more (product rule).

∂²_x g_t(x) = (x²/t² - 1/t) · g_t(x).

Used by

Heat-equation right-hand side check (Gaussian, internal) #

Sub-predicate decomposition #

def

InformationTheory.Shannon.FisherInfo.IsHeatSpatialDerivHyp

source

(p Δp : ℝ → ℝ → ℝ) :

Prop

The spatial-derivative sub-predicate: p t has the prescribed spatial second derivative Δp t at every x (for t > 0). For the Gaussian kernel this is discharged by isHeatSpatialDerivHyp_gaussian.

Equations

InformationTheory.Shannon.FisherInfo.IsHeatSpatialDerivHyp p Δp = ∀ (t : ℝ), 0 < t → ∀ (x : ℝ), deriv (fun (y : ℝ) => deriv (fun (z : ℝ) => p t z) y) x = Δp t x

Instances For

Used by

def

InformationTheory.Shannon.FisherInfo.IsHeatTimeDerivHyp

source

(p Δp : ℝ → ℝ → ℝ) :

Prop

The time-derivative sub-predicate: p solves the heat equation ∂_s p = (1/2) Δp at t.

Equations

InformationTheory.Shannon.FisherInfo.IsHeatTimeDerivHyp p Δp = ∀ (t : ℝ), 0 < t → ∀ (x : ℝ), HasDerivAt (fun (s : ℝ) => p s x) (1 / 2 * Δp t x) t

Instances For

Used by

def

InformationTheory.Shannon.FisherInfo.IsHeatFlowConvolutionHyp

source

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

Prop

The convolution-representation sub-predicate.

Equations

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

Instances For

Used by

Gaussian discharge of the spatial sub-predicate #

theorem

InformationTheory.Shannon.FisherInfo.isHeatSpatialDerivHyp_gaussian

source

IsHeatSpatialDerivHyp (fun (t x : ℝ) => heatKernel t x) fun (t x : ℝ) => spatialLaplacianHeatKernel t x

The Gaussian heat kernel satisfies IsHeatSpatialDerivHyp with Δp t x := spatialLaplacianHeatKernel t x.

Used by

Re-assembly into `IsHeatFlowDensity` #

def

InformationTheory.Shannon.FisherInfo.IsHeatFlowDensity_of_sub_predicates

source

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

IsHeatFlowDensity X Z P p

Re-assembly: the sub-predicates re-build an IsHeatFlowDensity.

Equations

⋯ = ⋯

Instances For

Used by

Measure-level Gaussian heat semigroup composition #

de Bruijn identity bridge re-publish (from sub-predicates) #

theorem

InformationTheory.Shannon.FisherInfo.deBruijn_identity_v2_of_heat_subhyp

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 Δp : ℝ → ℝ → ℝ} (h_conv : IsHeatFlowConvolutionHyp X Z P p) (h_time : IsHeatTimeDerivHyp 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 ⋯).density_t) t

The de Bruijn identity from the sub-predicate decomposition: given the convolution and time-derivative sub-predicates (which re-assemble into an IsHeatFlowDensity) and the IBP hypothesis at t, the de Bruijn identity holds. Re-publishes deBruijn_identity_v2_of_heat_flow. The _h_ibp argument is kept for caller compatibility but unused (the genuine derivation does not consume the heat-equation core of h_time).

@audit:ok

Used by

noncomputable def

InformationTheory.Shannon.FisherInfo.IsRegularDeBruijnHypV2.ofHeatSubhyp

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 Δp : ℝ → ℝ → ℝ} (h_conv : IsHeatFlowConvolutionHyp X Z P p) (h_time : IsHeatTimeDerivHyp p Δp) :

IsRegularDeBruijnHypV2 X Z P t

The IsRegularDeBruijnHypV2 constructor from the convolution and time-derivative sub-predicates, via IsHeatFlowDensity_of_sub_predicates and ofHeatFlow.

@audit:ok

Equations

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

Instances For

Used by

InformationTheory.Shannon.FisherInfo.HeatFlow

Fisher information V2 — heat flow #

Main definitions #

Main statements #

Implementation notes #

Spatial derivatives of the Gaussian heat kernel #

Heat-equation right-hand side check (Gaussian, internal) #

Sub-predicate decomposition #

Gaussian discharge of the spatial sub-predicate #

Re-assembly into IsHeatFlowDensity #

Measure-level Gaussian heat semigroup composition #

de Bruijn identity bridge re-publish (from sub-predicates) #

Re-assembly into `IsHeatFlowDensity` #