awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ StronglyMeasurable (stoppedValue f τ)

Tactic:
exact Measurable.stronglyMeasurable <|
            measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ

Premises used: MeasureTheory.Martingale.stronglyAdapted, Measurable.stronglyMeasurable, MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete, MeasureTheory.measurable_stoppedValue
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ Integrable (stoppedValue f τ) μ

Tactic:
integrable_stoppedValue ι hτ h.integrable hτ_le

Premises used: MeasureTheory.integrable_stoppedValue, MeasureTheory.Martingale.integrable
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ Integrable (stoppedValue f τ) μ

Tactic:
exact integrable_stoppedValue ι hτ h.integrable hτ_le

Premises used: MeasureTheory.integrable_stoppedValue, MeasureTheory.Martingale.integrable
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ

Tactic:
have h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ := by
        apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
        · exact Measurable.stronglyMeasurable <|
            measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
        · exact integrable_stoppedValue ι hτ h.integrable hτ_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
rw : stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[stoppedValue f τ | hσ.measurableSpace]
⊢ μ[stoppedValue f τ | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
rw [h1]
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
(condExp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm

Premises used: MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : TopologicalSpace ι
inst_7 : DiscreteTopology ι
inst_8 : MeasurableSpace ι
inst_9 : BorelSpace ι
inst_10 : MeasurableSpace E
inst_11 : BorelSpace E
inst_12 : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst_13 : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_sf_min : SigmaFinite (μ.trim ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
exact (condExp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm

Premises used: MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
rw :
  LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      (fun (ω : Ω) ↦
          ((∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) ω :
            E))
        a ∂μ)
hf₁ : Integrable (stoppedValue f π) μ
hg : Integrable (stoppedValue f τ) μ
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)

Tactic:
rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]

Premises used: MeasureTheory.stoppedValue_sub_eq_sum', MeasureTheory.integral_sub', sub_nonneg
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
simp :
  LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      ∑ c ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} (f (c + 1) - f c) a ∂μ)
⊢ LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      (fun (ω : Ω) ↦
          ((∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) ω :
            E))
        a ∂μ)

Tactic:
simp only [Finset.sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}

Tactic:
(hτ i).inter ?_

Premises used: Set.Mem, setOf, Set.inter, MeasurableSet.inter
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
refine : MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}

Tactic:
refine (hτ i).inter ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ

Tactic:
(hπ i).compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
h : Eq.{u_1 + 1} (α := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)

Tactic:
convert! (hπ i).compl using 1

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔
      Membership.mem (γ := Set Ω) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ x
⊢ Eq.{u_1 + 1} (α := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ

Tactic:
ext x
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
x : Ω
h : Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔ (↑i : WithTop ℕ) < π x
⊢ Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔
    Membership.mem (γ := Set Ω) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ x

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
x : Ω
⊢ Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔ (↑i : WithTop ℕ) < π x

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}

Tactic:
have : ∀ i, MeasurableSet[𝒢 i] {ω : Ω | τ ω ≤ i ∧ i < π ω} := by
      intro i
      refine (hτ i).inter ?_
      convert! (hπ i).compl using 1
      ext x
      simp; rfl
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
rw :
  LE.le.{u_2} (α := E) 0
    (∑ i ∈ Finset.range (N + 1),
      ∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
hf₁ :
  ∀ i ∈ Finset.range (N + 1), Integrable (Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) μ
⊢ LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      ∑ c ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} (f (c + 1) - f c) a ∂μ)

Tactic:
rw [integral_finsetSum]

Premises used: MeasureTheory.integral_finsetSum
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
⊢ LE.le.{u_2} (α := E) 0
    (∑ i ∈ Finset.range (N + 1),
      ∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)

Tactic:
Finset.sum_nonneg fun i _ => ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
refine :
  ∀ i ∈ Finset.range (N + 1),
    LE.le.{u_2} (α := E) 0 (∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
⊢ LE.le.{u_2} (α := E) 0
    (∑ i ∈ Finset.range (N + 1),
      ∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)

Tactic:
refine Finset.sum_nonneg fun i _ => ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
rw :
  LE.le.{u_2} (α := E) (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f i a ∂μ)
    (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f (i + 1) a ∂μ)
hf₁ : Integrable (f (i + 1)) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})
hg : Integrable (f i) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)

Tactic:
rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.integral_sub', MeasureTheory.Filtration.le, sub_nonneg
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ LE.le.{u_2} (α := E) (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f i a ∂μ)
    (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f (i + 1) a ∂μ)

Tactic:
hf.setIntegral_le (Nat.le_succ i) (this _)

Premises used: MeasureTheory.Submartingale.setIntegral_le, Nat.le_succ
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ LE.le.{u_2} (α := E) (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f i a ∂μ)
    (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f (i + 1) a ∂μ)

Tactic:
exact hf.setIntegral_le (Nat.le_succ i) (this _)

Premises used: MeasureTheory.Submartingale.setIntegral_le, Nat.le_succ
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ Integrable (f (i + 1)) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})

Tactic:
(hf.integrable _).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.IntegrableOn, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ Integrable (f (i + 1)) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})

Tactic:
exact (hf.integrable _).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ Integrable (f i) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})

Tactic:
(hf.integrable _).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.IntegrableOn, MeasureTheory.Integrable.integrableOn