InformationTheory

InformationTheory.Shannon.EPI.Conv.DensityAssoc

source

Imports 7

Convolution-density associativity + 4-fold interchange bridge (EPI A-5 precondition (3)) #

Closes the int_fisherZ retreat of EPI/Blachman/GeneralDensity.lean: the conv-of-conv convDensityAdd (convDensityAdd pX g_t) (convDensityAdd pY g_t) equals convDensityAdd (convDensityAdd pX pY) g_{2t} (variance-2t conv-with-Gaussian), which then closes Fisher integrability via convDensityAdd_fisher_integrand_integrable.

Route #

  1. convDensityAdd_assoc — conv(conv(a,b),c) = conv(a,conv(b,c)), via the bridge convDensityAdd = ⋆[mul ℝ ℝ, volume] (definitional, from the normalization file) and Mathlib MeasureTheory.convolution_assoc (all four bilinear maps = mul ℝ ℝ, compatibility (x*y)*z = x*(y*z) is mul_assoc). The ConvolutionExistsAt side conditions reduce to integrand integrability, supplied for nonneg integrable functions with a bounded (Gaussian-kernel) factor.
  2. convDensityAdd_convGaussian_interchange — assoc + convDensityAdd_comm rearrange (pX∗g)∗(pY∗g) = (pX∗pY)∗(g∗g), then variance-doubling g_t ∗ g_t = g_{2t} via convDensityAdd_gaussian_closed_form (mX=mY=0, vX=vY=⟨t,_⟩, sum ⟨2t,_⟩).

Regularity helpers (Part B consumer needs these for convDensityAdd pX pY) #

convDensityAdd_pXpY_nonneg / _measurable / _integrable / _integral_eq — the convDensityAdd (convDensityAdd pX pY) g_{2t} arm needs pX∗pY to be a normalized probability density (nonneg, measurable, integrable, mass 1).

@audit:ok (file-level, regularity helpers): convolutionExistsAt_of_integrable_bdd, convDensityAdd_pXpY_measurable, convDensityAdd_bdd_of_integrable_bdd, convDensityAdd_pXpY_nonneg, convDensityAdd_pXpY_integrable, convDensityAdd_pXpY_integral_eq are all constructive regularity lemmas (integrand integrability / measurability / global bound / nonneg / mass) with only regularity hypotheses; no circular / :True / bundled-core / degenerate shape.

theorem

InformationTheory.Shannon.EPIConvDensity.convDensityAdd_eq_convolution

source
(a b : ℝ → ℝ) :
convDensityAdd a b = fun (z : ℝ) => MeasureTheory.convolution a b (ContinuousLinearMap.mul ℝ ℝ) MeasureTheory.volume z

The convolution density convDensityAdd a b equals a ⋆[mul ℝ ℝ, volume] b (definitional, via ContinuousLinearMap.mul_apply'). @audit:ok

Used by
    theorem

    InformationTheory.Shannon.EPIConvDensity.convolutionExistsAt_of_integrable_bdd

    source
    (a b : ℝ → ℝ) (ha_int : MeasureTheory.Integrable a MeasureTheory.volume) (hb_meas : Measurable b) (hb_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |b x| ≤ M) (z : ℝ) :
    MeasureTheory.ConvolutionExistsAt a b z (ContinuousLinearMap.mul ℝ ℝ) MeasureTheory.volume

    ConvolutionExistsAt for two integrable functions, one of which is bounded.

    Used by
      theorem

      InformationTheory.Shannon.EPIConvDensity.convDensityAdd_pXpY_measurable

      source
      (pX pY : ℝ → ℝ) (hpX_meas : Measurable pX) (hpY_meas : Measurable pY) :
      Measurable (convDensityAdd pX pY)

      Measurability of convDensityAdd pX pY.

      Used by
        theorem

        InformationTheory.Shannon.EPIConvDensity.convDensityAdd_bdd_of_integrable_bdd

        source
        (a b : ℝ → ℝ) (ha_nn : ∀ (x : ℝ), 0 ≤ a x) (ha_int : MeasureTheory.Integrable a MeasureTheory.volume) (hb_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |b x| ≤ M) :
        ∃ (M : ℝ), ∀ (z : ℝ), |convDensityAdd a b z| ≤ M

        Global bound of convDensityAdd a b when one factor is bounded: |conv a b z| ≤ (∫|a|)·M. (Stated for a nonneg so ∫|a| = ∫a.)

        Used by
          theorem

          InformationTheory.Shannon.EPIConvDensity.convDensityAdd_assoc

          source
          (a b c : ℝ → ℝ) (ha_nn : ∀ (x : ℝ), 0 ≤ a x) (ha_int : MeasureTheory.Integrable a MeasureTheory.volume) (ha_meas : Measurable a) (hb_nn : ∀ (x : ℝ), 0 ≤ b x) (hb_int : MeasureTheory.Integrable b MeasureTheory.volume) (hb_meas : Measurable b) (hc_nn : ∀ (x : ℝ), 0 ≤ c x) (hc_int : MeasureTheory.Integrable c MeasureTheory.volume) (hc_meas : Measurable c) (hc_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |c x| ≤ M) :
          convDensityAdd (convDensityAdd a b) c = convDensityAdd a (convDensityAdd b c)

          The convolution density is associative: conv(conv(a,b),c) = conv(a,conv(b,c)). Via the bridge convDensityAdd = ⋆[mul ℝ ℝ, volume] and Mathlib convolution_assoc. Requires nonneg + integrable data; only the third factor c need be bounded (so that the ‖b‖ ⋆ ‖c‖-at-x₀ existence holds everywhere). The a ⋆ b and ‖b‖ ⋆ ‖c‖ existence are a.e. from Integrable.ae_convolution_exists (a, b may both be unbounded L¹). @audit:ok

          Used by
            theorem

            InformationTheory.Shannon.EPIConvDensity.convDensityAdd_pXpY_nonneg

            source
            (pX pY : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpY_nn : ∀ (x : ℝ), 0 ≤ pY x) (z : ℝ) :
            0 ≤ convDensityAdd pX pY z

            Nonnegativity of convDensityAdd pX pY (pointwise).

            Used by
              theorem

              InformationTheory.Shannon.EPIConvDensity.convDensityAdd_pXpY_integrable

              source
              (pX pY : ℝ → ℝ) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_meas : Measurable pX) (hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume) (hpY_meas : Measurable pY) :
              MeasureTheory.Integrable (convDensityAdd pX pY) MeasureTheory.volume

              Integrability of convDensityAdd pX pY when one factor is bounded.

              Used by
                theorem

                InformationTheory.Shannon.EPIConvDensity.convDensityAdd_pXpY_integral_eq

                source
                (pX pY : ℝ → ℝ) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume) :
                ∫ (z : ℝ), convDensityAdd pX pY z = (∫ (x : ℝ), pX x) * ∫ (x : ℝ), pY x

                ∫ convDensityAdd pX pY = (∫ pX)·(∫ pY); with both normalized, = 1.

                Used by
                  theorem

                  InformationTheory.Shannon.EPIConvDensity.convDensityAdd_gaussian_variance_double

                  source
                  {t : ℝ} (ht : 0 < t) :
                  convDensityAdd (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) = ProbabilityTheory.gaussianPDFReal 0 ⟨2 * t, ⋯⟩

                  Variance doubling: g_t ∗ g_t = g_{2t} (g_s = gaussianPDFReal 0 ⟨s, _⟩). @audit:ok

                  Used by
                    theorem

                    InformationTheory.Shannon.EPIConvDensity.convDensityAdd_gaussian_variance_add

                    source
                    {s t : ℝ} (hs : 0 < s) (ht : 0 < t) :
                    convDensityAdd (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩) (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) = ProbabilityTheory.gaussianPDFReal 0 ⟨s + t, ⋯⟩

                    Variance adding with asymmetric variances: g_s ∗ g_t = g_{s+t} (g_s = gaussianPDFReal 0 ⟨s, _⟩). Independent-time generalization of convDensityAdd_gaussian_variance_double (s = t); feeds the two-time route's harmonic-Stam supply producer (density_sum_{σ+τ} = conv(density_X_σ, density_Y_τ)).

                    Used by
                      theorem

                      InformationTheory.Shannon.EPIConvDensity.convDensityAdd_convGaussian_interchange

                      source
                      (pX pY : ℝ → ℝ) {t : ℝ} (ht : 0 < t) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpY_nn : ∀ (x : ℝ), 0 ≤ pY x) (hpY_meas : Measurable pY) (hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume) :
                      convDensityAdd (convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) (convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) = convDensityAdd (convDensityAdd pX pY) (ProbabilityTheory.gaussianPDFReal 0 ⟨2 * t, ⋯⟩)

                      The 4-fold interchange bridge (consumed by int_fisherZ): conv(conv(pX,g_t), conv(pY,g_t)) = conv(conv(pX,pY), g_{2t}). @audit:ok

                      Used by
                        theorem

                        InformationTheory.Shannon.EPIConvDensity.convDensityAdd_convGaussian_interchange_asym

                        source
                        (pX pY : ℝ → ℝ) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpY_nn : ∀ (x : ℝ), 0 ≤ pY x) (hpY_meas : Measurable pY) (hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume) :
                        convDensityAdd (convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩)) (convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) = convDensityAdd (convDensityAdd pX pY) (ProbabilityTheory.gaussianPDFReal 0 ⟨s + t, ⋯⟩)

                        The asymmetric 4-fold interchange bridge with independent times s, t: conv(conv(pX,g_s), conv(pY,g_t)) = conv(conv(pX,pY), g_{s+t}). Independent-time generalization of convDensityAdd_convGaussian_interchange (σ = τ); feeds the two-time route's harmonic-Stam supply producer for density_sum_{σ+τ} = conv(density_X_σ, density_Y_τ).

                        Used by