InformationTheory

InformationTheory.Shannon.MeasurePiTiltedFactorization

source

Imports 7

Finite Measure.pi tilt factorization #

This file builds the finite-product tilt factorization lemma, a building block for the IsMeasureInfinitePiTiltedEq reduction in InformationTheory/Shannon/Cramer/LC2PhaseC.lean.

The key result is pi_tilted_sum_eq_pi_tilted:

(Measure.pi (fun _ : Fin n => μ₀)).tilted (fun ω => ∑ i, lam * Y (ω i))
  = Measure.pi (fun _ : Fin n => μ₀.tilted (fun ω => lam * Y ω))

Main statements #

Implementation notes #

The factorization is built from Measure.pi_eq (a measure on a finite product equals the product measure if they agree on rectangles), reducing to a box-wise lintegral product factorization proved by Fin n induction mirroring MeasureTheory.integral_fin_nat_prod_eq_prod.

Lintegral product factorization over Measure.pi #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.lintegral_pi_prod

source
{n : ℕ} {E : Fin n → Type u_2} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → MeasureTheory.Measure (E i)} [∀ (i : Fin n), MeasureTheory.SigmaFinite (μ i)] {g : (i : Fin n) → E i → ENNReal} (hg : ∀ (i : Fin n), Measurable (g i)) :
∫⁻ (x : (i : Fin n) → E i), ∏ i : Fin n, g i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i : Fin n, ∫⁻ (ω : E i), g i ω ∂μ i

Unrestricted lintegral Fubini for Measure.pi of a per-coordinate product of nonnegative measurable functions, the lintegral analogue of MeasureTheory.integral_fin_nat_prod_eq_prod.

Used by
    theorem

    InformationTheory.Shannon.Cramer.TiltedLLN.setLIntegral_pi_prod_factor

    source
    {Ω₀ : Type u_1} [MeasurableSpace Ω₀] {n : ℕ} {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {g : Ω₀ → ENNReal} (hg : Measurable g) (s : Fin n → Set Ω₀) (hs : ∀ (i : Fin n), MeasurableSet (s i)) :
    (∫⁻ (x : Fin n → Ω₀) in Set.univ.pi s, ∏ i : Fin n, g (x i) ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ₀) = ∏ i : Fin n, ∫⁻ (ω : Ω₀) in s i, g ω ∂μ₀

    Box-restricted Tonelli: the lintegral over the box pi univ s of a per-coordinate product factors as the product of the per-coordinate box-restricted lintegrals.

    Used by

      Normalization constant Z^n #

      theorem

      InformationTheory.Shannon.Cramer.TiltedLLN.integral_exp_sum_pi_eq_pow

      source
      {Ω₀ : Type u_1} [MeasurableSpace Ω₀] {n : ℕ} {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (lam : ℝ) :
      (∫ (x : Fin n → Ω₀), Real.exp (∑ i : Fin n, lam * Y (x i)) ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ₀) = (∫ (ω : Ω₀), Real.exp (lam * Y ω) ∂μ₀) ^ n

      The partition function of the sum exponent on the finite product is the n-th power of the single-coordinate partition function.

      Used by

        The finite tilt factorization #

        theorem

        InformationTheory.Shannon.Cramer.TiltedLLN.pi_tilted_sum_eq_pi_tilted

        source
        {Ω₀ : Type u_1} [MeasurableSpace Ω₀] {n : ℕ} {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY : Measurable Y) (lam : ℝ) :
        ((MeasureTheory.Measure.pi fun (x : Fin n) => μ₀).tilted fun (ω : Fin n → Ω₀) => ∑ i : Fin n, lam * Y (ω i)) = MeasureTheory.Measure.pi fun (x : Fin n) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω

        The tilt of the finite product measure by the sum exponent factors as the product of the per-coordinate tilts.

        (Measure.pi (fun _ => μ₀)).tilted (∑ i, lam · Y (· i)) = Measure.pi (fun _ => μ₀.tilted (lam · Y)).

        Used by