InformationTheory

InformationTheory.Shannon.EPI.Case1.ProducerMeasurability

source

Imports 11

EPI Case-1 producer measurability bricks (Layer C closure, C-b route) #

This file supplies the t-parameter measurability needed by the integrable_deriv field of isDeBruijnRegularityHyp_of_methodX_unitnoise (EPI/Case1/RatioLimit/Producer.lean).

Route — C-b (closed-form score, no measurable_deriv_with_param) #

measurable_deriv_with_param requires global Continuous f.uncurry, which fails at t ≤ 0 (gaussianPDFReal 0 0 = 0 plus prefactor blow-up). We bypass it: the score logDeriv (convDensityAdd pX g_t) z = (∫ x, pX x · deriv g_t (z - x)) / (convDensityAdd pX g_t) z (convDensityAdd_logDeriv) is built from jointly measurable pieces — StronglyMeasurable.integral_prod_right for the numerator, Layer-A joint measurability for the denominator, then Measurable.div.

All hypotheses are pure regularity (Measurable pX etc.); no de Bruijn / Fisher core is threaded as a load-bearing hypothesis (CLAUDE.md "Verification honesty").

theorem

InformationTheory.Shannon.EPICase1ProducerMeasurability.measurable_gaussianPDFReal_var_uncurry

source
:
Measurable fun (p : ℝ × ℝ) => ProbabilityTheory.gaussianPDFReal 0 p.1.toNNReal p.2

The Gaussian pdf is jointly measurable in (variance, point). The in-tree port measurable_gaussianPDFReal_uncurry is on the mean axis; this is the variance axis (v = p.1.toNNReal). @audit:ok

Used by
    theorem

    InformationTheory.Shannon.EPICase1ProducerMeasurability.measurable_convDensityAdd_gaussian_uncurry

    source
    {pX : ℝ → ℝ} (hpX : Measurable pX) :
    Measurable fun (p : ℝ × ℝ) => EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 p.1.toNNReal) p.2

    The convolution density is jointly measurable in (t, z). @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.EPICase1ProducerMeasurability.deriv_gaussianPDFReal_zero_mean_all

      source
      (v : NNReal) (w : ℝ) :
      deriv (ProbabilityTheory.gaussianPDFReal 0 v) w = -w / ↑v * ProbabilityTheory.gaussianPDFReal 0 v w

      The Gaussian spatial-derivative closed form deriv (gaussianPDFReal 0 v) w = -(w)/v · gaussianPDFReal 0 v w, valid for all v (including v = 0, where both sides vanish: gaussianPDFReal 0 0 = 0 and -(w)/0 = 0). @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.EPICase1ProducerMeasurability.measurable_scoreNum_gaussian_uncurry

        source
        {pX : ℝ → ℝ} (hpX : Measurable pX) :
        Measurable fun (p : ℝ × ℝ) => ∫ (x : ℝ), pX x * deriv (ProbabilityTheory.gaussianPDFReal 0 p.1.toNNReal) (p.2 - x)

        The score-form numerator (t, z) ↦ ∫ x, pX x · deriv g_t (z - x) is jointly measurable. Uses the closed form deriv (gaussianPDFReal 0 v) w = -(w)/v · gaussianPDFReal 0 v w so the integrand is jointly measurable. @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.EPICase1ProducerMeasurability.deriv_convDensityAdd_gaussian_eq_scoreNum

          source
          {pX : ℝ → ℝ} (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (t z : ℝ) :
          deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 t.toNNReal)) z = ∫ (x : ℝ), pX x * deriv (ProbabilityTheory.gaussianPDFReal 0 t.toNNReal) (z - x)

          The key identity deriv (convDensityAdd pX g_t) z = ∫ x, pX x · deriv g_t (z - x) for all t, z (the differentiation-under-the-integral score form). For t > 0 this is convDensityAdd_hasDerivAt_of_integrable_smoothKernel.deriv; for t ≤ 0 both sides vanish (g_0 = 0 ⇒ conv = 0 ⇒ deriv = 0, and deriv g_0 = 0 ⇒ integrand 0).

          hpX_int is a pure regularity precondition (pX is an integrable density). @audit:ok

          Used by
            theorem

            InformationTheory.Shannon.EPICase1ProducerMeasurability.measurable_logDeriv_convDensityAdd_gaussian_uncurry

            source
            {pX : ℝ → ℝ} (hpX : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) :
            Measurable fun (p : ℝ × ℝ) => logDeriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 p.1.toNNReal)) p.2

            logDeriv (convDensityAdd pX g_t) is jointly measurable in (t, z). By logDeriv = deriv / conv and the C-b key identity deriv (conv_t) = scoreNum t, this is scoreNum / conv, both jointly measurable.

            hpX_int is a pure regularity precondition, not the de Bruijn core. @audit:ok

            Used by
              theorem

              InformationTheory.Shannon.EPICase1ProducerMeasurability.aestronglyMeasurable_fisherInfo_t

              source
              {pX : ℝ → ℝ} (hpX : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) :
              MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => 1 / 2 * (FisherInfo.fisherInfoOfDensity (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 t.toNNReal))).toReal) MeasureTheory.volume

              The t-side measurability the producer's integrable_deriv field needs, in the exact Measure.integrableOn_of_bounded shape (over volume).

              hpX_int is a pure regularity precondition (integrable probability density). @audit:ok

              Used by