InformationTheory.Shannon.EPI.Case1.TwoTime.Paths

Imports 20

EPI case-1 two-time object — matched-time path existence (§1) #

The inverse-function subproject: construct s(t) = N_A⁻¹(N_A(0)·eᵗ). Five private sub-lemmas (i)–(v) + matchedTimePath_exists. Lives in EPI/Case1/TwoTime.lean §1, building on TwoTime/Core.lean (§0). Umbrella: EPI/Case1/TwoTime.lean.

§1 — Matched-time path existence (inverse-function subproject) #

Construct s(t) = N_A⁻¹(N_A(0)·eᵗ) via strict monotonicity (J_A > 0), continuity on Ici 0, surjectivity (N_A → ∞), continuous inverse (StrictMonoOn.orderIso), and inverse-function derivative (HasDerivAt.of_local_left_inverse + comp). The hypotheses are only regularity preconditions; the conclusion (existence of a matched path) is the genuine output, not bundled.

The five pieces (i)-(v) are isolated as private sub-lemmas below.

theorem

InformationTheory.Shannon.EPICase1TwoTime.matchedTimePath_exists

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (A B : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (J_A : ℝ → ℝ) (_hA : Measurable A) (_hB : Measurable B) (_hAB : ProbabilityTheory.IndepFun A B P) (hJ_pos : ∀ (s : ℝ), 0 < s → 0 < J_A s) (hJ_deriv : ∀ (s : ℝ), 0 < s → HasDerivAt (fun (u : ℝ) => heatFlowEP A B P u) (heatFlowEP A B P s * J_A s) s) (h_endpt : IsHeatFlowEndpointRegular A B P) (hN_tendsto : Filter.Tendsto (fun (s : ℝ) => heatFlowEP A B P s) Filter.atTop Filter.atTop) :

∃ (s : ℝ → ℝ), IsMatchedTimePath A B P J_A s ∧ (∀ (t : ℝ), 0 < t → 0 < s t) ∧ Filter.Tendsto s Filter.atTop Filter.atTop

The matched-time path s : ℝ → ℝ exists.

Hypotheses are regularity preconditions only: positivity of the Fisher info J_A along the path (hJ_pos, a genuine 0 < fisherInfo precondition that has no in-tree theorem, threaded as in csiszarLogRatioGap_deriv_le_zero's hJX_pos), measurability, and independence. The conclusion is ∃ s, IsMatchedTimePath ... — the existence of the matched path with its e^t property and FII-matched derivative.

The inverse-function subproject is assembled from five private sub-lemmas:

(i) matchedTimePath_N_strictMonoOn — strict monotonicity from J_A > 0 (strictMonoOn_of_deriv_pos, derivative N_A(s)·J_A(s) > 0 via entropyPower_pos × hJ_pos);
(ii) matchedTimePath_N_continuousOn — continuity on Ici 0 (interior from the supplied derivative DifferentiableAt → ContinuousAt; endpoint s = 0⁺ from heatFlowEntropyPower_continuousWithinAt_zero via continuousWithinAt_Ioi_iff_Ici);
(iii)+(iv) matchedTimePath_inverse — surjectivity onto [N_A 0, ∞) (isPreconnected_Ici.intermediate_value_Ici, IVT) + continuous inverse g = Function.invFunOn N_A (Ici 0) (StrictMonoOn.continuousAt_of_image_mem_nhds / ...continuousWithinAt_right_of_surjOn);
(v) matchedTimePath_path_hasDerivAt — inverse-function chain rule glue (HasDerivAt.of_local_left_inverse giving g'(C·eᵗ) = (N·J)⁻¹, composed via HasDerivAt.comp with d/dt (C·eᵗ) = C·eᵗ, cancelling to 1/J_A).

The surjectivity precondition (hN_tendsto): the single-source heat-flow entropy power N_A(s) = entropyPower (P.map (A + √s·B)) diverges to ∞ as s → ∞. This is a genuine regularity datum (no in-tree theorem gives it for an arbitrary A), assembled from entropyPower_path_scaling (N_A(s) = s · entropyPower(P.map(A/√s + B))) times entropyPower_rescaled_path_tendsto (the rescaled path entropy power tends to the positive entropyPower (P.map B)). It is not load-bearing on the EPI conclusion: it is the order-completeness datum used to invert N_A (surjectivity onto [N_A 0, ∞)).

The endpoint precondition (h_endpt : IsHeatFlowEndpointRegular A B P): a regularity bundle (measurability / independence / Real density witness of P.map A / input entropy finiteness) consumed by the heat-flow endpoint continuity lemma; all fields are preconditions, none bundles the EPI conclusion. @audit:ok

Used by