Integrability of Bounded Time Integrals

This auxiliary statement establishes integrability of time integrals along a cutoff Eldan process.

Let $P$ be a probability measure on $\Omega$, let $p_t(\omega)$ be an IsEldanCutoff process, and let $\varphi$ be a continuous real-valued function on the parameter space. Suppose that for some $B\in\mathbb R$,

$$|\varphi(p_s(\omega))|\leq B$$

for $P$-almost every $\omega$, simultaneously for every $s\geq 0$. Then, for every $T\geq 0$, the random variable

$$\omega\longmapsto\int_{(0,T]}\varphi(p_s(\omega))\,ds$$

is $P$-integrable.

The result supplies a basic integrability tool for later time-integration and interchange arguments.

Formalization Note. The almost-everywhere bound is uniform over all nonnegative times, and the time integral is with respect to Lebesgue measure restricted to $(0,T]$.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem IsEldanCutoff.integrable_integral_of_ae_bound (h : IsEldanCutoff μ hc W ℱ hW γ p)
    {φ : Param n → ℝ} (hφ : Continuous φ) {B : ℝ}
    (hB : ∀ᵐ ω ∂P, ∀ s : ℝ, 0 ≤ s → |φ (p s ω)| ≤ B) {T : ℝ} (hT : 0 ≤ T) :
    Integrable (fun ω => ∫ s in Set.Ioc (0 : ℝ) T, φ (p s ω)) P

Module navigation

Module: KLS/BKL/Localization/Process/Integral.

Definition modules: KLS/BKL/Localization/Process/Basic, KLS/BKL/Localization/Coefficients, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim.

Supporting theorems: IsEldanCutoff.continuous.

Next: IsEldanCutoff.measurable_uncurry_path.

Source excerpt, lines 28–31 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Process_Integral

open MeasureTheory ProbabilityTheory Filter Topology
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
variable {μ hc} {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P n} {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
  {hW : ∀ k, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ} {γ : FunctionalInequalities.KLS.BKL.Localization.Param n → ℝ} {p : ℝ → Ω → FunctionalInequalities.KLS.BKL.Localization.Param n}

theorem FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.integrable_integral_of_ae_bound_readable (h : IsEldanCutoff μ hc W ℱ hW γ p)
    {φ : Param n → ℝ} (hφ : Continuous φ) {B : ℝ}
    (hB : ∀ᵐ ω ∂P, ∀ s : ℝ, 0 ≤ s → |φ (p s ω)| ≤ B) {T : ℝ} (hT : 0 ≤ T) :
    Integrable (fun ω => ∫ s in Set.Ioc (0 : ℝ) T, φ (p s ω)) P := by sorry