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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ σ ω}

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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ σ ω}

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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
⊢ Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ

Tactic:
have h_int :
      Integrable ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ := by
    refine (integrable_stoppedValue ι hτ h.integrable hτ_le).indicator ?_
    exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ

Tactic:
StronglyMeasurable.aestronglyMeasurable ?_

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
refine : StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ

Tactic:
refine StronglyMeasurable.aestronglyMeasurable ?_

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))

Tactic:
StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_

Premises used: MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
refine_1 : ∀ (t : Set Ω), MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t) → MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
refine_2 :
  StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))
refine_3 :
  ∀ x ∉ {ω : Ω | τ ω ≤ σ ω},
    Eq.{u_2 + 1} (α := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ) x) 0
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))

Tactic:
refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_

Premises used: MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)
refine_1 : ∀ (ht : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})), MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet ({ω : Ω | τ ω ≤ σ ω} ∩ t)

Tactic:
rw [Set.inter_comm _ t] at ht ⊢

Premises used: Set.inter_comm
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ∧ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})

Tactic:
rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht

Premises used: MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, MeasureTheory.IsStoppingTime.measurableSet_min_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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ∧ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})

Tactic:
ht.2

Premises used: And.right
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω}) ∧ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ σ ω})

Tactic:
exact ht.2

Premises used: And.right
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))

Tactic:
StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.StronglyMeasurable.indicator
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
refine_2 : StronglyMeasurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ))

Tactic:
refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.StronglyMeasurable.indicator
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)

Tactic:
Measurable.stronglyMeasurable ?_

Premises used: Measurable.stronglyMeasurable
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
refine_2 : Measurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)
⊢ StronglyMeasurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)

Tactic:
refine Measurable.stronglyMeasurable ?_

Premises used: Measurable.stronglyMeasurable
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ Measurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)

Tactic:
measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ

Premises used: MeasureTheory.Martingale.stronglyAdapted, 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ Measurable.{u_1, u_2} (β := E) (stoppedValue (fun (n : ι) ↦ f n) τ)

Tactic:
exact measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ

Premises used: MeasureTheory.Martingale.stronglyAdapted, 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
x : Ω
hx : x ∉ {ω : Ω | τ ω ≤ σ ω}
⊢ Eq.{u_2 + 1} (α := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ) x) 0

Tactic:
simp only [hx, Set.indicator_of_notMem, not_false_iff]

Premises used: Set.indicator_of_notMem, not_false_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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ

Tactic:
have h_meas : AEStronglyMeasurable[hσ.measurableSpace]
      ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ := by
    refine StronglyMeasurable.aestronglyMeasurable ?_
    refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
    · intro t ht
      rw [Set.inter_comm _ t] at ht ⊢
      rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht
      exact ht.2
    · refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)
      refine Measurable.stronglyMeasurable ?_
      exact measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
    · intro x hx
      simp only [hx, Set.indicator_of_notMem, not_false_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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
h_meas :
  AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ μ[Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ) | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)

Tactic:
condExp_of_aestronglyMeasurable' hσ.measurableSpace_le h_meas h_int

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.condExp_of_aestronglyMeasurable'
-- 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst_13 : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ (↑i : WithTop ι)
h_int : Integrable.{u_2, u_1} (ε := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
h_meas :
  AEStronglyMeasurable.{u_1, u_2} (β := E) (Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue (fun (n : ι) ↦ f n) τ)) μ
⊢ μ[Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ) | hσ.measurableSpace] =ᶠ[ae μ]
    Set.indicator {ω : Ω | τ ω ≤ σ ω} (stoppedValue f τ)

Tactic:
exact condExp_of_aestronglyMeasurable' hσ.measurableSpace_le h_meas h_int

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.condExp_of_aestronglyMeasurable'