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 ⋯)
⊢ (stoppedValue f fun (x : Ω) ↦ min (σ x) (τ x)) =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
(h.stoppedValue_ae_eq_condExp_of_le hτ (hσ.min hτ) (fun x => min_le_right _ _) hτ_le).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.IsStoppingTime.min, min_le_right, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_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 ⋯)
hτ₁ : μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]
⊢ (stoppedValue f fun (x : Ω) ↦ min (σ x) (τ x)) =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
refine
    (h.stoppedValue_ae_eq_condExp_of_le hτ (hσ.min hτ) (fun x => min_le_right _ _) hτ_le).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.IsStoppingTime.min, min_le_right, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_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 ⋯)
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} ?_ ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, setOf, Filter.EventuallyEq, LE.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 ⋯)
refine_1 :
  ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
refine_2 :
  ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} ?_ ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, setOf, LE.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 ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
condExp_min_stopping_time_ae_eq_restrict_le hσ hτ

Premises used: Filter.EventuallyEq, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_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 ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
exact condExp_min_stopping_time_ae_eq_restrict_le hσ hτ

Premises used: MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_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 ⋯)
this :
  μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
rw :
  ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.IsStoppingTime.measurableSpace_le, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- 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 ⋯)
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
rw₁ :
  ∀
    (this :
      ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | τ x ≤ σ x},
        μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x),
    MeasurableSet.{u_1} (α := Ω) {x : Ω | τ x ≤ σ x}
⊢ ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff'] at this

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- 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 ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | τ x ≤ σ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ MeasurableSet.{u_1} (α := Ω) {x : Ω | τ x ≤ σ x}

Tactic:
hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.IsStoppingTime.measurableSpace_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 ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ.restrict {x : Ω | τ x ≤ σ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ MeasurableSet.{u_1} (α := Ω) {x : Ω | τ x ≤ σ x}

Tactic:
exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.IsStoppingTime.measurableSpace_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 ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {x : Ω | τ x ≤ σ x} x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
h₁ :
  ∀ (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
⊢ ∀ᵐ (x : Ω) ∂μ,
    Membership.mem (γ := Set Ω) {ω : Ω | σ ω ≤ τ ω}ᶜ x →
      μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
filter_upwards [this] with x hx hx_mem
-- 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 ⋯)
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
⊢ τ x < σ x

Tactic:
simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx_mem

Premises used: not_le, Set.mem_setOf_eq, Set.mem_compl_iff
-- 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 ⋯)
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 : τ x < σ x
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
hx hx_mem.le

Premises used: LT.lt.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 ⋯)
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 : τ x < σ x
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
exact hx hx_mem.le

Premises used: LT.lt.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 ⋯)
refine_2 :
  μ[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

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
-- 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 ⋯)
apply : Ω → E
apply₁ :
  μ[stoppedValue f τ | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | ⋯.measurableSpace]
apply₂ :
  μ[stoppedValue f τ | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})]
    μ[stoppedValue f τ | hσ.measurableSpace]
⊢ μ[stoppedValue f τ | ⋯.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 _)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_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 ⋯)
⊢ Ω → E

Tactic:
exact stoppedValue f τ

Premises used: MeasureTheory.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 ⋯)
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]
rw₂ 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]

Tactic:
rw [IsStoppingTime.measurableSpace_min hσ hτ,
        IsStoppingTime.measurableSpace_min hτ hσ, inf_comm]

Premises used: inf_comm, MeasureTheory.IsStoppingTime.measurableSpace_min
-- 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 ⋯)
hf : StronglyMeasurable (stoppedValue f τ)
hfi : Integrable (stoppedValue f τ) μ
⊢ μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ

Tactic:
apply condExp_of_stronglyMeasurable hτ.measurableSpace_le

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.IsStoppingTime.measurableSpace_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 ⋯)
⊢ StronglyMeasurable (stoppedValue f τ)

Tactic:
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