awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 τ | ⋯.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
have refine_1 : ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x},
  μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Tactic: refine ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
refine_1 :
  ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
have refine_2 : ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x}ᶜ,
  μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Tactic: refine ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
this :
  μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
have rw : ∀ᵐ (x : Ω) ∂μ,
  Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
    μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Tactic: rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
this :
  μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
⊢ ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
have rw : ∀
  (this :
    ∀ᵐ (x : Ω) ∂μ,
      Membership.mem (γ := Set Ω) {x : Ω | τ x ≤ σ x} x →
        μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x),
  ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
this :
  μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
rw :
  ∀
    (this :
      ∀ᵐ (x : Ω) ∂μ,
        Membership.mem (γ := Set Ω) {x : Ω | τ x ≤ σ x} x →
          μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x),
    ∀ᵐ (x : Ω) ∂μ,
      Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
        μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
have rw₁ : ∀
  (this :
    ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | τ x ≤ σ x},
      μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x),
  MeasurableSet.{u_1} (α := Ω) {x : Ω | τ x ≤ σ x}
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {x : Ω | τ x ≤ σ x} x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
have h₁ : ∀ (x : Ω) (hx : τ x ≤ σ x → μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x)
  (hx_mem : Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x),
  μ[stoppedValue f τ | sorry.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Tactic: filter_upwards [this] with x hx hx_mem
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {x : Ω | τ x ≤ σ x} x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
x : Ω
hx : τ x ≤ σ x → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
hx_mem : Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
have hx_mem₁ : τ x < σ x
Tactic: simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx_mem
Cleared hypotheses: hx_mem
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
have refine_2 : μ[stoppedValue f τ | sorry.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[stoppedValue f τ | hσ.measurableSpace]
Tactic: suffices μ[stoppedValue f τ | (hσ.min hτ).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
        μ[stoppedValue f τ | hσ.measurableSpace] by
      rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]
      rw [Filter.EventuallyEq, ae_restrict_iff'] at this
      swap; · exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
      filter_upwards [this] with x hx hx_mem
      simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx_mem
      exact hx hx_mem.le
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
have apply : Ω → E
Tactic: apply Filter.EventuallyEq.trans _ ((condExp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
apply : Ω → E
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
have apply₁ : μ[stoppedValue f τ | sorry.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[stoppedValue f τ | sorry.measurableSpace]
Tactic: apply Filter.EventuallyEq.trans _ ((condExp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
apply : Ω → E
apply₁ :
  μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
have apply₂ : μ[stoppedValue f τ | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
  μ[stoppedValue f τ | hσ.measurableSpace]
Tactic: apply Filter.EventuallyEq.trans _ ((condExp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
have rw : μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
  μ[stoppedValue f τ | sorry.measurableSpace]
Tactic: rw [IsStoppingTime.measurableSpace_min hσ hτ,
        IsStoppingTime.measurableSpace_min hτ hσ, inf_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
rw :
  μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
have rw₁ : μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
  μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace]
Tactic: rw [IsStoppingTime.measurableSpace_min hσ hτ,
        IsStoppingTime.measurableSpace_min hτ hσ, inf_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
rw :
  μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
rw₁ :
  μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace]
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
have rw₂ : μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
  μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace]
Tactic: rw [IsStoppingTime.measurableSpace_min hσ hτ,
        IsStoppingTime.measurableSpace_min hτ hσ, inf_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 τ
have hf : StronglyMeasurable (stoppedValue f τ)
Tactic: apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ⋯)
hf : StronglyMeasurable (stoppedValue f τ)
⊢ μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
have hfi : Integrable (stoppedValue f τ) μ
Tactic: apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
have h1 : μ[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
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 τ | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
have rw : stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[stoppedValue f τ | hσ.measurableSpace]
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
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 : ℕ∞)
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
have 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 ∂μ)
Tactic: rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]