6.1 · Book p. 174 · PDF p. 186
Analysis of LMC via Interpolation Argument
Controls Rényi divergence along an interpolation of LMC, combining differential identities, functional inequalities, and local drift error.
Open this section in the canonical August 9 source ↗Section 6.1
Rényi divergence packages a power integral of a density ratio.
At order q, Rényi divergence is the logarithm of a q-th power integral of the density ratio, scaled by 1/(q-1). The power weight changes both the dissipation term and the error estimates used in the LMC analysis.
Why is this valid?
Absolute continuity and the extended-value behavior of the density ratio cannot be suppressed.
Source assumptions
- density ratio
- order parameter
Formal assumptions
- measurable nonnegative densities
- explicit domination for finiteness
View Lean formalization
ASTIS first establishes positivity, measurability, finite lintegral transfer, and calculus for the scalar integrand.
AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.renyiIntegrand_pos
theorem renyiIntegrand_pos {a p q : ℝ}
(hp : 0 < p) (hq : 0 < q) :
0 < renyiIntegrand a p q := by
exact mul_pos (Real.rpow_pos_of_pos hp a) (Real.rpow_pos_of_pos hq (1 - a))
variable [MeasurableSpace α]
/-- A measurable pair of real densities gives a measurable Renyi integrand for
orders `a ∈ [0,1]`. -/Imports
- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.measurable_renyiIntegrandENNReal
theorem measurable_renyiIntegrandENNReal {a : ℝ} {p q : α → ℝ}
(ha0 : 0 ≤ a) (ha1 : a ≤ 1)
(hp : Measurable p) (hq : Measurable q) :
Measurable (renyiIntegrandENNReal a p q) := by
change Measurable (fun x => ENNReal.ofReal (renyiIntegrand a (p x) (q x)))
exact (measurable_renyiIntegrand (α := α) ha0 ha1 hp hq).ennreal_ofReal
/-- A finite envelope gives a finite Renyi lintegral. -/Imports
- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.lintegral_renyiIntegrandENNReal_ne_top_of_ae_le
theorem lintegral_renyiIntegrandENNReal_ne_top_of_ae_le
(μ : MeasureTheory.Measure α) (a : ℝ) (p q : α → ℝ) (g : α → ℝ≥0∞)
(hle : ∀ᵐ x ∂μ, renyiIntegrandENNReal a p q x ≤ g x)
(hgfin : ∫⁻ x, g x ∂μ ≠ ∞) :
∫⁻ x, renyiIntegrandENNReal a p q x ∂μ ≠ ∞ :=
ne_top_of_le_ne_top hgfin (lintegral_mono_ae hle)
/-- Pointwise derivative rule for the Renyi density integrand. Positivity,
domination, and differentiating under the integral are deliberately outside
this leaf. -/Imports
- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Local dependencies
No Registry dependency inferred.
Downstream consumers
- warm-start comparison
- discretization error conversion