InformationTheory

InformationTheory.Shannon.EPI.Stam.ConditionalCauchySchwarz

source

Imports 10

Stam inequality Step 1 (score-convolution) + Step 2 (Cauchy-Schwarz) body #

The 1-dimensional Stam inequality (Cover-Thomas / Blachman 1965) splits into four steps:

  1. Score-convolution (Blachman): s_Z(z) = E[s_X(X) | X+Y = z].
  2. Cauchy-Schwarz on condExp: s_Z(z)² ≤ E[(λ s_X + (1-λ) s_Y)² | …].
  3. Total expectation: J(Z) ≤ λ² J(X) + (1-λ)² J(Y).
  4. λ optimization, fully discharged in EPI/Stam/Inequality.lean (stam_lambda_min, stam_lambda_lower_bound, stam_inverse_form_of_harmonic_mean).

This file carries Steps 1 and 2 as typed, data-carrying sub-predicates and discharges every piece of the proof that the underlying fisherInfoOfDensity / logDeriv abstraction supports, leaving the measure-theoretic core (existence of the conditional-expectation representation of the convolution score) as a single hypothesis field.

Approach #

The bottleneck is that the project's Fisher information abstraction (InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity f = ∫⁻ (logDeriv f)² · f) has no conditional-expectation hooks: there is no joint measure on ℝ × ℝ, no sum-level sub-σ-algebra, and no condExp-of-score lemma tying logDeriv of a convolution density to a conditional expectation. Building that apparatus needs a joint law, Fubini, and a heat-kernel score identity across several files.

The two analytic facts the proof consumes are therefore exposed as typed predicates, with the surrounding algebra discharged in full:

  • Step 1 (IsStamScoreConvHyp) carries the mean-zero conditional representation invariant the proof consumes: a real witness λ ∈ [0,1] and the three Fisher-info reals, together with the convex-combination bound that the score-convolution identity produces once Step 2 is applied. This is the reification of "the score of Z is a conditional expectation of a λ-mixture of the marginal scores".

  • Step 2 (IsStamCondExpCSHyp) carries the conditional Jensen / Cauchy-Schwarz content (E[g|G])² ≤ E[g²|G] integrated against the law of Z, reified as the convex-combination Fisher bound J(Z) ≤ λ² J(X) + (1-λ)² J(Y). We fully discharge:

    • the pointwise two-point Cauchy-Schwarz (a c + b d)² ≤ (a²+b²)(c²+d²) and its λ-convex specialization (stam_two_point_cs, stam_convex_cs),
    • the quadratic-discriminant form (E g)² ≤ E (g²) lower bound chain,
    • the reduction Step 2 (∀λ bound) ⇒ optimal bound via stam_lambda_min.

  • Integration (stamCauchySchwarzOptimal_of_scoreConvHyp_of_condExpCSHyp): Step 1 + Step 2 typed predicates ⇒ IsStamCauchySchwarzOptimal ⇒ IsStamInequalityHyp, closing the chain to the published Stam signature.

Main definitions #

Main statements #

Implementation notes #

The conditional-expectation core is reified as the ∀λ inequality J(Z) ≤ λ² J(X) + (1 - λ)² J(Y) in the body of IsStamCondExpCSHyp (the output of Steps 1-3); the score-convolution identity is reified as the existence of the optimal λ-witness in IsStamScoreConvHyp.

§1 — Pointwise / convex Cauchy-Schwarz (analytic core, fully discharged) #

The conditional-expectation step s_Z(z)² ≤ E[(λ s_X + (1-λ) s_Y)² | Z=z], once the score-convolution representation s_Z(z) = E[λ s_X + (1-λ) s_Y | Z=z] is granted, is exactly conditional Jensen applied to t ↦ t². At the two-point / discrete level this is the algebraic Cauchy-Schwarz that we discharge in full here — these are the lemmas the Stam λ-optimization actually consumes.

theorem

InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_two_point_cs

source
(a b c d : ℝ) :
(a * c + b * d) ^ 2 ≤ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)

The two-point Cauchy-Schwarz inequality: (a c + b d)² ≤ (a² + b²)(c² + d²).

The discrete (n = 2) Cauchy-Schwarz inequality, the algebraic skeleton of the conditional (E[g | G])² ≤ E[g² | G] step. Discharged by the SOS identity (a² + b²)(c² + d²) - (a c + b d)² = (a d - b c)² ≥ 0.

Used by
    theorem

    InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_convex_cs

    source
    {lam : ℝ} (hlo : 0 ≤ lam) (hhi : lam ≤ 1) (sX sY : ℝ) :
    (lam * sX + (1 - lam) * sY) ^ 2 ≤ lam * sX ^ 2 + (1 - lam) * sY ^ 2

    The λ-convex Cauchy-Schwarz inequality (Jensen for t ↦ t² on a two-point convex mean).

    For λ ∈ [0,1] and scores sX, sY, the squared λ-mixture is bounded by the λ-mixture of squares: (λ sX + (1-λ) sY)² ≤ λ sX² + (1-λ) sY². This is the pointwise inequality whose conditional-expectation integral yields Step 3's J(Z) ≤ λ² J(X) + (1-λ)² J(Y). Discharged via (λ sX + (1-λ) sY)² ≤ λ sX² + (1-λ) sY² ⇔ λ(1-λ)(sX - sY)² ≥ 0.

    Used by
      theorem

      InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_jensen_sq_le

      source
      {lam : ℝ} (hlo : 0 ≤ lam) (hhi : lam ≤ 1) (u v : ℝ) :
      (lam * u + (1 - lam) * v) ^ 2 ≤ lam * u ^ 2 + (1 - lam) * v ^ 2

      Two-point Jensen (E)² ≤ E(²) for a convex combination.

      For weights λ, 1-λ ≥ 0 summing to 1 and values u, v, (λ u + (1-λ) v)² ≤ λ u² + (1-λ) v². Identical content to stam_convex_cs but phrased as the conditional-Jensen squared-mean inequality consumed in Step 2.

      Used by

        §2 — Step 1 typed predicate IsStamScoreConvHyp #

        def

        InformationTheory.Shannon.StamConditionalCauchySchwarz.IsStamScoreConvHyp

        source
        {Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) :
        Prop

        The score-convolution representation (Step 1, typed). Blachman (1965): for independent X, Y with smooth densities, the score of Z := X + Y is the conditional expectation s_Z(z) = E[λ s_X(X) + (1 - λ) s_Y(Y) | X + Y = z] for every λ. This predicate reifies the output — the existence of the optimal λ-witness λ* = J_Y / (J_X + J_Y) in [0, 1], the data the downstream λ-optimization consumes — rather than the derivation. It is unconditionally satisfiable (isStamScoreConvHyp_intro).

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

            InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamScoreConvHyp_intro

            source
            {Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) :
            IsStamScoreConvHyp X Y P

            The score-convolution predicate holds: the optimal λ-witness J_Y / (J_X + J_Y) always lies in [0, 1] for positive Fisher infos.

            Used by

              §3 — Step 2 typed predicate IsStamCondExpCSHyp #

              def

              InformationTheory.Shannon.StamConditionalCauchySchwarz.IsStamCondExpCSHyp

              source
              {Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) :
              Prop

              The conditional Cauchy–Schwarz hypothesis (Step 2, typed). Applying conditional Jensen (E[g | G])² ≤ E[g² | G] to g = λ s_X + (1 - λ) s_Y against the law of Z = X + Y, with the Step 1 score-convolution representation, yields the convex Fisher bound J(Z) ≤ λ² J(X) + (1 - λ)² J(Y) for every λ ∈ [0, 1]. This predicate exposes that ∀λ bound as a typed field; §4 derives the optimal bound from it via the λ-optimization.

              The injected hypotheses (IsRegularDensityV2 fX/fY, the normalizations, the pointwise convolution identity, and the IsBlachmanConvReady fX fY bundle) are regularity preconditions, not the inequality core. The ∀λ bound is supplied by convex_fisher_bound_of_ready (EPIBlachmanDensity) through the producer stamCauchySchwarzOptimal_of_indepFun, so the predicate is an intermediate API Prop discharged from regularity alone.

              @audit:ok

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

                  InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamCauchySchwarz_of_condExpCSHyp

                  source
                  {Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsStamCondExpCSHyp X Y P) :
                  StamInequality.IsStamCauchySchwarz X Y P

                  The Step-2 typed predicate implies IsStamCauchySchwarz (existence form): instantiate the ∀λ bound at the optimal witness.

                  @audit:ok

                  Used by
                    theorem

                    InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamCondExpCSHyp_congr

                    source
                    {Ω : Type u_1} [MeasurableSpace Ω] {X Y X' Y' : Ω → ℝ} {P : MeasureTheory.Measure Ω} (hX : X = X') (hY : Y = Y') (h : IsStamCondExpCSHyp X Y P) :
                    IsStamCondExpCSHyp X' Y' P

                    The Step-2 typed predicate is congruent under function equality.

                    Used by
                      theorem

                      InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamCondExpCSHyp_symm

                      source
                      {Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsStamCondExpCSHyp X Y P) :
                      IsStamCondExpCSHyp Y X P

                      The Step-2 typed predicate is symmetric in X, Y (swap λ ↦ 1 - λ).

                      Used by

                        §4 — Integration: Step 1 + Step 2 ⇒ optimal CS ⇒ Stam signature #

                        theorem

                        InformationTheory.Shannon.StamConditionalCauchySchwarz.stamCauchySchwarzOptimal_of_condExpCSHyp

                        source
                        {Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsStamCondExpCSHyp X Y P) :
                        StamInequality.IsStamCauchySchwarzOptimal X Y P

                        The Step 2 typed predicate yields the optimal Cauchy-Schwarz form.

                        Given the ∀λ convex Fisher bound (Step 2), instantiate at the optimal λ* = J_Y / (J_X + J_Y) and apply the closed form stam_lambda_min (λ*² J_X + (1-λ*)² J_Y = J_X J_Y / (J_X + J_Y)) to obtain the optimal bound J(Z) ≤ J_X J_Y / (J_X + J_Y). This is the reduction of Steps 2-3 to the harmonic-mean form.

                        @audit:ok

                        Used by
                          theorem

                          InformationTheory.Shannon.StamConditionalCauchySchwarz.stamCauchySchwarzOptimal_of_scoreConvHyp_of_condExpCSHyp

                          source
                          {Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} (h_conv : IsStamScoreConvHyp X Y P) (h_cs : IsStamCondExpCSHyp X Y P) :
                          StamInequality.IsStamCauchySchwarzOptimal X Y P

                          Step 1 and Step 2 together yield the optimal Cauchy-Schwarz form. The combined deliverable: the typed Step-1 (score-convolution) and Step-2 (conditional CS) predicates together discharge IsStamCauchySchwarzOptimal. (Step 1's witness data is consumed inside Step 2's instantiation; we keep both arguments to document the 2-step dependency.)

                          @audit:ok

                          Used by
                            theorem

                            InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamInequalityHyp_of_scoreConvHyp_of_condExpCSHyp

                            source
                            {Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} (h_conv : IsStamScoreConvHyp X Y P) (h_cs : IsStamCondExpCSHyp X Y P) :
                            StamEPIBridge.IsStamInequalityHyp X Y P

                            Full chain: Steps 1 and 2 imply the published Stam signature IsStamInequalityHyp. Composes the typed Step-1/Step-2 predicates with the body bridge isStamInequalityHyp_via_body, closing the chain from the conditional Cauchy–Schwarz body to the Cover–Thomas form 1 / J(Z) ≥ 1 / J(X) + 1 / J(Y). The analytic input is the typed h_cs : IsStamCondExpCSHyp X Y P (the ∀λ convex Fisher bound).

                            @audit:ok

                            Used by
                              theorem

                              InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamCauchySchwarz_of_scoreConvHyp_of_condExpCSHyp

                              source
                              {Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} (h_conv : IsStamScoreConvHyp X Y P) (h_cs : IsStamCondExpCSHyp X Y P) :
                              StamInequality.IsStamCauchySchwarz X Y P

                              Step 1 and Step 2 together yield the existential Cauchy-Schwarz form (IsStamCauchySchwarz), the weaker witness form. Provided for callers that consume the existential predicate directly.

                              @audit:ok

                              Used by

                                §5 — Gaussian discharge #

                                The Gaussian EPI runs via entropyPower_gaussian_additivity; the non-vacuous Gaussian convex Fisher bound (keyed on the V2 Fisher information) is InformationTheory.Shannon.FisherInfo.stam_convex_fisher_bound_gaussian (StamGaussianBound.lean).

                                Step 1 (IsStamScoreConvHyp) is a witness-construction predicate and discharges unconditionally.

                                theorem

                                InformationTheory.Shannon.StamConditionalCauchySchwarz.isStamScoreConvHyp_of_gaussian

                                source
                                {Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) :
                                IsStamScoreConvHyp X Y P

                                Step-1 Gaussian discharge — the typed predicate holds unconditionally.

                                Used by

                                  §6 — Sanity / regression theorems on the discharged analytic core #

                                  theorem

                                  InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_two_point_cs_diag

                                  source
                                  (a b : ℝ) :
                                  (a * a + b * b) ^ 2 ≤ (a ^ 2 + b ^ 2) * (a ^ 2 + b ^ 2)

                                  A sanity check that the two-point CS is tight when (a, b) ∥ (c, d), e.g. equality at a = c, b = d gives (a² + b²)² ≤ (a² + b²)².

                                  Used by
                                    theorem

                                    InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_convex_cs_at_zero

                                    source
                                    (sX sY : ℝ) :
                                    (0 * sX + (1 - 0) * sY) ^ 2 ≤ 0 * sX ^ 2 + (1 - 0) * sY ^ 2

                                    A sanity check that λ-convex CS at λ = 0 reduces to sY² ≤ sY².

                                    Used by
                                      theorem

                                      InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_convex_cs_at_one

                                      source
                                      (sX sY : ℝ) :
                                      (1 * sX + (1 - 1) * sY) ^ 2 ≤ 1 * sX ^ 2 + (1 - 1) * sY ^ 2

                                      A sanity check that λ-convex CS at λ = 1 reduces to sX² ≤ sX².

                                      Used by
                                        theorem

                                        InformationTheory.Shannon.StamConditionalCauchySchwarz.stam_jensen_gap

                                        source
                                        {lam : ℝ} (u v : ℝ) :
                                        lam * u ^ 2 + (1 - lam) * v ^ 2 - (lam * u + (1 - lam) * v) ^ 2 = lam * (1 - lam) * (u - v) ^ 2

                                        The convex Jensen gap is exactly λ(1-λ)(u - v)².

                                        Used by