Martingale Helper Lemmas #
Contents #
lintegral_fatou_ofReal_norm: Fatou's lemma forENNReal.ofReal ∘ ‖·‖
References #
- Durrett, Probability: Theory and Examples (2019), Section 5.5
- Williams, Probability with Martingales (1991)
Fatou-Type Lemmas #
theorem
Exchangeability.Probability.lintegral_fatou_ofReal_norm
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasurableSpace β]
[NormedAddCommGroup β]
[BorelSpace β]
{u : ℕ → α → β}
{g : α → β}
(hae : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => u n x) Filter.atTop (nhds (g x)))
(hu_meas : ∀ (n : ℕ), AEMeasurable (fun (x : α) => ENNReal.ofReal ‖u n x‖) μ)
(_hg_meas : AEMeasurable (fun (x : α) => ENNReal.ofReal ‖g x‖) μ)
:
∫⁻ (x : α), ENNReal.ofReal ‖g x‖ ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (x : α), ENNReal.ofReal ‖u n x‖ ∂μ) Filter.atTop
Fatou's lemma on ENNReal.ofReal ∘ ‖·‖ along an a.e. pointwise limit.
If u n x → g x a.e., then ∫⁻ ‖g‖ ≤ liminf (∫⁻ ‖u n‖).