InformationTheory

InformationTheory.Shannon.EPI.NoiseExtension

source

Imports 6

EPI lift-and-transport: 3-noise lift machinery #

The 3-noise lift space Ω × ℝ × ℝ × ℝ (three independent standard Gaussian factors) and the transport lemma that reduces a lift-space EPI conclusion to a base-space one.

Main definitions #

  • liftMeasure3: the product measure on Ω × ℝ × ℝ × ℝ.

Main statements #

3-noise lift (two-time route) #

The two-time assembler entropyPower_add_ge_case1_of_regular_twotime perturbs the sum with a SEPARATE single unit noise Z, independent of (Z_X, Z_Y). That requires a 3-noise lift Ω × ℝ × ℝ × ℝ (three independent standard normals), since reusing one of the 2-noise factors for Z would break Z ⊥ (Z_X, Z_Y). In the transport lemma below only the first factor (Prod.fst) carries X/Y, so all three entropyPower terms transport via measurePreserving_fst.

noncomputable abbrev

InformationTheory.Shannon.EPINoiseExtension.liftMeasure3

source
@[reducible, inline]
{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) :
MeasureTheory.Measure (Ω × ℝ × ℝ × ℝ)

Product measure on the 3-noise lift space Ω × ℝ × ℝ × ℝ (three standard Gaussian factors).

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

      InformationTheory.Shannon.EPINoiseExtension.entropyPower_map_comp_fst_eq3

      source
      {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (X : Ω → ℝ) (hX : Measurable X) :
      EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => X p.1) (liftMeasure3 P)) = EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map X P)
      Used by
        theorem

        InformationTheory.Shannon.EPINoiseExtension.entropy_power_inequality_via_lift3

        source
        {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hX : Measurable X) (hY : Measurable Y) (h_lift_epi : EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => X p.1 + Y p.1) (liftMeasure3 P)) ≥ EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => X p.1) (liftMeasure3 P)) + EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => Y p.1) (liftMeasure3 P))) :
        EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) ≥ EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map X P) + EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map Y P)

        Reduce a lift-space EPI conclusion to the base-space EPI via measure transport along Prod.fst.

        Used by