AutoSamplingTheory.TechnicalLemmas.Measure.GibbsIntegral

- Bochner integrals against a Gibbs `withDensity` measure rewrite to a base-measure integral weighted by the real Gibbs density. The only scalar hypothesis needed for this algebraic rewrite is `Z ≠ 0`, which keeps the `ℝ≥0∞` density `Z⁻¹ * exp(-V)` finite. Finiteness of the normalizing integral and probability-measure normalization are separate Gibbs leaves.

theorem integral_withDensity_inv_mul_gibbsDensityENNReal_eq_integral_inv_mul_exp_smul
    (μ : Measure α) {V : α → ℝ} (hV : AEMeasurable V μ)
    {Z : ℝ≥0∞} (hZ0 : Z ≠ 0) (g : α → F) :
    ∫ x, g x ∂μ.withDensity (fun x => Z⁻¹ * Measure.Gibbs.gibbsDensityENNReal V x) =
      ∫ x, (Z.toReal⁻¹ * Real.exp (-V x)) • g x ∂μ := by
  let f : α → ℝ≥0∞ := fun x => Z⁻¹ * Measure.Gibbs.gibbsDensityENNReal V x
  have hf_meas : AEMeasurable f μ := by
    exact AEMeasurable.const_mul
      (Measure.Gibbs.aemeasurable_gibbsDensityENNReal μ hV) Z⁻¹
  have hf_top : ∀ᵐ x ∂μ, f x < ∞ := by
    filter_upwards with x
    have hZpos : 0 < Z := bot_lt_iff_ne_bot.mpr hZ0
    have hZinv_lt_top : Z⁻¹ < ∞ := ENNReal.inv_lt_top.mpr hZpos
    have hg_lt_top : Measure.Gibbs.gibbsDensityENNReal V x < ∞ :=
      Measure.Gibbs.gibbsDensityENNReal_lt_top V x
    exact ENNReal.mul_lt_top hZinv_lt_top hg_lt_top
  rw [integral_withDensity_eq_integral_toReal_smul₀ hf_meas hf_top]
  apply integral_congr_ae
  filter_upwards with x
  simp [f, Measure.Gibbs.gibbsDensityENNReal, ENNReal.toReal_mul, ENNReal.toReal_inv,
    ENNReal.toReal_ofReal (Real.exp_nonneg _)]

/-- Source-facing specialization of the Gibbs integral rewrite where the scalar
is the Gibbs lintegral.  The finite-normalizer proof, when needed to obtain a
probability measure, remains a separate input to the probability-measure leaf. -/

AutoSamplingTheory/TechnicalLemmas/Measure/GibbsIntegral.lean:31published source at 7bcd37294df1Open detailed card

- Source-facing specialization of the Gibbs integral rewrite where the scalar is the Gibbs lintegral. The finite-normalizer proof, when needed to obtain a probability measure, remains a separate input to the probability-measure leaf.

theorem integral_withDensity_lintegral_inv_mul_gibbsDensityENNReal_eq_integral_lintegral_inv_mul_exp_smul
    (μ : Measure α) {V : α → ℝ} (hV : AEMeasurable V μ)
    (hZ0 : ∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂μ ≠ 0) (g : α → F) :
    ∫ x, g x ∂μ.withDensity
        (fun x =>
          (∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂μ)⁻¹ *
            Measure.Gibbs.gibbsDensityENNReal V x) =
      ∫ x,
        ((∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂μ).toReal⁻¹ *
          Real.exp (-V x)) • g x ∂μ :=
  integral_withDensity_inv_mul_gibbsDensityENNReal_eq_integral_inv_mul_exp_smul
    μ hV hZ0 g

/-- Nonzero-base-measure specialization of the source-facing Gibbs integral
rewrite.  It discharges the nonzero Gibbs normalizer from positivity of
`exp (-V)` and `[NeZero μ]`.

This remains only a Bochner-integral rewrite.  If a later theorem needs a
probability measure, it must also supply the finite-normalizer hypothesis to
the separate Gibbs probability leaf. -/

AutoSamplingTheory/TechnicalLemmas/Measure/GibbsIntegral.lean:56published source at 7bcd37294df1Open detailed card

- Nonzero-base-measure specialization of the source-facing Gibbs integral rewrite. It discharges the nonzero Gibbs normalizer from positivity of `exp (-V)` and `[NeZero μ]`. This remains only a Bochner-integral rewrite. If a later theorem needs a probability measure, it must also supply the finite-normalizer hypothesis to the separate Gibbs probability leaf.

theorem integral_withDensity_lintegral_inv_mul_gibbsDensityENNReal_eq_integral_lintegral_inv_mul_exp_smul_of_neZero
    (μ : Measure α) [NeZero μ] {V : α → ℝ} (hV : AEMeasurable V μ) (g : α → F) :
    ∫ x, g x ∂μ.withDensity
        (fun x =>
          (∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂μ)⁻¹ *
            Measure.Gibbs.gibbsDensityENNReal V x) =
      ∫ x,
        ((∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂μ).toReal⁻¹ *
          Real.exp (-V x)) • g x ∂μ :=
  integral_withDensity_lintegral_inv_mul_gibbsDensityENNReal_eq_integral_lintegral_inv_mul_exp_smul
    μ hV (Measure.Gibbs.lintegral_gibbsDensityENNReal_ne_zero μ hV) g

end GibbsIntegral
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/GibbsIntegral.lean:76published source at 7bcd37294df1Open detailed card