[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : upcrossings a b f ω ≠ ⊤
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
[PROOFSTEP]
rw [← lt_top_iff_ne_top, upcrossings_lt_top_iff] at hω 
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
[PROOFSTEP]
replace hω : ∃ k, ∀ N, upcrossingsBefore a b f N ω < k
[GOAL]
case hω
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
[PROOFSTEP]
obtain ⟨k, hk⟩ := hω
[GOAL]
case hω.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
[PROOFSTEP]
exact ⟨k + 1, fun N => lt_of_le_of_lt (hk N) k.lt_succ_self⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a
h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω
⊢ False
[PROOFSTEP]
rw [frequently_atTop] at h₁ h₂ 
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
⊢ False
[PROOFSTEP]
refine' Classical.not_not.2 hω _
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
⊢ ¬∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
[PROOFSTEP]
push_neg
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
⊢ ∀ (k : ℕ), ∃ N, k ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
intro k
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
k : ℕ
⊢ ∃ N, k ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
induction' k with k ih
[GOAL]
case intro.zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
⊢ ∃ N, Nat.zero ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
simp only [Nat.zero_eq, zero_le, exists_const]
[GOAL]
case intro.succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
k : ℕ
ih : ∃ N, k ≤ upcrossingsBefore a b f N ω
⊢ ∃ N, Nat.succ k ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
obtain ⟨N, hN⟩ := ih
[GOAL]
case intro.succ.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
⊢ ∃ N, Nat.succ k ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N
[GOAL]
case intro.succ.intro.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
N₁ : ℕ
hN₁ : N₁ ≥ N
hN₁' : f N₁ ω < a
⊢ ∃ N, Nat.succ k ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁
[GOAL]
case intro.succ.intro.intro.intro.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, b ≥ a_1 ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, b_1 ≥ a ∧ b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
N₁ : ℕ
hN₁ : N₁ ≥ N
hN₁' : f N₁ ω < a
N₂ : ℕ
hN₂ : N₂ ≥ N₁
hN₂' : b < f N₂ ω
⊢ ∃ N, Nat.succ k ≤ upcrossingsBefore a b f N ω
[PROOFSTEP]
exact ⟨N₂ + 1, Nat.succ_le_of_lt <| lt_of_le_of_lt hN (upcrossingsBefore_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
by_cases h : IsBoundedUnder (· ≤ ·) atTop fun n => |f n ω|
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => |f n ω|
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
rw [isBoundedUnder_le_abs] at h 
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h :
  (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => f n ω) ∧
    IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop fun n => f n ω
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
refine' tendsto_of_no_upcrossings Rat.denseRange_cast _ h.1 h.2
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h :
  (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => f n ω) ∧
    IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop fun n => f n ω
⊢ ∀ (a : ℝ),
    a ∈ Set.range Rat.cast →
      ∀ (b : ℝ), b ∈ Set.range Rat.cast → a < b → ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
[PROOFSTEP]
intro a ha b hb hab
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h :
  (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => f n ω) ∧
    IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop fun n => f n ω
a : ℝ
ha : a ∈ Set.range Rat.cast
b : ℝ
hb : b ∈ Set.range Rat.cast
hab : a < b
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
[PROOFSTEP]
obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := ha, hb
[GOAL]
case pos.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h :
  (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => f n ω) ∧
    IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop fun n => f n ω
a b : ℚ
hab : ↑a < ↑b
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < ↑a) ∧ ∃ᶠ (n : ℕ) in atTop, ↑b < f n ω)
[PROOFSTEP]
exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => |f n ω|
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
obtain ⟨a, b, hab, h₁, h₂⟩ := ENNReal.exists_upcrossings_of_not_bounded_under hf₁.ne h
[GOAL]
case neg.intro.intro.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => |f n ω|
a b : ℚ
hab : a < b
h₁ : ∃ᶠ (i : ℕ) in atTop, f i ω < ↑a
h₂ : ∃ᶠ (i : ℕ) in atTop, ↑b < f i ω
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
exact False.elim ((hf₂ a b hab).ne (upcrossings_eq_top_of_frequently_lt (Rat.cast_lt.2 hab) h₁ h₂))
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, upcrossings a b f ω < ⊤
[PROOFSTEP]
refine' ae_lt_top (hf.adapted.measurable_upcrossings hab) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ⊤
[PROOFSTEP]
have := hf.mul_lintegral_upcrossings_le_lintegral_pos_part a b
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ⊤
[PROOFSTEP]
rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this 
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ⊤
[PROOFSTEP]
refine' (lt_of_le_of_lt this (ENNReal.div_lt_top _ _)).ne
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ⊤
[PROOFSTEP]
have hR' : ∀ n, ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ R + ‖a‖₊ * μ Set.univ :=
  by
  simp_rw [snorm_one_eq_lintegral_nnnorm] 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
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
[PROOFSTEP]
simp_rw [snorm_one_eq_lintegral_nnnorm] at hbdd 
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
⊢ ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
[PROOFSTEP]
intro n
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
n : ℕ
⊢ ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
[PROOFSTEP]
refine' (lintegral_mono _ : ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ ∫⁻ ω, ‖f n ω‖₊ + ‖a‖₊ ∂μ).trans _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
n : ℕ
⊢ (fun ω => ↑‖f n ω - a‖₊) ≤ fun ω => ↑‖f n ω‖₊ + ↑‖a‖₊
[PROOFSTEP]
intro ω
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
n : ℕ
ω : Ω
⊢ (fun ω => ↑‖f n ω - a‖₊) ω ≤ (fun ω => ↑‖f n ω‖₊ + ↑‖a‖₊) ω
[PROOFSTEP]
simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ENNReal.coe_add, ENNReal.coe_le_coe]
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
n : ℕ
ω : Ω
⊢ ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊
[PROOFSTEP]
exact nnnorm_add_le _ _
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
n : ℕ
⊢ ∫⁻ (a_1 : Ω), ↑‖f n a_1‖₊ + ↑‖a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
[PROOFSTEP]
simp_rw [lintegral_add_right _ measurable_const, lintegral_const]
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ↑‖f n x‖₊ ∂μ ≤ ↑R
n : ℕ
⊢ ∫⁻ (a : Ω), ↑‖f n a‖₊ ∂μ + ↑‖a‖₊ * ↑↑μ Set.univ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
[PROOFSTEP]
exact add_le_add (hbdd _) le_rfl
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
⊢ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ⊤
[PROOFSTEP]
refine'
  ne_of_lt
    (iSup_lt_iff.2
      ⟨R + ‖a‖₊ * μ Set.univ,
        ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.mul_lt_top ENNReal.coe_lt_top.ne (measure_ne_top _ _)⟩,
        fun n => le_trans _ (hR' n)⟩)
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
⊢ ∫⁻ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ∂μ ≤ ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ
[PROOFSTEP]
refine' lintegral_mono fun ω => _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
⊢ ENNReal.ofReal (f n ω - a)⁺ ≤ ↑‖f n ω - a‖₊
[PROOFSTEP]
rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
⊢ ↑‖f n ω - a‖₊ ≠ ⊤
[PROOFSTEP]
by_cases hnonneg : 0 ≤ f n ω - a
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
hnonneg : 0 ≤ f n ω - a
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
[PROOFSTEP]
rw [LatticeOrderedGroup.pos_of_nonneg _ hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
hnonneg : ¬0 ≤ f n ω - a
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
[PROOFSTEP]
rw [LatticeOrderedGroup.pos_of_nonpos _ (not_le.1 hnonneg).le]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
hnonneg : ¬0 ≤ f n ω - a
⊢ 0 ≤ ‖f n ω - a‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * ↑↑μ Set.univ
n : ℕ
ω : Ω
⊢ ↑‖f n ω - a‖₊ ≠ ⊤
[PROOFSTEP]
simp only [Ne.def, ENNReal.coe_ne_top, not_false_iff]
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ENNReal.ofReal (b - a) ≠ 0
[PROOFSTEP]
simp only [hab, Ne.def, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]
[GOAL]
case h0
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ 0 ∨ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ 0
[PROOFSTEP]
simp only [hab, Ne.def, ENNReal.ofReal_eq_zero, sub_nonpos, not_le, true_or_iff]
[GOAL]
case ht
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
hab : a < b
this :
  (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ⊤ ∨ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ⊤
[PROOFSTEP]
simp only [Ne.def, ENNReal.ofReal_ne_top, not_false_iff, true_or_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
[PROOFSTEP]
simp only [ae_all_iff, eventually_imp_distrib_left]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∀ (i i_1 : ℚ), i < i_1 → ∀ᵐ (x : Ω) ∂μ, upcrossings (↑i) (↑i_1) f x < ⊤
[PROOFSTEP]
rintro a b hab
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
a b : ℚ
hab : a < b
⊢ ∀ᵐ (x : Ω) ∂μ, upcrossings (↑a) (↑b) f x < ⊤
[PROOFSTEP]
exact hf.upcrossings_ae_lt_top' hbdd (Rat.cast_lt.2 hab)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
filter_upwards [hf.upcrossings_ae_lt_top hbdd,
  ae_bdd_liminf_atTop_of_snorm_bdd one_ne_zero (fun n => (hf.stronglyMeasurable n).measurable.mono (ℱ.le n) le_rfl)
    hbdd] with
  ω h₁ h₂
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h₂ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
exact tendsto_of_uncrossing_lt_top h₂ h₁
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂Measure.trim μ (_ : sSup (Set.range fun n => ↑ℱ n) ≤ m0), ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
rw [@ae_iff _ (⨆ n, ℱ n) _ _, trim_measurableSet_eq]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ↑↑μ {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)} = 0
[PROOFSTEP]
exact hf.exists_ae_tendsto_of_bdd hbdd
[GOAL]
case hs
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ MeasurableSet {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)}
[PROOFSTEP]
exact
  MeasurableSet.compl
    (@measurableSet_exists_tendsto _ _ _ _ _ _ (⨆ n, ℱ n) _ _ _ _ _ fun n =>
      (hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩) le_rfl)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
[PROOFSTEP]
classical
suffices ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
  by
  rw [limitProcess, dif_pos this]
  exact (Classical.choose_spec this).2
set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) :=
  by
  filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
  simp_rw [dif_pos hω]
  exact hω.choose_spec
have hg'm : @AEStronglyMeasurable _ _ _ (⨆ n, ℱ n) g' (μ.trim hle) :=
  (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n) le_rfl).aemeasurable)
      hg').aestronglyMeasurable
obtain ⟨g, hgm, hae⟩ := hg'm
have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) :=
  by
  filter_upwards [hae, hg'] with ω hω hg'ω
  exact hω ▸ hg'ω
exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
[PROOFSTEP]
suffices ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
  by
  rw [limitProcess, dif_pos this]
  exact (Classical.choose_spec this).2
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
this : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
[PROOFSTEP]
rw [limitProcess, dif_pos this]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
this : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (Classical.choose this ω))
[PROOFSTEP]
exact (Classical.choose_spec this).2
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) :=
  by
  filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
  simp_rw [dif_pos hω]
  exact hω.choose_spec
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
⊢ ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
[PROOFSTEP]
filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
ω : Ω
hω : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0))
[PROOFSTEP]
simp_rw [dif_pos hω]
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
ω : Ω
hω : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (Exists.choose hω))
[PROOFSTEP]
exact hω.choose_spec
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
have hg'm : @AEStronglyMeasurable _ _ _ (⨆ n, ℱ n) g' (μ.trim hle) :=
  (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n) le_rfl).aemeasurable)
      hg').aestronglyMeasurable
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
hg'm : AEStronglyMeasurable g' (Measure.trim μ hle)
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
obtain ⟨g, hgm, hae⟩ := hg'm
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[Measure.trim μ hle] g
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) :=
  by
  filter_upwards [hae, hg'] with ω hω hg'ω
  exact hω ▸ hg'ω
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[Measure.trim μ hle] g
⊢ ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
filter_upwards [hae, hg'] with ω hω hg'ω
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω✝ : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[Measure.trim μ hle] g
ω : Ω
hω : (if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0) = g ω
hg'ω : Tendsto (fun n => f n ω) atTop (𝓝 (if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0))
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
exact hω ▸ hg'ω
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), snorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then Exists.choose h else 0
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[Measure.trim μ hle] g
hg : ∀ᵐ (ω : Ω) ∂Measure.trim μ hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
[PROOFSTEP]
exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
⊢ Tendsto (fun n => snorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
[PROOFSTEP]
obtain ⟨R, hR⟩ := hunif.2.2
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm (f i) 1 μ ≤ ↑R
⊢ Tendsto (fun n => snorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
[PROOFSTEP]
have hmeas : ∀ n, AEStronglyMeasurable (f n) μ := fun n =>
  ((hf.stronglyMeasurable n).mono (ℱ.le _)).aestronglyMeasurable
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm (f i) 1 μ ≤ ↑R
hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
⊢ Tendsto (fun n => snorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
[PROOFSTEP]
exact
  tendsto_Lp_of_tendstoInMeasure _ le_rfl ENNReal.one_ne_top hmeas (memℒp_limitProcess_of_snorm_bdd hmeas hR) hunif.2.1
    (tendstoInMeasure_of_tendsto_ae hmeas <| hf.ae_tendsto_limitProcess hR)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ f n =ᵐ[μ] μ[g|↑ℱ n]
[PROOFSTEP]
rw [← sub_ae_eq_zero, ←
  snorm_eq_zero_iff
    (((hf.stronglyMeasurable n).mono (ℱ.le _)).sub (stronglyMeasurable_condexp.mono (ℱ.le _))).aestronglyMeasurable
    one_ne_zero]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ snorm (f n - μ[g|↑ℱ n]) 1 μ = 0
[PROOFSTEP]
have ht : Tendsto (fun m => snorm (μ[f m - g|ℱ n]) 1 μ) atTop (𝓝 0) :=
  haveI hint : ∀ m, Integrable (f m - g) μ := fun m => (hf.integrable m).sub hg
  tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hgtends (fun m => zero_le _) fun m =>
    snorm_one_condexp_le_snorm _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => snorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ snorm (f n - μ[g|↑ℱ n]) 1 μ = 0
[PROOFSTEP]
have hev : ∀ m ≥ n, snorm (μ[f m - g|ℱ n]) 1 μ = snorm (f n - μ[g|ℱ n]) 1 μ :=
  by
  refine' fun m hm => snorm_congr_ae ((condexp_sub (hf.integrable m) hg).trans _)
  filter_upwards [hf.2 n m hm] with x hx
  simp only [hx, Pi.sub_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => snorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ ∀ (m : ℕ), m ≥ n → snorm (μ[f m - g|↑ℱ n]) 1 μ = snorm (f n - μ[g|↑ℱ n]) 1 μ
[PROOFSTEP]
refine' fun m hm => snorm_congr_ae ((condexp_sub (hf.integrable m) hg).trans _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => snorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
⊢ μ[f m|↑ℱ n] - μ[g|↑ℱ n] =ᵐ[μ] f n - μ[g|↑ℱ n]
[PROOFSTEP]
filter_upwards [hf.2 n m hm] with x hx
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => snorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
x : Ω
hx : (μ[f m|↑ℱ n]) x = f n x
⊢ (μ[f m|↑ℱ n] - μ[g|↑ℱ n]) x = (f n - μ[g|↑ℱ n]) x
[PROOFSTEP]
simp only [hx, Pi.sub_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ✝
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g
hgtends : Tendsto (fun n => snorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => snorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
hev : ∀ (m : ℕ), m ≥ n → snorm (μ[f m - g|↑ℱ n]) 1 μ = snorm (f n - μ[g|↑ℱ n]) 1 μ
⊢ snorm (f n - μ[g|↑ℱ n]) 1 μ = 0
[PROOFSTEP]
exact tendsto_nhds_unique (tendsto_atTop_of_eventually_const hev) ht
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
have hunif : UniformIntegrable (fun n => μ[g|ℱ n]) 1 μ := hg.uniformIntegrable_condexp_filtration
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
obtain ⟨R, hR⟩ := hunif.2.2
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
have hlimint : Integrable (ℱ.limitProcess (fun n => μ[g|ℱ n]) μ) μ :=
  (memℒp_limitProcess_of_snorm_bdd hunif.1 hR).integrable le_rfl
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
suffices g =ᵐ[μ] ℱ.limitProcess (fun n x => (μ[g|ℱ n]) x) μ
  by
  filter_upwards [this, (martingale_condexp g ℱ μ).submartingale.ae_tendsto_limitProcess hR] with x heq ht
  rwa [heq]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this : g =ᵐ[μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
filter_upwards [this, (martingale_condexp g ℱ μ).submartingale.ae_tendsto_limitProcess hR] with x heq ht
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this : g =ᵐ[μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ
x : Ω
heq : g x = limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x
ht : Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (limitProcess (fun i => μ[g|↑ℱ i]) ℱ μ x))
⊢ Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
[PROOFSTEP]
rwa [heq]
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
⊢ g =ᵐ[μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ
[PROOFSTEP]
have : ∀ n s, MeasurableSet[ℱ n] s → ∫ x in s, g x ∂μ = ∫ x in s, ℱ.limitProcess (fun n x => (μ[g|ℱ n]) x) μ x ∂μ :=
  by
  intro n s hs
  rw [← set_integral_condexp (ℱ.le n) hg hs, ← set_integral_condexp (ℱ.le n) hlimint hs]
  refine' set_integral_congr_ae (ℱ.le _ _ hs) _
  filter_upwards [(martingale_condexp g ℱ μ).ae_eq_condexp_limitProcess hunif n] with x hx _
  rw [hx]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
⊢ ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
intro n s hs
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rw [← set_integral_condexp (ℱ.le n) hg hs, ← set_integral_condexp (ℱ.le n) hlimint hs]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (x : Ω) in s, (μ[g|↑ℱ n]) x ∂μ = ∫ (x : Ω) in s, (μ[limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ|↑ℱ n]) x ∂μ
[PROOFSTEP]
refine' set_integral_congr_ae (ℱ.le _ _ hs) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → (μ[g|↑ℱ n]) x = (μ[limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ|↑ℱ n]) x
[PROOFSTEP]
filter_upwards [(martingale_condexp g ℱ μ).ae_eq_condexp_limitProcess hunif n] with x hx _
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
n : ℕ
s : Set Ω
hs : MeasurableSet s
x : Ω
hx : (μ[g|↑ℱ n]) x = (μ[limitProcess (fun i => μ[g|↑ℱ i]) ℱ μ|↑ℱ n]) x
a✝ : x ∈ s
⊢ (μ[g|↑ℱ n]) x = (μ[limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ|↑ℱ n]) x
[PROOFSTEP]
rw [hx]
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
⊢ g =ᵐ[μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ
[PROOFSTEP]
refine'
  ae_eq_of_forall_set_integral_eq_of_sigmaFinite' hle (fun s _ _ => hg.integrableOn) (fun s _ _ => hlimint.integrableOn)
    (fun s hs => _) hgmeas.aeStronglyMeasurable' stronglyMeasurable_limitProcess.aeStronglyMeasurable'
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
⊢ ↑↑μ s < ⊤ → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
apply @MeasurableSpace.induction_on_inter _ _ _ (⨆ n, ℱ n) (MeasurableSpace.measurableSpace_iSup_eq ℱ) _ _ _ _ _ _ hs
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
⊢ IsPiSystem {s | ∃ n, MeasurableSet s}
[PROOFSTEP]
rintro s ⟨n, hs⟩ t ⟨m, ht⟩ -
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s✝ : Set Ω
hs✝ : MeasurableSet s✝
s : Set Ω
n : ℕ
hs : MeasurableSet s
t : Set Ω
m : ℕ
ht : MeasurableSet t
⊢ s ∩ t ∈ {s | ∃ n, MeasurableSet s}
[PROOFSTEP]
by_cases hnm : n ≤ m
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s✝ : Set Ω
hs✝ : MeasurableSet s✝
s : Set Ω
n : ℕ
hs : MeasurableSet s
t : Set Ω
m : ℕ
ht : MeasurableSet t
hnm : n ≤ m
⊢ s ∩ t ∈ {s | ∃ n, MeasurableSet s}
[PROOFSTEP]
exact ⟨m, (ℱ.mono hnm _ hs).inter ht⟩
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s✝ : Set Ω
hs✝ : MeasurableSet s✝
s : Set Ω
n : ℕ
hs : MeasurableSet s
t : Set Ω
m : ℕ
ht : MeasurableSet t
hnm : ¬n ≤ m
⊢ s ∩ t ∈ {s | ∃ n, MeasurableSet s}
[PROOFSTEP]
exact ⟨n, hs.inter (ℱ.mono (not_le.1 hnm).le _ ht)⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
⊢ ↑↑μ ∅ < ⊤ → ∫ (x : Ω) in ∅, g x ∂μ = ∫ (x : Ω) in ∅, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
simp only [measure_empty, WithTop.zero_lt_top, Measure.restrict_empty, integral_zero_measure, forall_true_left]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (t : Set Ω),
    t ∈ {s | ∃ n, MeasurableSet s} →
      ↑↑μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rintro t ⟨n, ht⟩ -
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
t : Set Ω
n : ℕ
ht : MeasurableSet t
⊢ ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
exact this n _ ht
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (t : Set Ω),
    MeasurableSet t →
      (↑↑μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ) →
        ↑↑μ tᶜ < ⊤ → ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rintro t htmeas ht -
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
t : Set Ω
htmeas : MeasurableSet t
ht : ↑↑μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
have hgeq := @integral_add_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
t : Set Ω
htmeas : MeasurableSet t
ht : ↑↑μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
hgeq :
  ∫ (x : Ω) in t, g x ∂Measure.trim μ hle + ∫ (x : Ω) in tᶜ, g x ∂Measure.trim μ hle =
    ∫ (x : Ω), g x ∂Measure.trim μ hle
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
have hheq := @integral_add_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hlimint.trim hle stronglyMeasurable_limitProcess)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
t : Set Ω
htmeas : MeasurableSet t
ht : ↑↑μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
hgeq :
  ∫ (x : Ω) in t, g x ∂Measure.trim μ hle + ∫ (x : Ω) in tᶜ, g x ∂Measure.trim μ hle =
    ∫ (x : Ω), g x ∂Measure.trim μ hle
hheq :
  ∫ (x : Ω) in t, limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ x ∂Measure.trim μ hle +
      ∫ (x : Ω) in tᶜ, limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ x ∂Measure.trim μ hle =
    ∫ (x : Ω), limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ x ∂Measure.trim μ hle
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rw [add_comm, ← eq_sub_iff_add_eq] at hgeq hheq 
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
t : Set Ω
htmeas : MeasurableSet t
ht : ↑↑μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
hgeq :
  ∫ (x : Ω) in tᶜ, g x ∂Measure.trim μ hle =
    ∫ (x : Ω), g x ∂Measure.trim μ hle - ∫ (x : Ω) in t, g x ∂Measure.trim μ hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ x ∂Measure.trim μ hle =
    ∫ (x : Ω), limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ x ∂Measure.trim μ hle -
      ∫ (x : Ω) in t, limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ x ∂Measure.trim μ hle
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rw [set_integral_trim hle hgmeas htmeas.compl, set_integral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq,
  hheq, ← set_integral_trim hle hgmeas htmeas, ← set_integral_trim hle stronglyMeasurable_limitProcess htmeas, ←
  integral_trim hle hgmeas, ← integral_trim hle stronglyMeasurable_limitProcess, ← integral_univ,
  this 0 _ MeasurableSet.univ, integral_univ, ht (measure_lt_top _ _)]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (f : ℕ → Set Ω),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ),
            ↑↑μ (f i) < ⊤ →
              ∫ (x : Ω) in f i, g x ∂μ = ∫ (x : Ω) in f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ) →
          ↑↑μ (⋃ (i : ℕ), f i) < ⊤ →
            ∫ (x : Ω) in ⋃ (i : ℕ), f i, g x ∂μ =
              ∫ (x : Ω) in ⋃ (i : ℕ), f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rintro f hf hfmeas heq -
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f✝ : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
f : ℕ → Set Ω
hf : Pairwise (Disjoint on f)
hfmeas : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (i : ℕ),
    ↑↑μ (f i) < ⊤ → ∫ (x : Ω) in f i, g x ∂μ = ∫ (x : Ω) in f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
⊢ ∫ (x : Ω) in ⋃ (i : ℕ), f i, g x ∂μ = ∫ (x : Ω) in ⋃ (i : ℕ), f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
[PROOFSTEP]
rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
  integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f✝ : ℕ → Ω → ℝ
ω : Ω
R✝ : ℝ≥0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), snorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ)
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
f : ℕ → Set Ω
hf : Pairwise (Disjoint on f)
hfmeas : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (i : ℕ),
    ↑↑μ (f i) < ⊤ → ∫ (x : Ω) in f i, g x ∂μ = ∫ (x : Ω) in f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
⊢ ∑' (n : ℕ), ∫ (a : Ω) in f n, g a ∂μ = ∑' (n : ℕ), ∫ (a : Ω) in f n, limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ a ∂μ
[PROOFSTEP]
exact tsum_congr fun n => heq _ (measure_lt_top _ _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
[PROOFSTEP]
have ht : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ℱ n]) x)) :=
  integrable_condexp.tendsto_ae_condexp stronglyMeasurable_condexp
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
[PROOFSTEP]
have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x = (μ[g|ℱ n]) x := fun n =>
  condexp_condexp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
[PROOFSTEP]
rw [← ae_all_iff] at heq 
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
[PROOFSTEP]
filter_upwards [heq, ht] with x hxeq hxt
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a
x : Ω
hxeq : ∀ (i : ℕ), (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ i]) x = (μ[g|↑ℱ i]) x
hxt : Tendsto (fun n => (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
⊢ Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ (n : ℕ), ↑ℱ n]) x))
[PROOFSTEP]
exact hxt.congr hxeq
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
⊢ Tendsto (fun n => snorm (μ[g|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
[PROOFSTEP]
have ht : Tendsto (fun n => snorm (μ[μ[g|⨆ n, ℱ n]|ℱ n] - μ[g|⨆ n, ℱ n]) 1 μ) atTop (𝓝 0) :=
  integrable_condexp.tendsto_snorm_condexp stronglyMeasurable_condexp
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : Tendsto (fun n => snorm (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ Tendsto (fun n => snorm (μ[g|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
[PROOFSTEP]
have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x = (μ[g|ℱ n]) x := fun n =>
  condexp_condexp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : Tendsto (fun n => snorm (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ Tendsto (fun n => snorm (μ[g|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
[PROOFSTEP]
refine' ht.congr fun n => snorm_congr_ae _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : Tendsto (fun n => snorm (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
n : ℕ
⊢ μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n] =ᵐ[μ] μ[g|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]
[PROOFSTEP]
filter_upwards [heq n] with x hxeq
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
g✝ g : Ω → ℝ
ht : Tendsto (fun n => snorm (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
n : ℕ
x : Ω
hxeq : (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ (μ[μ[g|⨆ (n : ℕ), ↑ℱ n]|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) x = (μ[g|↑ℱ n] - μ[g|⨆ (n : ℕ), ↑ℱ n]) x
[PROOFSTEP]
simp only [hxeq, Pi.sub_apply]
