InformationTheory

InformationTheory.Shannon.AWGN.ConverseMIChainRule.PerLetterIntegrability

source

Imports 11

Converse-side per-letter log-density integrability #

Converse-side shared lemmas #

The converse-side analytic facts: per-letter log-density integrability, the memoryless MI chain rule, and the deterministic-encoder Markov factorization.

The old predicate bodies referenced awgnConverseJoint / perLetterYLaw / perLetterMI / jointMIXnYn, all defined in ConverseMutualInfoFiniteness.lean. Referencing those named defs from this file directly would create the import cycle ConverseMIChainRule → ConverseMutualInfoFiniteness → ConverseMIChainRule, so the body of awgnConverseJoint is inlined here as the private mirror def converseJointInline. The two defs share the same RHS, so they are definitionally equal: on the consumer side unfold awgnConverseJoint perLetterYLaw … reduces the goal to the inline form here, where the shared lemmas apply.

noncomputable def

InformationTheory.Shannon.AWGN.converseJointInline

source
{P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (c : AwgnCode M n P) :
MeasureTheory.Measure (Fin M × (Fin n → ℝ))

Mirror of the awgnConverseJoint body, inlined here to break the would-be import cycle. Defeq to awgnConverseJoint h_meas c (both defs share the same RHS, so consumer-side unfold awgnConverseJoint reduces to this form).

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

      InformationTheory.Shannon.AWGN.converseJointInline.instIsProbabilityMeasure

      source
      {P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} [NeZero M] (c : AwgnCode M n P) :
      MeasureTheory.IsProbabilityMeasure (converseJointInline h_meas c)

      converseJointInline is a probability measure for M ≥ 1 (mixture with weights 1/M summing to 1). Mirror of awgnConverseJoint.instIsProbabilityMeasure (ConverseMutualInfoFiniteness.lean:74); needed so IsMarkovChain's [IsFiniteMeasure μ] prerequisite resolves on the inlined joint.

      Used by

        Per-letter log-density integrability #

        The goal is a 1-dimensional integrability against volume on ℝ. The per-letter output law Y_i is a finite mixture of shifted 1-D Gaussians (1/M) ∑ₘ 𝒩(encoder m i, N), so its rnDeriv volume is the finite Gaussian-mixture density (1/M) ∑ₘ gaussianPDF (encoder m i) N. negMulLog of that density is dominated by a Gaussian moment integrand — pure 1-D measure-theoretic domination. The proof mirrors the continuous-input analogue outputDistribution_logDensity_integrable in CapacityConverseMaxent.lean (not importable here, due to the import cycle), but is simpler: the finite mixture needs no Chebyshev concentration (the lower bound comes from a single component).

        noncomputable def

        InformationTheory.Shannon.AWGN.perLetterMixtureDensity

        source
        {P : ℝ} (N : NNReal) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) (y : ℝ) :
        ENNReal

        The finite per-letter Gaussian-mixture density at coordinate i: (1/M) ∑ₘ gaussianPDF (encoder m i) N y (ℝ≥0∞-valued). For M ≥ 1 and N ≠ 0 this is the rnDeriv volume of the per-letter output law (converseJointInline h_meas c).map (·.2 i).

        Equations
        Instances For
          Used by
            theorem

            InformationTheory.Shannon.AWGN.perLetterMixtureDensity_measurable

            source
            {P : ℝ} (N : NNReal) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) :
            Measurable (perLetterMixtureDensity N c i)
            Used by
              theorem

              InformationTheory.Shannon.AWGN.perLetterLaw_withDensity

              source
              {P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) (hM : 0 < M) (hN : N ≠ 0) :
              MeasureTheory.Measure.map (fun (ω : Fin M × (Fin n → ℝ)) => ω.2 i) (converseJointInline h_meas c) = MeasureTheory.volume.withDensity (perLetterMixtureDensity N c i)

              For M ≥ 1 and N ≠ 0, the per-letter output law is volume.withDensity (perLetterMixtureDensity c i).

              Used by
                theorem

                InformationTheory.Shannon.AWGN.perLetterMixtureDensity_le_sup

                source
                {P : ℝ} (N : NNReal) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) (hM : 0 < M) (y : ℝ) :
                perLetterMixtureDensity N c i y ≤ ENNReal.ofReal (√(2 * Real.pi * ↑N))⁻¹

                The mixture density is bounded above by (√(2πN))⁻¹ (each component is, and the weights 1/M sum to ≤ 1).

                Used by
                  theorem

                  InformationTheory.Shannon.AWGN.perLetterMixtureDensity_log_abs_le

                  source
                  {P : ℝ} (N : NNReal) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) (hM : 0 < M) (hN : N ≠ 0) :
                  ∃ (c₀ : ℝ) (c₁ : ℝ), 0 ≤ c₁ ∧ ∀ (y : ℝ), |Real.log (perLetterMixtureDensity N c i y).toReal| ≤ c₀ + c₁ * y ^ 2

                  Lower bound on log of the mixture density (no Chebyshev needed — a single component suffices): there are c₀ c₁ with |log (f y).toReal| ≤ c₀ + c₁ y².

                  Used by
                    theorem

                    InformationTheory.Shannon.AWGN.perLetterLaw_sq_integrable

                    source
                    {P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) (hM : 0 < M) (hN : N ≠ 0) :
                    MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2) (MeasureTheory.Measure.map (fun (ω : Fin M × (Fin n → ℝ)) => ω.2 i) (converseJointInline h_meas c))

                    y² is integrable against the per-letter output law (finite mixture of Gaussians, each with finite second moment).

                    Used by
                      theorem

                      InformationTheory.Shannon.AWGN.awgnPerLetterIntegrability_holds

                      source
                      {P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) :
                      MeasureTheory.Integrable (fun (y : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Fin M × (Fin n → ℝ)) => ω.2 i) (converseJointInline h_meas c)).rnDeriv MeasureTheory.volume y).toReal.negMulLog) MeasureTheory.volume

                      Per-letter Y_i log-density integrability.

                      For every coordinate i, the per-letter output law Y_i (here the pushforward of the inlined joint along ω ↦ ω.2 i) has Lebesgue-integrable negMulLog (rnDeriv · vol). Consumer-side unfold perLetterYLaw awgnConverseJoint reduces perLetterYLaw h_meas c i to (converseJointInline h_meas c).map (fun ω => ω.2 i) (defeq).

                      The per-letter law is a finite Gaussian mixture; negMulLog of its rnDeriv is dominated by a Gaussian-moment integrand (perLetterMixtureDensity_log_abs_le + perLetterLaw_sq_integrable). The degenerate M = 0 / N = 0 cases give a singular law (rnDeriv = 0 a.e., negMulLog 0 = 0, constant, integrable), so the boundary is discharged by a genuine singular-law argument rather than a vacuity exploit. @audit:ok

                      Used by