Finite Energy Under Quadratic Domination

This vendored technical lemma proves finiteness of a square-integrated energy under pointwise domination.

Let $\Omega$ be a measurable space with measure $P$, and let $H_1,H_2,K:\Omega\times\mathbb R\to\mathbb R$. Assume:

1. For every $(\omega,s)$,

2. The uncurried functions $H_1$ and $H_2$ are measurable.
3. For every $T>0$, the double ENNReal energy integrals of $H_1$ and $H_2$ over $\Omega\times[0,T]$ are strictly below $\infty$.

Then, for every $T>0$, the corresponding double energy integral of $K$ is also strictly below $\infty$:

No probability-measure instance is required by the theorem. This is a technical integrability tool for Itô-integrand constructions.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem lintegral_energy_lt_top_of_bound {K : Ω → ℝ → ℝ}
    (hbound : ∀ ω s, (‖K ω s‖₊ : ℝ≥0∞) ^ 2
      ≤ 2 * ((‖H₁ ω s‖₊ : ℝ≥0∞) ^ 2 + (‖H₂ ω s‖₊ : ℝ≥0∞) ^ 2))
    (hm₁ : Measurable (Function.uncurry H₁)) (hm₂ : Measurable (Function.uncurry H₂))
    (hq₁ : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H₁ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hq₂ : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H₂ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) :
    ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤

Module navigation

Module: LevyStochCalc/Brownian/ItoLinear.

Previous: lintegral_energy_parallelogram · Next: lintegral_energy_const_mul.

Source excerpt, lines 104–113 · Frozen source 408915f.