theorem
integrable_of_sq_integrable_finite_measure
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{Y : Ω → ℝ}
(hY_asm : MeasureTheory.AEStronglyMeasurable Y μ)
(hY2 : MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ 2) μ)
:
On a finite measure space, square-integrability (together with a.e. strong
measurability) implies integrability. This follows from the elementary bound
|Y| ≤ Y^2 + 1.
theorem
integrable_mul_of_sq_integrable
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f g : Ω → ℝ}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
(hf2 : MeasureTheory.Integrable (fun (ω : Ω) => f ω ^ 2) μ)
(hg2 : MeasureTheory.Integrable (fun (ω : Ω) => g ω ^ 2) μ)
:
MeasureTheory.Integrable (fun (ω : Ω) => f ω * g ω) μ
If f and g are both integrable and square-integrable, then their pointwise
product ω ↦ f ω * g ω is integrable. This is the Cauchy–Schwarz-style bound
|fg| ≤ (f² + g²)/2.
theorem
martingale_orthogonal_general
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{ℱ : MeasureTheory.Filtration ℕ m0}
{X : ℕ → Ω → ℝ}
(hmart : MeasureTheory.Martingale X ℱ μ)
{m n : ℕ}
(hmn : m ≤ n)
{Y : Ω → ℝ}
(hY_meas : MeasureTheory.StronglyMeasurable Y)
(hY_int : MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ 2) μ)
(hX_sq : ∀ (k : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => X k ω ^ 2) μ)
:
Orthogonality of martingale increments (Lecture 28): if X is a martingale
with E X_n^2 < ∞ for all n, and m ≤ n, then for any ℱ m-measurable
random variable Y with E Y^2 < ∞ we have E[(X_n - X_m) · Y] = 0. In
other words the increment X_n - X_m is orthogonal in L^2 to every
ℱ_m-measurable random variable.