feat: prove reverse Fatou's lemma (Issue #456)

[FrankieNC]

This proves the reverse Fatou sorry in BrownianMotion/StochasticIntegral/DoobMeyer.lean

Statement change

I think the original hypotheses do not imply the conclusion, because of Mathlib's Filter.limsup convention over ℝ: as a conditionally complete lattice, a sequence that is not bounded above has limsup equal to sInf ∅ = 0, not +∞. This lets the right-hand side vanish even when the integrals stay bounded away from 0.

A counterexample, on [0,1] with Lebesgue measure: take independent events A n with P (A n) = 1/n, and set Y ≡ 1 and X n = 1 + √n · 𝟙_{A n}. All four hypotheses hold — X n ≥ 0, Y is integrable and nonnegative, and ∫ (X n - Y)⁺ = √n · P (A n) = 1/√n → 0. Since Σ P (A n) = ∞ and the A n are independent, the Borel–Cantelli lemma places almost every ω in infinitely many A n; on those indices X n ω = 1 + √n → ∞, so (X n ω) is a.e. unbounded above and its limsup is 0 a.e. The right-hand side ∫ limsup_n X n is therefore 0, while ∫ X n = 1 + 1/√n keeps the left-hand side at 1.

Following the issue, I replaced that hypothesis with a single integrable function Y that bounds all the X n from above:

• before: (hX_nonneg : ∀ n, 0 ≤ᵐ[P] X n) (hY : Integrable Y P) (hY_nonneg : 0 ≤ᵐ[P] Y) (h_tendsto : Tendsto (fun n => ∫ ω, max (X n ω - Y ω) 0 ∂P) atTop (𝓝 0))
• after: (hX_meas : ∀ n, Measurable (X n)) (hX_nonneg : ∀ n, 0 ≤ᵐ[P] X n) (hY : Integrable Y P) (hXY : ∀ n, X n ≤ᵐ[P] Y)

I also renamed the lemma to limsup_integral_le_integral_limsup_of_le, since the _of_… suffix should name the governing hypothesis, and that hypothesis has changed.

Closes #456

[FrankieNC]

awaiting-review

[RemyDegenne]

Can you replace the Measurable hypothesis with AEMeasurable? (if that's convenient you can keep the lemma with measurable as auxiliary result, and generalize in a new lemma)

[CoolRmal]

It is good to have this version, but for the application in Doob Meyer's decomposition we won't be able to bound X n by a single integrable random variable, and instead you need to assume that $$\lim\sup X_n$$ is integrable as discussed over here: #Brownian motion > Status of the project

[FrankieNC]

It is good to have this version, but for the application in Doob Meyer's decomposition we won't be able to bound X n by a single integrable random variable, and instead you need to assume that lim sup X n is integrable as discussed over here: #Brownian motion > Status of the project

I see, thanks! I will try to formalise it as suggested then.

[FrankieNC]

Can you replace the Measurable hypothesis with AEMeasurable? (if that's convenient you can keep the lemma with measurable as auxiliary result, and generalize in a new lemma)

Done!

It is good to have this version, but for the application in Doob Meyer's decomposition we won't be able to bound X n by a single integrable random variable, and instead you need to assume that lim sup X n is integrable as discussed over here: #Brownian motion > Status of the project

In the latest commit I proved the following:

theorem limsup_integral_le_integral_of_tendsto_integral_posPart_sub {Ω : Type*}
    {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ℕ → Ω → ℝ} {Y : Ω → ℝ}
    (hX_int : ∀ n, Integrable (X n) P) (hX_nonneg : ∀ n, 0 ≤ᵐ[P] X n) (hY : Integrable Y P)
    (h_tendsto : Tendsto (fun n ↦ ∫ ω, max (X n ω - Y ω) 0 ∂P) atTop (𝓝 0)) :
    limsup (fun n ↦ ∫ ω, X n ω ∂P) atTop ≤ ∫ ω, Y ω ∂P := by

Does this statement work?

[CoolRmal]

I still want limsup to appear on the RHS. The trick is that you can do the following decomposition and then apply limsup_lintegral_le' to $$X_n \wedge Y$$ :

and then use the trivial inequality $$\mathbb{E}[\lim\sup X_n\wedge Y]\le \mathbb{E}[\lim\sup X_n]$$.

After a second thought I think it is probably a good idea to have both the ENNReal version and the real version. For the ENNReal version you probably don't need the integrability of $$\lim\sup X_n$$. For the real version I think eventually we should drop the nonnegativity assumption of $$X_n$$ and instead prove it for any sequence of random variables that are uniformly bdd from below (this is not required for the Doob-Meyer decompostion, you can prove it depending on your availability).

Another point is that all these should be true for countably generated filters instead Nat indexed sequences. You can check out this PR for more info: leanprover-community/mathlib4#37313