Lean4
/-- An L¹-bounded submartingale has bounded upcrossings almost everywhere. -/
theorem upcrossings_ae_lt_top' [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R)
(hab : a < b) : ∀ᵐ ω ∂μ, upcrossings a b f ω < ∞ :=
by
refine ae_lt_top (hf.adapted.measurable_upcrossings hab) ?_
have := hf.mul_lintegral_upcrossings_le_lintegral_pos_part a b
rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this
· refine (lt_of_le_of_lt this (ENNReal.div_lt_top ?_ ?_)).ne
· have hR' : ∀ n, ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ R + ‖a‖₊ * μ Set.univ :=
by
simp_rw [eLpNorm_one_eq_lintegral_enorm] at hbdd
intro n
refine (lintegral_mono ?_ : ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ ∫⁻ ω, ‖f n ω‖₊ + ‖a‖₊ ∂μ).trans ?_
· intro ω
simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ENNReal.coe_add, ENNReal.coe_le_coe]
exact nnnorm_add_le _ _
· simp_rw [lintegral_add_right _ measurable_const, lintegral_const]
exact add_le_add (hbdd _) le_rfl
refine
ne_of_lt
(iSup_lt_iff.2
⟨R + ‖a‖₊ * μ Set.univ, ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, by finiteness⟩, fun n =>
le_trans ?_ (hR' n)⟩)
refine lintegral_mono fun ω => ?_
rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]
· by_cases hnonneg : 0 ≤ f n ω - a
· rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
· rw [posPart_eq_zero.2 (not_le.1 hnonneg).le]
exact norm_nonneg _
· finiteness
· simp only [hab, Ne, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]
· left; simp only [hab, Ne, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]
· left; finiteness
