Support-Bound Preservation Under Exponential Tilting
ProvedFunctionalInequalities.Probability.Posterior.norm_integral_tilted_le_of_compact_readableThis statement formalizes the support-bound estimate for tilted expectations in the compact-prior stage of Bizeul–Klartag–Lehec, p. 19.
Let be a topological, measurable, Borel, second-countable space, and let be a probability measure with compact support. Let be continuous and let be measurable. Suppose satisfies and
on the support of . Then the integral of against the exponentially tilted measure is bounded by the same constant:
This is a finite-valued norm estimate for a tilted probability expectation and is useful for controlling posterior statistics.
Original Lean declaration header
Within namespace FunctionalInequalities.Probability.Posterior. Shown in its original module context. Proof omitted.
theorem norm_integral_tilted_le_of_compact (μ : ProbabilityMeasure Ω)
(hc : IsCompact (μ : Measure Ω).support) {φ f : Ω → ℝ}
(hφ : Continuous φ) (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
(hb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
‖∫ x, f x ∂((μ : Measure Ω).tilted φ)‖ ≤ C
Module navigation
Module: Probability/Posterior/CompactPrior.
Previous: expectation_hasDerivAt_of_compact · Next: covariance_hasDerivAt_of_compact.
Source excerpt, lines 174–178 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactPrior
open MeasureTheory Filter Topology ProbabilityTheory
variable {Ω : Type*} [TopologicalSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]
[SecondCountableTopology Ω]
theorem FunctionalInequalities.Probability.Posterior.norm_integral_tilted_le_of_compact_readable (μ : ProbabilityMeasure Ω)
(hc : IsCompact (μ : Measure Ω).support) {φ f : Ω → ℝ}
(hφ : Continuous φ) (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
(hb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
‖∫ x, f x ∂((μ : Measure Ω).tilted φ)‖ ≤ C := by sorry