InformationTheory

InformationTheory.Shannon.EPI.Case1.TwoTime.GapDerivative

source

Imports 21

EPI case-1 two-time object — gap object and its derivative (§2–§3) #

The two-time log-ratio gap object twoTimeLogRatioGap (formulation (b), e^t closed form), its value at the left endpoint twoTimeLogRatioGap_at_zero, the matched-sum law matchedSum_law_eq (the matched-sum perturbation reduces to a single-noise heat flow of X + Y), and the derivative twoTimeLogRatioGap_hasDerivAt / twoTimeLogRatioGap_deriv_le_zero. Verbatim split of EPI/Case1/TwoTime.lean §2–§3; proofs unchanged. Builds on TwoTime/Core.lean (§0) + TwoTime/Paths.lean (§1). Umbrella: EPI/Case1/TwoTime.lean.

§2 — Two-time log-ratio object (formulation (b), e^t closed form) #

R(t) = log N(s(t), r(t)) − log(N_X(0) + N_Y(0)) − t, where the sum entropy power N(s,r) = entropyPower (P.map (X + √(s)·Z_X + Y + √(r)·Z_Y)) is taken at the matched times s = s(t), r = r(t).

The third and second terms log(N_X(0)+N_Y(0)) and t are closed forms in t (constant minus t), so the only derivative content is d/dt log N(s(t),r(t)).

noncomputable def

InformationTheory.Shannon.EPICase1TwoTime.sumHeatFlowEP

source
{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) (s r : ℝ) :
ℝ

Sum entropy power of the independently-perturbed pair X + √s·Z_X and Y + √r·Z_Y.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Used by
      noncomputable def

      InformationTheory.Shannon.EPICase1TwoTime.twoTimeLogRatioGap

      source
      {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) (s r : ℝ → ℝ) (t : ℝ) :
      ℝ

      The two-time EPI log-ratio object twoTimeLogRatioGap (formulation (b), e^t closed form), parametrized by the matched paths s r : ℝ → ℝ.

      R(t) = log N(s(t),r(t)) − log(N_X(0) + N_Y(0)) − t.

      This is a plain def (no sorry): the paths s, r are inputs (constructed by matchedTimePath_exists), not load-bearing hypotheses. Mirrors the structure of csiszarLogRatioGap (EPI/L3Integration.lean) with the independent two-time perturbation and the e^t reparametrization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Used by
          theorem

          InformationTheory.Shannon.EPICase1TwoTime.twoTimeLogRatioGap_at_zero

          source
          {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) {J_X J_Y s r : ℝ → ℝ} (h_path_X : IsMatchedTimePath X Z_X P J_X s) (h_path_Y : IsMatchedTimePath Y Z_Y P J_Y r) :
          twoTimeLogRatioGap X Y Z_X Z_Y P s r 0 = Real.log (EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P)) - Real.log (EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map X P) + EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map Y P))

          At t = 0 the two-time gap reduces to the EPI bridge form log (eP(X+Y)) − log (eP X + eP Y).

          Uses s 0 = r 0 = 0 (IsMatchedTimePath.start_zero) so the perturbations vanish (√0 = 0), N(s 0, r 0) = eP(X+Y), and the −t term is 0. @audit:ok

          Used by

            §3 — Derivative of the two-time object #

            R'(t) = J_S·(1/J_X + 1/J_Y) − 1 along the matched path, where J_S = J(X_s + Y_r), via per-component de Bruijn (deBruijn_identity_v2) + chain rule (HasDerivAt.comp with s' = 1/J_X, r' = 1/J_Y).

            theorem

            InformationTheory.Shannon.EPICase1TwoTime.matchedSum_law_eq

            source
            {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hZX : Measurable Z_X) (hZY : Measurable Z_Y) (hZ : Measurable Z) (hZX_law : MeasureTheory.Measure.map Z_X P = ProbabilityTheory.gaussianReal 0 1) (hZY_law : MeasureTheory.Measure.map Z_Y P = ProbabilityTheory.gaussianReal 0 1) (hZ_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1) (hXY_ZXZY_pair : ProbabilityTheory.IndepFun (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => (Z_X ω, Z_Y ω)) P) (hXY_Z : ProbabilityTheory.IndepFun (fun (ω : Ω) => X ω + Y ω) Z P) (hZX_ZY : ProbabilityTheory.IndepFun Z_X Z_Y P) (s_t r_t : ℝ) (hst : 0 < s_t) (hrt : 0 < r_t) :
            MeasureTheory.Measure.map (fun (ω : Ω) => X ω + √s_t * Z_X ω + (Y ω + √r_t * Z_Y ω)) P = MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω + √(s_t + r_t) * Z ω) P

            The matched-sum law equals the single-noise heat flow of X+Y at τ = s_t + r_t.

            At a single time the matched-sum perturbation X + √(s_t)·Z_X + (Y + √(r_t)·Z_Y) rearranges to (X+Y) + (√(s_t)·Z_X + √(r_t)·Z_Y), and the noise √(s_t)·Z_X + √(r_t)·Z_Y — being a sum of independent centered Gaussians of variances s_t·v_X and r_t·v_Y — has law 𝒩(0, s_t·v_X + r_t·v_Y) independent of X+Y. Taking unit-variance noises (v_X = v_Y = 1) and τ = s_t + r_t, the matched-sum law equals the law of (X+Y) + √τ·Z for a unit Gaussian Z independent of X+Y. This is the single-noise heat flow of X+Y at time τ, which lets J_S be pinned by the existing single-noise IsDeBruijnRegularityHyp (X+Y) Z P.

            The hypotheses are regularity preconditions only (measurability, the unit-noise laws of Z_X, Z_Y, Z, and the relevant independences). The conclusion is a pure measure equality; no derivative value or EPI content is bundled. Body: Gaussian convolution additivity (gaussianReal add of the independent noise variances) + reassociation of the map.

            The precondition is joint independence of X+Y from the pair (Z_X, Z_Y) (hXY_ZXZY_pair) rather than from the unscaled sum Z_X+Z_Y: the matched-sum noise is the scaled combination √s_t·Z_X + √r_t·Z_Y (a different linear functional from Z_X+Z_Y when s_t ≠ r_t), and its independence from X+Y is recovered by IndepFun.comp with the measurable map (z₁, z₂) ↦ √s_t·z₁ + √r_t·z₂. This is a regularity precondition, not a bundling of the conclusion.

            Closed via gaussianReal_map_const_mul (scaled-noise law √c·W ∼ 𝒩(0,c)), gaussianReal_add_gaussianReal_of_indepFun (LHS noise additivity), and IndepFun.map_add_eq_map_conv_map (split both sides as (P.map (X+Y)) ∗ 𝒩(0, s_t+r_t)). #print axioms = sorryAx-free.

            Used by
              theorem

              InformationTheory.Shannon.EPICase1TwoTime.twoTimeLogRatioGap_hasDerivAt

              source
              {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {J_X J_Y s r : ℝ → ℝ} (hX : Measurable X) (hZX : Measurable Z_X) (_hXZX : ProbabilityTheory.IndepFun X Z_X P) (hY : Measurable Y) (hZY : Measurable Z_Y) (_hYZY : ProbabilityTheory.IndepFun Y Z_Y P) (h_path_X : IsMatchedTimePath X Z_X P J_X s) (h_path_Y : IsMatchedTimePath Y Z_Y P J_Y r) (h_reg_X : StamEPIBridge.IsDeBruijnRegularityHyp X Z_X P) (h_reg_Y : StamEPIBridge.IsDeBruijnRegularityHyp Y Z_Y P) (hZ : Measurable Z) (hZ_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1) (hXYZ : ProbabilityTheory.IndepFun (fun (ω : Ω) => X ω + Y ω) Z P) (hZX_law : MeasureTheory.Measure.map Z_X P = ProbabilityTheory.gaussianReal 0 1) (hZY_law : MeasureTheory.Measure.map Z_Y P = ProbabilityTheory.gaussianReal 0 1) (hXY_ZXZY_pair : ProbabilityTheory.IndepFun (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => (Z_X ω, Z_Y ω)) P) (hZX_ZY : ProbabilityTheory.IndepFun Z_X Z_Y P) (h_reg_sum : StamEPIBridge.IsDeBruijnRegularityHyp (fun (ω : Ω) => X ω + Y ω) Z P) {t : ℝ} (ht : 0 < t) (hst : 0 < s t) (hrt : 0 < r t) (hτ : 0 < s t + r t) (_hJX_eq : J_X (s t) = FisherInfo.fisherInfoOfDensityReal (h_reg_X.reg_at (s t) hst).density_t) (_hJY_eq : J_Y (r t) = FisherInfo.fisherInfoOfDensityReal (h_reg_Y.reg_at (r t) hrt).density_t) (_hJX_pos : 0 < J_X (s t)) (_hJY_pos : 0 < J_Y (r t)) :
              HasDerivAt (fun (u : ℝ) => twoTimeLogRatioGap X Y Z_X Z_Y P s r u) (FisherInfo.fisherInfoOfDensityReal (h_reg_sum.reg_at (s t + r t) hτ).density_t * (1 / J_X (s t) + 1 / J_Y (r t)) - 1) t

              The two-time gap has derivative J_S·(1/J_X + 1/J_Y) − 1 at t > 0 along the matched path.

              Reuses the per-component de Bruijn building blocks of csiszarLogRatioGap_hasDerivAt (EPI/Stam/ToBridge.lean, the entropyPower(X_s)·J_X form hN_X) composed via the chain rule with the matched velocities s'(t) = 1/J_X(s(t)), r'(t) = 1/J_Y(r(t)) (IsMatchedTimePath.deriv_at). The bivariate de Bruijn for the sum is deBruijn_identity_v2 applied at base X + Y_r, noise Z_X (and symmetrically), structurally identical to the existing sum version (no new asset).

              The de Bruijn regularity is IsDeBruijnRegularityHyp for each component; the J_* > 0 positivity is threaded as in csiszarLogRatioGap_deriv_le_zero.

              All three Fisher infos in the conclusion are pinned to a pointwise-smooth representative, so none is a free, skeptic-choosable variable:

              • J_X (s t) / J_Y (r t): density-pinned. hJX_eq/hJY_eq fix them to fisherInfoOfDensityReal ((h_reg_*.reg_at (s t) hst).density_t), and that density_t is pointwise pinned to the smooth representative via IsRegularDeBruijnHypV2.density_t_eq, with the real X/Y-density fixed by pX_law (same mechanism as the single-time csiszarLogRatioGap_hasDerivAt).
              • J_S: embedded directly, no free variable. At the single time t, the matched sum X_{s t} + Y_{r t} = (X+Y) + (√(s t)·Z_X + √(r t)·Z_Y), and the noise has law 𝒩(0, s t + r t) independent of X+Y, so the matched-sum law equals that of (X+Y) + √τ·Z (τ = s t + r t, Z unit Gaussian) — a single-noise heat flow of X+Y at time τ (proved by matchedSum_law_eq). Hence J_S is embedded directly into the conclusion as fisherInfoOfDensityReal ((h_reg_sum.reg_at (s t + r t) hτ).density_t) by threading the single-noise IsDeBruijnRegularityHyp (X+Y) Z P. Its density_t_eq supplies the smooth pointwise pin, so no free Fisher-info variable remains. @audit:ok
              Used by
                theorem

                InformationTheory.Shannon.EPICase1TwoTime.twoTimeLogRatioGap_deriv_le_zero

                source
                {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {J_X J_Y s r : ℝ → ℝ} (_h_path_X : IsMatchedTimePath X Z_X P J_X s) (_h_path_Y : IsMatchedTimePath Y Z_Y P J_Y r) {t : ℝ} (_ht : 0 < t) (J_S : ℝ) (_hJX_pos : 0 < J_X (s t)) (_hJY_pos : 0 < J_Y (r t)) (hJS_pos : 0 < J_S) (h_stam : 1 / J_S ≥ 1 / J_X (s t) + 1 / J_Y (r t)) :
                J_S * (1 / J_X (s t) + 1 / J_Y (r t)) - 1 ≤ 0

                The two-time gap derivative is ≤ 0 at t > 0 along the matched path (the analytic core).

                From harmonic Stam 1/J_S ≥ 1/J_X + 1/J_Y (J_S > 0), the value J_S·(1/J_X + 1/J_Y) − 1 ≤ 0. The harmonic Stam supply is the existing producer isStamInequalityHyp_of_indepFun / isStamInequalityHyp_via_body (sorryAx-free).

                Signature-honest: free J_S/J_X/J_Y are here OK because h_stam : 1/J_S ≥ 1/J_X(s t)+1/J_Y(r t) + hJS_pos constrain them — the conclusion is pure abstract arith (J_S·(1/J_X+1/J_Y) ≤ J_S·(1/J_S) = 1) that follows for any reals satisfying the hypotheses. Same shape as csiszar_ratio_deriv_le_zero_arith. @audit:ok

                Used by