-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Submartingale.stoppedValue_leastGE [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (r : ℝ) :
    Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ

Proof state:
Ω : 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 ∂μ

Tactic:
obtain ⟨n, hπ_le_n⟩ := hπ_bdd

Result:
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 ∂μ

Proof state:
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)) μ

Tactic:
exact fun i => integrable_stoppedValue _ (hf.adapted.isStoppingTime_leastGE _ _) hf.integrable
  leastGE_le

Result:
no goals

Proof state:
Ω : 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 ∂μ

Tactic:
intro σ π hσ hπ hσ_le_π hπ_bdd

Result:
Ω : 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 ∂μ

Proof state:
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 => σ x ⊓ leastGE f r n x) ≤ fun x => π x ⊓ leastGE f r n x

Tactic:
exact fun ω => min_le_min (hσ_le_π ω) le_rfl

Result:
no goals

Proof state:
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)

Tactic:
exact fun i => stronglyMeasurable_stoppedValue_of_le hf.adapted.progMeasurable_of_discrete
  (hf.adapted.isStoppingTime_leastGE _ _) leastGE_le

Result:
no goals

Proof state:
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 ∂μ

Tactic:
simp_rw [stoppedValue_stoppedValue_leastGE f σ r fun i => (hσ_le_π i).trans (hπ_le_n i)]

Result:
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 ∂μ

Proof state:
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 => σ x ⊓ leastGE f r n x

Tactic:
exact hσ.min (hf.adapted.isStoppingTime_leastGE _ _)

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
⊢ Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ

Tactic:
rw [submartingale_iff_expected_stoppedValue_mono]

Result:
Ω : 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 ∂μ

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)

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)) μ

Proof state:
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 => π x ⊓ leastGE f r n x

Tactic:
exact hπ.min (hf.adapted.isStoppingTime_leastGE _ _)

Result:
no goals

Proof state:
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 ∂μ

Tactic:
refine hf.expected_stoppedValue_mono ?_ ?_ ?_ fun ω => (min_le_left _ _).trans (hπ_le_n ω)

Result:
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 => σ x ⊓ leastGE f r n x

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 => π x ⊓ leastGE f r n x

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 => σ x ⊓ leastGE f r n x) ≤ fun x => π x ⊓ leastGE f r n x