InformationTheory.Shannon.EPI.Case1.TwoTime.Core

Imports 19

EPI case-1 two-time object — Core (§0) #

Matched-time path abbreviations shared across the two-time object split (TwoTime/Paths.lean = §1 path existence, TwoTime/GapDerivative.lean + TwoTime/MonotonicityAndSaturation.lean + TwoTime/EntropyPowerInequality.lean = §2–§4). Verbatim split of EPI/Case1/TwoTime.lean §0; proofs unchanged. Umbrella: EPI/Case1/TwoTime.lean.

§0 — Matched-time path abbreviations #

The single-source heat-flow entropy power N_A(s) = entropyPower (P.map (A + √s·B)). The matched path s(t) is the inverse of N_A solving N_A(s(t)) = N_A(0)·eᵗ.

noncomputable def

InformationTheory.Shannon.EPICase1TwoTime.heatFlowEP

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (A B : Ω → ℝ) (P : MeasureTheory.Measure Ω) (s : ℝ) :

ℝ

Single-source heat-flow entropy power along the perturbation A + √s·B. N_A(0) = entropyPower (P.map A).

Equations

InformationTheory.Shannon.EPICase1TwoTime.heatFlowEP A B P s = InformationTheory.Shannon.EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => A ω + √s * B ω) P)

Instances For

Used by

structure

InformationTheory.Shannon.EPICase1TwoTime.IsMatchedTimePath

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (A B : Ω → ℝ) (P : MeasureTheory.Measure Ω) (J_A s : ℝ → ℝ) :

Prop

Matched-time path predicate (output of the inverse-function construction).

For a path s : ℝ → ℝ along the A-perturbation, this records that:

s starts at 0 (s 0 = 0);
the entropy power grows as eᵗ: N_A(s(t)) = N_A(0)·eᵗ for t ≥ 0 (the matched-time e^t characterization, proof-log §formulation gate);
s is continuous on [0, ∞);
on the interior t > 0, s has derivative 1/J_A(s(t)) (FII-matched velocity), where J_A is the Fisher info of the perturbed density.

This is not a load-bearing hypothesis on the EPI conclusion: it is the genuine output of matchedTimePath_exists (inverse-function subproject), whose inputs are only regularity preconditions (J_A > 0, measurability, indep).

start_zero : s 0 = 0
The path starts at time 0.
matched_growth(t : ℝ) : 0 ≤ t → heatFlowEP A B P (s t) = heatFlowEP A B P 0 * Real.exp t
Matched e^t growth of the single-source entropy power.
cont : ContinuousOn s (Set.Ici 0)
The path is continuous on [0, ∞).
deriv_at(t : ℝ) : 0 < t → HasDerivAt s (1 / J_A (s t)) t
FII-matched velocity on the interior.

Instances For

Used by