[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ leastGE f r (π ω) ω = min (π ω) (leastGE f r n ω)
[PROOFSTEP]
classical
refine' le_antisymm (le_min (leastGE_le _) (leastGE_mono (hπn ω) r ω)) _
by_cases hle : π ω ≤ leastGE f r n ω
· rw [min_eq_left hle, leastGE]
  by_cases h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
  · refine' hle.trans (Eq.le _)
    rw [leastGE, ← hitting_eq_hitting_of_exists (hπn ω) h]
  · simp only [hitting, if_neg h, le_rfl]
· rw [min_eq_right (not_le.1 hle).le, leastGE, leastGE, ← hitting_eq_hitting_of_exists (hπn ω) _]
  rw [not_le, leastGE, hitting_lt_iff _ (hπn ω)] at hle 
  exact
    let ⟨j, hj₁, hj₂⟩ := hle
    ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ leastGE f r (π ω) ω = min (π ω) (leastGE f r n ω)
[PROOFSTEP]
refine' le_antisymm (le_min (leastGE_le _) (leastGE_mono (hπn ω) r ω)) _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ min (π ω) (leastGE f r n ω) ≤ leastGE f r (π ω) ω
[PROOFSTEP]
by_cases hle : π ω ≤ leastGE f r n ω
[GOAL]
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
⊢ min (π ω) (leastGE f r n ω) ≤ leastGE f r (π ω) ω
[PROOFSTEP]
rw [min_eq_left hle, leastGE]
[GOAL]
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω
[PROOFSTEP]
by_cases h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
[GOAL]
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ∃ j, j ∈ Set.Icc 0 (π ω) ∧ f j ω ∈ Set.Ici r
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω
[PROOFSTEP]
refine' hle.trans (Eq.le _)
[GOAL]
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ∃ j, j ∈ Set.Icc 0 (π ω) ∧ f j ω ∈ Set.Ici r
⊢ leastGE f r n ω = hitting f (Set.Ici r) 0 (π ω) ω
[PROOFSTEP]
rw [leastGE, ← hitting_eq_hitting_of_exists (hπn ω) h]
[GOAL]
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ¬∃ j, j ∈ Set.Icc 0 (π ω) ∧ f j ω ∈ Set.Ici r
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω
[PROOFSTEP]
simp only [hitting, if_neg h, le_rfl]
[GOAL]
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ¬π ω ≤ leastGE f r n ω
⊢ min (π ω) (leastGE f r n ω) ≤ leastGE f r (π ω) ω
[PROOFSTEP]
rw [min_eq_right (not_le.1 hle).le, leastGE, leastGE, ← hitting_eq_hitting_of_exists (hπn ω) _]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ¬π ω ≤ leastGE f r n ω
⊢ ∃ j, j ∈ Set.Icc 0 (π ω) ∧ f j ω ∈ Set.Ici r
[PROOFSTEP]
rw [not_le, leastGE, hitting_lt_iff _ (hπn ω)] at hle 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ∃ j, j ∈ Set.Ico 0 (π ω) ∧ f j ω ∈ Set.Ici r
⊢ ∃ j, j ∈ Set.Icc 0 (π ω) ∧ f j ω ∈ Set.Ici r
[PROOFSTEP]
exact
  let ⟨j, hj₁, hj₂⟩ := hle
  ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f✝ : ℕ → Ω → ℝ
ω : Ω
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ stoppedValue (fun i => stoppedValue f (leastGE f r i)) π = stoppedValue (stoppedProcess f (leastGE f r n)) π
[PROOFSTEP]
ext1 ω
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f✝ : ℕ → Ω → ℝ
ω✝ : Ω
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
ω : Ω
⊢ stoppedValue (fun i => stoppedValue f (leastGE f r i)) π ω = stoppedValue (stoppedProcess f (leastGE f r n)) π ω
[PROOFSTEP]
simp_rw [stoppedProcess, stoppedValue]
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f✝ : ℕ → Ω → ℝ
ω✝ : Ω
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
ω : Ω
⊢ f (leastGE f r (π ω) ω) ω = f (min (π ω) (leastGE f r n ω)) ω
[PROOFSTEP]
rw [leastGE_eq_min _ _ _ hπn]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
⊢ Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ
[PROOFSTEP]
rw [submartingale_iff_expected_stoppedValue_mono]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
⊢ ∀ (τ π : Ω → ℕ),
    IsStoppingTime ℱ τ →
      IsStoppingTime ℱ π →
        τ ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ N) →
            ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) τ x ∂μ ≤
              ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) π x ∂μ
[PROOFSTEP]
intro σ π hσ hπ hσ_le_π hπ_bdd
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ N, ∀ (x : Ω), π x ≤ N
⊢ ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) σ x ∂μ ≤
    ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) π x ∂μ
[PROOFSTEP]
obtain ⟨n, hπ_le_n⟩ := hπ_bdd
[GOAL]
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) σ x ∂μ ≤
    ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) π x ∂μ
[PROOFSTEP]
simp_rw [stoppedValue_stoppedValue_leastGE f σ r fun i => (hσ_le_π i).trans (hπ_le_n i)]
[GOAL]
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f (leastGE f r n)) σ x ∂μ ≤
    ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) π x ∂μ
[PROOFSTEP]
simp_rw [stoppedValue_stoppedValue_leastGE f π r hπ_le_n]
[GOAL]
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f (leastGE f r n)) σ x ∂μ ≤
    ∫ (x : Ω), stoppedValue (stoppedProcess f (leastGE f r n)) π x ∂μ
[PROOFSTEP]
refine' hf.expected_stoppedValue_mono _ _ _ fun ω => (min_le_left _ _).trans (hπ_le_n ω)
[GOAL]
case intro.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ IsStoppingTime ℱ fun x => min (σ x) (leastGE f r n x)
[PROOFSTEP]
exact hσ.min (hf.adapted.isStoppingTime_leastGE _ _)
[GOAL]
case intro.refine'_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ IsStoppingTime ℱ fun x => min (π x) (leastGE f r n x)
[PROOFSTEP]
exact hπ.min (hf.adapted.isStoppingTime_leastGE _ _)
[GOAL]
case intro.refine'_3
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ (fun x => min (σ x) (leastGE f r n x)) ≤ fun x => min (π x) (leastGE f r n x)
[PROOFSTEP]
exact fun ω => min_le_min (hσ_le_π ω) le_rfl
[GOAL]
case hadp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
⊢ Adapted ℱ fun i => stoppedValue f (leastGE f r i)
[PROOFSTEP]
exact fun i =>
  stronglyMeasurable_stoppedValue_of_le hf.adapted.progMeasurable_of_discrete (hf.adapted.isStoppingTime_leastGE _ _)
    leastGE_le
[GOAL]
case hint
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
⊢ ∀ (i : ℕ), Integrable (stoppedValue f (leastGE f r i))
[PROOFSTEP]
exact fun i => integrable_stoppedValue _ (hf.adapted.isStoppingTime_leastGE _ _) hf.integrable leastGE_le
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ ∀ᵐ (ω : Ω) ∂μ, stoppedValue f (leastGE f r i) ω ≤ r + ↑R
[PROOFSTEP]
filter_upwards [hbdd] with ω hbddω
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ stoppedValue f (leastGE f r i) ω ≤ r + ↑R
[PROOFSTEP]
change f (leastGE f r i ω) ω ≤ r + R
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ f (leastGE f r i ω) ω ≤ r + ↑R
[PROOFSTEP]
by_cases heq : leastGE f r i ω = 0
[GOAL]
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : leastGE f r i ω = 0
⊢ f (leastGE f r i ω) ω ≤ r + ↑R
[PROOFSTEP]
rw [heq, hf0, Pi.zero_apply]
[GOAL]
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : leastGE f r i ω = 0
⊢ 0 ≤ r + ↑R
[PROOFSTEP]
exact add_nonneg hr R.coe_nonneg
[GOAL]
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : ¬leastGE f r i ω = 0
⊢ f (leastGE f r i ω) ω ≤ r + ↑R
[PROOFSTEP]
obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero heq
[GOAL]
case neg.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : ¬leastGE f r i ω = 0
k : ℕ
hk : leastGE f r i ω = Nat.succ k
⊢ f (leastGE f r i ω) ω ≤ r + ↑R
[PROOFSTEP]
rw [hk, add_comm, ← sub_le_iff_le_add]
[GOAL]
case neg.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : ¬leastGE f r i ω = 0
k : ℕ
hk : leastGE f r i ω = Nat.succ k
⊢ f (Nat.succ k) ω - r ≤ ↑R
[PROOFSTEP]
have := not_mem_of_lt_hitting (hk.symm ▸ k.lt_succ_self : k < leastGE f r i ω) (zero_le _)
[GOAL]
case neg.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : ¬leastGE f r i ω = 0
k : ℕ
hk : leastGE f r i ω = Nat.succ k
this : ¬f k ω ∈ Set.Ici r
⊢ f (Nat.succ k) ω - r ≤ ↑R
[PROOFSTEP]
simp only [Set.mem_union, Set.mem_Iic, Set.mem_Ici, not_or, not_le] at this 
[GOAL]
case neg.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
heq : ¬leastGE f r i ω = 0
k : ℕ
hk : leastGE f r i ω = Nat.succ k
this : f k ω < r
⊢ f (Nat.succ k) ω - r ≤ ↑R
[PROOFSTEP]
exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ snorm (stoppedValue f (leastGE f r i)) 1 μ ≤ 2 * ↑↑μ Set.univ * ENNReal.ofReal (r + ↑R)
[PROOFSTEP]
refine' snorm_one_le_of_le' ((hf.stoppedValue_leastGE r).integrable _) _ (norm_stoppedValue_leastGE_le hr hf0 hbdd i)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (x : Ω), stoppedValue f (leastGE f r i) x ∂μ
[PROOFSTEP]
rw [← integral_univ]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (x : Ω) in Set.univ, stoppedValue f (leastGE f r i) x ∂μ
[PROOFSTEP]
refine' le_trans _ ((hf.stoppedValue_leastGE r).set_integral_le (zero_le _) MeasurableSet.univ)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (ω : Ω) in Set.univ, stoppedValue f (leastGE f r 0) ω ∂μ
[PROOFSTEP]
simp_rw [stoppedValue, leastGE, hitting_of_le le_rfl, hf0, integral_zero', le_rfl]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ snorm (stoppedValue f (leastGE f r i)) 1 μ ≤ ↑(ENNReal.toNNReal (2 * ↑↑μ Set.univ * ENNReal.ofReal (r + ↑R)))
[PROOFSTEP]
refine' (hf.stoppedValue_leastGE_snorm_le hr hf0 hbdd i).trans _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 2 * ↑↑μ Set.univ * ENNReal.ofReal (r + ↑R) ≤ ↑(ENNReal.toNNReal (2 * ↑↑μ Set.univ * ENNReal.ofReal (r + ↑R)))
[PROOFSTEP]
simp [ENNReal.coe_toNNReal (measure_ne_top μ _), ENNReal.coe_toNNReal]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
have ht : ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedValue f (leastGE f i n) ω) atTop (𝓝 c) :=
  by
  rw [ae_all_iff]
  exact fun i =>
    Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedValue_leastGE i)
      (hf.stoppedValue_leastGE_snorm_le' i.cast_nonneg hf0 hbdd)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
[PROOFSTEP]
rw [ae_all_iff]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) a) atTop (𝓝 c)
[PROOFSTEP]
exact fun i =>
  Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedValue_leastGE i)
    (hf.stoppedValue_leastGE_snorm_le' i.cast_nonneg hf0 hbdd)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
filter_upwards [ht] with ω hω hωb
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : BddAbove (Set.range fun n => f n ω)
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
rw [BddAbove] at hωb 
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
obtain ⟨i, hi⟩ := exists_nat_gt hωb.some
[GOAL]
case h.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
have hib : ∀ n, f n ω < i := by
  intro n
  exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
⊢ ∀ (n : ℕ), f n ω < ↑i
[PROOFSTEP]
intro n
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
n : ℕ
⊢ f n ω < ↑i
[PROOFSTEP]
exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
[GOAL]
case h.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
have heq : ∀ n, stoppedValue f (leastGE f i n) ω = f n ω :=
  by
  intro n
  rw [leastGE]; unfold hitting; rw [stoppedValue]
  rw [if_neg]
  simp only [Set.mem_Icc, Set.mem_union, Set.mem_Ici]
  push_neg
  exact fun j _ => hib j
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
⊢ ∀ (n : ℕ), stoppedValue f (leastGE f (↑i) n) ω = f n ω
[PROOFSTEP]
intro n
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ stoppedValue f (leastGE f (↑i) n) ω = f n ω
[PROOFSTEP]
rw [leastGE]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ stoppedValue f (hitting f (Set.Ici ↑i) 0 n) ω = f n ω
[PROOFSTEP]
unfold hitting
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ stoppedValue f
      (fun x =>
        if ∃ j, j ∈ Set.Icc 0 n ∧ f j x ∈ Set.Ici ↑i then sInf (Set.Icc 0 n ∩ {i_1 | f i_1 x ∈ Set.Ici ↑i}) else n)
      ω =
    f n ω
[PROOFSTEP]
rw [stoppedValue]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ f (if ∃ j, j ∈ Set.Icc 0 n ∧ f j ω ∈ Set.Ici ↑i then sInf (Set.Icc 0 n ∩ {i_1 | f i_1 ω ∈ Set.Ici ↑i}) else n) ω =
    f n ω
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ¬∃ j, j ∈ Set.Icc 0 n ∧ f j ω ∈ Set.Ici ↑i
[PROOFSTEP]
simp only [Set.mem_Icc, Set.mem_union, Set.mem_Ici]
[GOAL]
case hnc
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ¬∃ j, (0 ≤ j ∧ j ≤ n) ∧ ↑i ≤ f j ω
[PROOFSTEP]
push_neg
[GOAL]
case hnc
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ∀ (j : ℕ), 0 ≤ j ∧ j ≤ n → f j ω < ↑i
[PROOFSTEP]
exact fun j _ => hib j
[GOAL]
case h.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)
hωb : Set.Nonempty (upperBounds (Set.range fun n => f n ω))
i : ℕ
hi : Set.Nonempty.some hωb < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
heq : ∀ (n : ℕ), stoppedValue f (leastGE f (↑i) n) ω = f n ω
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
simp only [← heq, hω i]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
filter_upwards [hf.exists_tendsto_of_abs_bddAbove_aux hf0 hbdd] with ω hω using ⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
set g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
have hg : Submartingale g ℱ μ := hf.sub_martingale (martingale_const_fun _ _ (hf.adapted 0) (hf.integrable 0))
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
have hg0 : g 0 = 0 := by
  ext ω
  simp only [sub_self, Pi.zero_apply]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
⊢ g 0 = 0
[PROOFSTEP]
ext ω
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
ω : Ω
⊢ g 0 ω = OfNat.ofNat 0 ω
[PROOFSTEP]
simp only [sub_self, Pi.zero_apply]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by simpa only [sub_sub_sub_cancel_right]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
[PROOFSTEP]
simpa only [sub_sub_sub_cancel_right]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
filter_upwards [hg.bddAbove_iff_exists_tendsto_aux hg0 hgbdd] with ω hω
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
convert hω using 1
[GOAL]
case h.e'_1.a
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n => f n ω) ↔ BddAbove (Set.range fun n => f n ω - f 0 ω)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case h.e'_1.a.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
h : BddAbove (Set.range fun n => f n ω)
⊢ BddAbove (Set.range fun n => f n ω - f 0 ω)
[PROOFSTEP]
obtain ⟨b, hb⟩ := h
[GOAL]
case h.e'_1.a.refine'_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
h : BddAbove (Set.range fun n => f n ω - f 0 ω)
⊢ BddAbove (Set.range fun n => f n ω)
[PROOFSTEP]
obtain ⟨b, hb⟩ := h
[GOAL]
case h.e'_1.a.refine'_1.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω)
⊢ BddAbove (Set.range fun n => f n ω - f 0 ω)
[PROOFSTEP]
refine' ⟨b + |f 0 ω|, fun y hy => _⟩
[GOAL]
case h.e'_1.a.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω - f 0 ω)
⊢ BddAbove (Set.range fun n => f n ω)
[PROOFSTEP]
refine' ⟨b + |f 0 ω|, fun y hy => _⟩
[GOAL]
case h.e'_1.a.refine'_1.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω)
y : ℝ
hy : y ∈ Set.range fun n => f n ω - f 0 ω
⊢ y ≤ b + |f 0 ω|
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hy
[GOAL]
case h.e'_1.a.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω - f 0 ω)
y : ℝ
hy : y ∈ Set.range fun n => f n ω
⊢ y ≤ b + |f 0 ω|
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hy
[GOAL]
case h.e'_1.a.refine'_1.intro.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω)
n : ℕ
⊢ (fun n => f n ω - f 0 ω) n ≤ b + |f 0 ω|
[PROOFSTEP]
simp_rw [sub_eq_add_neg]
[GOAL]
case h.e'_1.a.refine'_1.intro.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω)
n : ℕ
⊢ f n ω + -f 0 ω ≤ b + |f 0 ω|
[PROOFSTEP]
exact add_le_add (hb ⟨n, rfl⟩) (neg_le_abs_self _)
[GOAL]
case h.e'_1.a.refine'_2.intro.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n => f n ω - f 0 ω)
n : ℕ
⊢ (fun n => f n ω) n ≤ b + |f 0 ω|
[PROOFSTEP]
exact sub_le_iff_le_add.1 (le_trans (sub_le_sub_left (le_abs_self _) _) (hb ⟨n, rfl⟩))
[GOAL]
case h.e'_2.a
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case h.e'_2.a.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
[PROOFSTEP]
obtain ⟨c, hc⟩ := h
[GOAL]
case h.e'_2.a.refine'_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
h : ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
obtain ⟨c, hc⟩ := h
[GOAL]
case h.e'_2.a.refine'_1.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
[PROOFSTEP]
exact ⟨c - f 0 ω, hc.sub_const _⟩
[GOAL]
case h.e'_2.a.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
refine' ⟨c + f 0 ω, _⟩
[GOAL]
case h.e'_2.a.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (c + f 0 ω))
[PROOFSTEP]
have := hc.add_const (f 0 ω)
[GOAL]
case h.e'_2.a.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n => f n ω - f 0 ω) ↔ ∃ c, Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => f n ω - f 0 ω) atTop (𝓝 c)
this : Tendsto (fun k => f k ω - f 0 ω + f 0 ω) atTop (𝓝 (c + f 0 ω))
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (c + f 0 ω))
[PROOFSTEP]
simpa only [sub_add_cancel]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
have hbdd' : ∀ᵐ ω ∂μ, ∀ i, |(-f) (i + 1) ω - (-f) i ω| ≤ R :=
  by
  filter_upwards [hbdd] with ω hω i
  erw [← abs_neg, neg_sub, sub_neg_eq_add, neg_add_eq_sub]
  exact hω i
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
[PROOFSTEP]
filter_upwards [hbdd] with ω hω i
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ω : Ω
hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
[PROOFSTEP]
erw [← abs_neg, neg_sub, sub_neg_eq_add, neg_add_eq_sub]
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ω : Ω
hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ |f (i + 1) ω - f i ω| ≤ ↑R
[PROOFSTEP]
exact hω i
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
have hup := hf.submartingale.bddAbove_iff_exists_tendsto hbdd
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
have hdown := hf.neg.submartingale.bddAbove_iff_exists_tendsto hbdd'
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
filter_upwards [hup, hdown] with ω hω₁ hω₂
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
have : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c) :=
  by
  constructor <;> rintro ⟨c, hc⟩
  · exact ⟨-c, hc.neg⟩
  · refine' ⟨-c, _⟩
    convert hc.neg
    simp only [neg_neg, Pi.neg_apply]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) → ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)) → ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case mp.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
[PROOFSTEP]
exact ⟨-c, hc.neg⟩
[GOAL]
case mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
[PROOFSTEP]
refine' ⟨-c, _⟩
[GOAL]
case mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (-c))
[PROOFSTEP]
convert hc.neg
[GOAL]
case h.e'_3.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
x✝ : ℕ
⊢ f x✝ ω = -(-f) x✝ ω
[PROOFSTEP]
simp only [neg_neg, Pi.neg_apply]
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
rw [hω₁, this, ← hω₂]
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n => (-f) n ω) ↔ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n => (-f) n ω) → BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ BddBelow (Set.range fun n => f n ω) → BddAbove (Set.range fun n => (-f) n ω)
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case h.mp.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : c ∈ upperBounds (Set.range fun n => (-f) n ω)
⊢ BddBelow (Set.range fun n => f n ω)
[PROOFSTEP]
refine' ⟨-c, fun ω hω => _⟩
[GOAL]
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : c ∈ lowerBounds (Set.range fun n => f n ω)
⊢ BddAbove (Set.range fun n => (-f) n ω)
[PROOFSTEP]
refine' ⟨-c, fun ω hω => _⟩
[GOAL]
case h.mp.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : c ∈ upperBounds (Set.range fun n => (-f) n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n => f n ω✝
⊢ -c ≤ ω
[PROOFSTEP]
rw [mem_upperBounds] at hc 
[GOAL]
case h.mp.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), (x ∈ Set.range fun n => (-f) n ω✝) → x ≤ c
ω : ℝ
hω : ω ∈ Set.range fun n => f n ω✝
⊢ -c ≤ ω
[PROOFSTEP]
refine' neg_le.2 (hc _ _)
[GOAL]
case h.mp.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), (x ∈ Set.range fun n => (-f) n ω✝) → x ≤ c
ω : ℝ
hω : ω ∈ Set.range fun n => f n ω✝
⊢ -ω ∈ Set.range fun n => (-f) n ω✝
[PROOFSTEP]
simpa only [Pi.neg_apply, Set.mem_range, neg_inj]
[GOAL]
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : c ∈ lowerBounds (Set.range fun n => f n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n => (-f) n ω✝
⊢ ω ≤ -c
[PROOFSTEP]
rw [mem_lowerBounds] at hc 
[GOAL]
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), (x ∈ Set.range fun n => f n ω✝) → c ≤ x
ω : ℝ
hω : ω ∈ Set.range fun n => (-f) n ω✝
⊢ ω ≤ -c
[PROOFSTEP]
simp_rw [Set.mem_range, Pi.neg_apply, neg_eq_iff_eq_neg] at hω 
[GOAL]
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), (x ∈ Set.range fun n => f n ω✝) → c ≤ x
ω : ℝ
hω : ∃ y, f y ω✝ = -ω
⊢ ω ≤ -c
[PROOFSTEP]
refine' le_neg.1 (hc _ _)
[GOAL]
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝¹ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), (x ∈ Set.range fun n => f n ω✝) → c ≤ x
ω : ℝ
hω : ∃ y, f y ω✝ = -ω
⊢ -ω ∈ Set.range fun n => f n ω✝
[PROOFSTEP]
simpa only [Set.mem_range]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => f n ω) atTop atTop
[PROOFSTEP]
filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
  unbounded_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => f n ω) atTop atBot
[PROOFSTEP]
filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
  unbounded_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s : ℕ → Set Ω
⊢ process s 0 = 0
[PROOFSTEP]
rw [process, Finset.range_zero, Finset.sum_empty]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ✝ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s✝ : ℕ → Set Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ martingalePart (process s) ℱ μ n =
    ∑ k in Finset.range n, (Set.indicator (s (k + 1)) 1 - μ[Set.indicator (s (k + 1)) 1|↑ℱ k])
[PROOFSTEP]
simp only [martingalePart_eq_sum, process_zero, zero_add]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ✝ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s✝ : ℕ → Set Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ ∑ i in Finset.range n, (process s (i + 1) - process s i - μ[process s (i + 1) - process s i|↑ℱ i]) =
    ∑ k in Finset.range n, (Set.indicator (s (k + 1)) 1 - μ[Set.indicator (s (k + 1)) 1|↑ℱ k])
[PROOFSTEP]
refine' Finset.sum_congr rfl fun k _ => _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ✝ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s✝ : ℕ → Set Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n k : ℕ
x✝ : k ∈ Finset.range n
⊢ process s (k + 1) - process s k - μ[process s (k + 1) - process s k|↑ℱ k] =
    Set.indicator (s (k + 1)) 1 - μ[Set.indicator (s (k + 1)) 1|↑ℱ k]
[PROOFSTEP]
simp only [process, Finset.sum_range_succ_sub_sum]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ✝ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s✝ : ℕ → Set Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ predictablePart (process s) ℱ μ n = ∑ k in Finset.range n, μ[Set.indicator (s (k + 1)) 1|↑ℱ k]
[PROOFSTEP]
have := martingalePart_process_ae_eq ℱ μ s n
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ✝ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s✝ : ℕ → Set Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  martingalePart (process s) ℱ μ n =
    ∑ k in Finset.range n, (Set.indicator (s (k + 1)) 1 - μ[Set.indicator (s (k + 1)) 1|↑ℱ k])
⊢ predictablePart (process s) ℱ μ n = ∑ k in Finset.range n, μ[Set.indicator (s (k + 1)) 1|↑ℱ k]
[PROOFSTEP]
simp_rw [martingalePart, process, Finset.sum_sub_distrib] at this 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ✝ : Measure Ω
ℱ✝ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
s✝ : ℕ → Set Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 - predictablePart (process s) ℱ μ n =
    ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 - ∑ x in Finset.range n, μ[Set.indicator (s (x + 1)) 1|↑ℱ x]
⊢ predictablePart (process s) ℱ μ n = ∑ k in Finset.range n, μ[Set.indicator (s (k + 1)) 1|↑ℱ k]
[PROOFSTEP]
exact sub_right_injective this
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
s✝ s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ ↑1
[PROOFSTEP]
norm_cast
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
s✝ s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ 1
[PROOFSTEP]
rw [process, process, Finset.sum_apply, Finset.sum_apply, Finset.sum_range_succ_sub_sum, ← Real.norm_eq_abs,
  norm_indicator_eq_indicator_norm]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
s✝ s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ Set.indicator (s (n + 1)) (fun a => ‖OfNat.ofNat 1 a‖) ω ≤ 1
[PROOFSTEP]
refine' Set.indicator_le' (fun _ _ => _) (fun _ _ => zero_le_one) _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
s✝ s : ℕ → Set Ω
ω : Ω
n : ℕ
x✝¹ : Ω
x✝ : x✝¹ ∈ s (n + 1)
⊢ ‖OfNat.ofNat 1 x✝¹‖ ≤ 1
[PROOFSTEP]
rw [Pi.one_apply, norm_one]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
have h₁ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atTop (martingalePart_bdd_difference ℱ hbdd)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
have h₂ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atBot (martingalePart_bdd_difference ℱ hbdd)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
have h₃ : ∀ᵐ ω ∂μ, ∀ n, 0 ≤ (μ[f (n + 1) - f n|ℱ n]) ω :=
  by
  refine' ae_all_iff.2 fun n => condexp_nonneg _
  filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
[PROOFSTEP]
refine' ae_all_iff.2 fun n => condexp_nonneg _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
n : ℕ
⊢ 0 ≤ᵐ[μ] f (n + 1) - f n
[PROOFSTEP]
filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
filter_upwards [h₁, h₂, h₃, hfmono] with ω hω₁ hω₂ hω₃ hω₄
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
⊢ Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
constructor
[GOAL]
case h.mp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
⊢ Tendsto (fun n => f n ω) atTop atTop → Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
intro ht
[GOAL]
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
⊢ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop → Tendsto (fun n => f n ω) atTop atTop
[PROOFSTEP]
intro ht
[GOAL]
case h.mp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
⊢ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
[PROOFSTEP]
refine' tendsto_atTop_atTop_of_monotone' _ _
[GOAL]
case h.mp.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
⊢ Monotone fun n => predictablePart f ℱ μ n ω
[PROOFSTEP]
intro n m hnm
[GOAL]
case h.mp.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
⊢ (fun n => predictablePart f ℱ μ n ω) n ≤ (fun n => predictablePart f ℱ μ n ω) m
[PROOFSTEP]
simp only [predictablePart, Finset.sum_apply]
[GOAL]
case h.mp.refine'_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
⊢ ∑ c in Finset.range n, (μ[f (c + 1) - f c|↑ℱ c]) ω ≤ ∑ c in Finset.range m, (μ[f (c + 1) - f c|↑ℱ c]) ω
[PROOFSTEP]
refine' Finset.sum_mono_set_of_nonneg hω₃ (Finset.range_mono hnm)
[GOAL]
case h.mp.refine'_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
⊢ ¬BddAbove (Set.range fun n => predictablePart f ℱ μ n ω)
[PROOFSTEP]
rintro ⟨b, hbdd⟩
[GOAL]
case h.mp.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n => predictablePart f ℱ μ n ω)
⊢ False
[PROOFSTEP]
rw [← tendsto_neg_atBot_iff] at ht 
[GOAL]
case h.mp.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun x => -f x ω) atTop atBot
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n => predictablePart f ℱ μ n ω)
⊢ False
[PROOFSTEP]
simp only [martingalePart, sub_eq_add_neg] at hω₁ 
[GOAL]
case h.mp.refine'_2.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun x => -f x ω) atTop atBot
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n => predictablePart f ℱ μ n ω)
hω₁ : ¬Tendsto (fun n => (f n + -predictablePart f ℱ μ n) ω) atTop atTop
⊢ False
[PROOFSTEP]
exact hω₁ (tendsto_atTop_add_right_of_le _ (-b) (tendsto_neg_atBot_iff.1 ht) fun n => neg_le_neg (hbdd ⟨n, rfl⟩))
[GOAL]
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
⊢ Tendsto (fun n => f n ω) atTop atTop
[PROOFSTEP]
refine' tendsto_atTop_atTop_of_monotone' (monotone_nat_of_le_succ hω₄) _
[GOAL]
case h.mpr
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
⊢ ¬BddAbove (Set.range fun n => f n ω)
[PROOFSTEP]
rintro ⟨b, hbdd⟩
[GOAL]
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n)
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n => f n ω)
⊢ False
[PROOFSTEP]
exact hω₂ ((tendsto_atBot_add_left_of_ge _ b fun n => hbdd ⟨n, rfl⟩) <| tendsto_neg_atBot_iff.2 ht)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑ℱ k]) ω) atTop atTop
[PROOFSTEP]
have :=
  tendsto_sum_indicator_atTop_iff (eventually_of_forall fun ω n => ?_) (adapted_process hs) (integrable_process μ hs)
    (eventually_of_forall <| process_difference_le s)
[GOAL]
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => process (fun n => s n) n ω) atTop atTop ↔
      Tendsto (fun n => predictablePart (process fun n => s n) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑ℱ k]) ω) atTop atTop
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process (fun n => s n) n ω ≤ process (fun n => s n) (n + 1) ω
[PROOFSTEP]
swap
[GOAL]
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process (fun n => s n) n ω ≤ process (fun n => s n) (n + 1) ω
[PROOFSTEP]
rw [process, process, ← sub_nonneg, Finset.sum_apply, Finset.sum_apply, Finset.sum_range_succ_sub_sum]
[GOAL]
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω✝ : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ 0 ≤ Set.indicator (s (n + 1)) 1 ω
[PROOFSTEP]
exact Set.indicator_nonneg (fun _ _ => zero_le_one) _
[GOAL]
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => process (fun n => s n) n ω) atTop atTop ↔
      Tendsto (fun n => predictablePart (process fun n => s n) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑ℱ k]) ω) atTop atTop
[PROOFSTEP]
simp_rw [process, predictablePart_process_ae_eq] at this 
[GOAL]
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => Finset.sum (Finset.range n) (fun k => Set.indicator (s (k + 1)) 1) ω) atTop atTop ↔
      Tendsto (fun n => Finset.sum (Finset.range n) (fun k => μ[Set.indicator (s (k + 1)) 1|↑ℱ k]) ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
      Tendsto (fun n => ∑ k in Finset.range n, (μ[Set.indicator (s (k + 1)) 1|↑ℱ k]) ω) atTop atTop
[PROOFSTEP]
simpa using this
