[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
inst✝¹ : Filter.IsCountablyGenerated Filter.atTop
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
hin : i ≤ n
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] f i
[PROOFSTEP]
refine' Filter.EventuallyEq.trans _ (ae_restrict_of_ae (h.condexp_ae_eq hin))
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
inst✝¹ : Filter.IsCountablyGenerated Filter.atTop
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
hin : i ≤ n
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] fun x => (μ[f n|↑ℱ i]) x
[PROOFSTEP]
refine'
  condexp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i) (hτ.measurableSet_eq' i) fun t => _
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
inst✝¹ : Filter.IsCountablyGenerated Filter.atTop
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
hin : i ≤ n
t : Set Ω
⊢ MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)
[PROOFSTEP]
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] f i
[PROOFSTEP]
by_cases hin : i ≤ n
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : i ≤ n
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] f i
[PROOFSTEP]
refine' Filter.EventuallyEq.trans _ (ae_restrict_of_ae (h.condexp_ae_eq hin))
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : i ≤ n
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] fun x => (μ[f n|↑ℱ i]) x
[PROOFSTEP]
refine'
  condexp_ae_eq_restrict_of_measurableSpace_eq_on (hτ.measurableSpace_le_of_le hτ_le) (ℱ.le i) (hτ.measurableSet_eq' i)
    fun t => _
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : i ≤ n
t : Set Ω
⊢ MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)
[PROOFSTEP]
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : ¬i ≤ n
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] f i
[PROOFSTEP]
suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : ¬i ≤ n
this : {x | τ x = i} = ∅
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x = i}] f i
[PROOFSTEP]
simp [this]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : ¬i ≤ n
this : {x | τ x = i} = ∅
⊢ μ[f n|IsStoppingTime.measurableSpace hτ] =ᶠ[⊥] f i
[PROOFSTEP]
norm_cast
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : ¬i ≤ n
⊢ {x | τ x = i} = ∅
[PROOFSTEP]
ext1 x
[GOAL]
case neg.h
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : ¬i ≤ n
x : Ω
⊢ x ∈ {x | τ x = i} ↔ x ∈ ∅
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false_iff]
[GOAL]
case neg.h
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
hin : ¬i ≤ n
x : Ω
⊢ ¬τ x = i
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.h
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
x : Ω
hin : ¬τ x ≤ n
⊢ False
[PROOFSTEP]
exact hin (hτ_le x)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
⊢ stoppedValue f τ =ᵐ[Measure.restrict μ {x | τ x = i}] μ[f n|IsStoppingTime.measurableSpace hτ]
[PROOFSTEP]
refine' Filter.EventuallyEq.trans _ (condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
⊢ stoppedValue f τ =ᵐ[Measure.restrict μ {x | τ x = i}] f i
[PROOFSTEP]
rw [Filter.EventuallyEq, ae_restrict_iff' (ℱ.le _ _ (hτ.measurableSet_eq i))]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ {ω | τ ω = i} → stoppedValue f τ x = f i x
[PROOFSTEP]
refine' Filter.eventually_of_forall fun x hx => _
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
x : Ω
hx : x ∈ {ω | τ ω = i}
⊢ stoppedValue f τ x = f i x
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hx 
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i✝ n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
i : ι
x : Ω
hx : τ x = i
⊢ stoppedValue f τ x = f i x
[PROOFSTEP]
simp_rw [stoppedValue, hx]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
h_countable_range : Set.Countable (Set.range τ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
⊢ stoppedValue f τ =ᵐ[μ] μ[f n|IsStoppingTime.measurableSpace hτ]
[PROOFSTEP]
have : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i} := by
  ext1 x
  simp only [Set.mem_univ, Set.mem_range, true_and_iff, Set.iUnion_exists, Set.iUnion_iUnion_eq', Set.mem_iUnion,
    Set.mem_setOf_eq, exists_apply_eq_apply']
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
h_countable_range : Set.Countable (Set.range τ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
⊢ Set.univ = ⋃ (i : ι) (_ : i ∈ Set.range τ), {x | τ x = i}
[PROOFSTEP]
ext1 x
[GOAL]
case h
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
h_countable_range : Set.Countable (Set.range τ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
x : Ω
⊢ x ∈ Set.univ ↔ x ∈ ⋃ (i : ι) (_ : i ∈ Set.range τ), {x | τ x = i}
[PROOFSTEP]
simp only [Set.mem_univ, Set.mem_range, true_and_iff, Set.iUnion_exists, Set.iUnion_iUnion_eq', Set.mem_iUnion,
  Set.mem_setOf_eq, exists_apply_eq_apply']
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
h_countable_range : Set.Countable (Set.range τ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
this : Set.univ = ⋃ (i : ι) (_ : i ∈ Set.range τ), {x | τ x = i}
⊢ stoppedValue f τ =ᵐ[μ] μ[f n|IsStoppingTime.measurableSpace hτ]
[PROOFSTEP]
nth_rw 1 [← @Measure.restrict_univ Ω _ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
h_countable_range : Set.Countable (Set.range τ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
this : Set.univ = ⋃ (i : ι) (_ : i ∈ Set.range τ), {x | τ x = i}
⊢ stoppedValue f τ =ᵐ[Measure.restrict μ Set.univ] μ[f n|IsStoppingTime.measurableSpace hτ]
[PROOFSTEP]
rw [this, ae_eq_restrict_biUnion_iff _ h_countable_range]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
h_countable_range : Set.Countable (Set.range τ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
this : Set.univ = ⋃ (i : ι) (_ : i ∈ Set.range τ), {x | τ x = i}
⊢ ∀ (i : ι),
    i ∈ Set.range τ → stoppedValue f τ =ᵐ[Measure.restrict μ {x | τ x = i}] μ[f n|IsStoppingTime.measurableSpace hτ]
[PROOFSTEP]
exact fun i _ => stoppedValue_ae_eq_restrict_eq h _ hτ_le i
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : Set.Countable (Set.range τ)
hσ_countable_range : Set.Countable (Set.range σ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
⊢ stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
have : SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
  sigmaFiniteTrim_mono _ (IsStoppingTime.measurableSpace_mono hσ hτ hσ_le_τ)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : Set.Countable (Set.range τ)
hσ_countable_range : Set.Countable (Set.range σ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
this : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
⊢ stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
have : μ[stoppedValue f τ|hσ.measurableSpace] =ᵐ[μ] μ[μ[f n|hτ.measurableSpace]|hσ.measurableSpace] :=
  condexp_congr_ae (h.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range hτ hτ_le hτ_countable_range)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : Set.Countable (Set.range τ)
hσ_countable_range : Set.Countable (Set.range σ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
this✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
this :
  μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ] =ᵐ[μ]
    μ[μ[f n|IsStoppingTime.measurableSpace hτ]|IsStoppingTime.measurableSpace hσ]
⊢ stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
refine' (Filter.EventuallyEq.trans _ (condexp_condexp_of_le _ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : Set.Countable (Set.range τ)
hσ_countable_range : Set.Countable (Set.range σ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
this✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
this :
  μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ] =ᵐ[μ]
    μ[μ[f n|IsStoppingTime.measurableSpace hτ]|IsStoppingTime.measurableSpace hσ]
⊢ stoppedValue f σ =ᵐ[μ] μ[f n|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
exact
  h.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range hσ (fun x => (hσ_le_τ x).trans (hτ_le x))
    hσ_countable_range
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : Set.Countable (Set.range τ)
hσ_countable_range : Set.Countable (Set.range σ)
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
this✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hτ ≤ m))
this :
  μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ] =ᵐ[μ]
    μ[μ[f n|IsStoppingTime.measurableSpace hτ]|IsStoppingTime.measurableSpace hσ]
⊢ IsStoppingTime.measurableSpace hσ ≤ IsStoppingTime.measurableSpace hτ
[PROOFSTEP]
exact hσ.measurableSpace_mono hτ hσ_le_τ
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
⊢ μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}] stoppedValue f τ
[PROOFSTEP]
rw [ae_eq_restrict_iff_indicator_ae_eq (hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ))]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
⊢ Set.indicator {ω | τ ω ≤ σ ω} (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) =ᵐ[μ]
    Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue f τ)
[PROOFSTEP]
refine'
  (condexp_indicator (integrable_stoppedValue ι hτ h.integrable hτ_le)
        (hτ.measurableSet_stopping_time_le hσ)).symm.trans
    _
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
⊢ μ[Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ)|IsStoppingTime.measurableSpace hσ] =ᵐ[μ]
    Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue f τ)
[PROOFSTEP]
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σ)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
⊢ Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
[PROOFSTEP]
refine' (integrable_stoppedValue ι hτ h.integrable hτ_le).indicator _
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
⊢ MeasurableSet {ω | τ ω ≤ σ ω}
[PROOFSTEP]
exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ μ[Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ)|IsStoppingTime.measurableSpace hσ] =ᵐ[μ]
    Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue f τ)
[PROOFSTEP]
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.adapted.progMeasurable_of_discrete hτ
  · intro x hx
    simp only [hx, Set.indicator_of_not_mem, not_false_iff]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ AEStronglyMeasurable' (IsStoppingTime.measurableSpace hσ)
    (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ)) μ
[PROOFSTEP]
refine' StronglyMeasurable.aeStronglyMeasurable' _
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ StronglyMeasurable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
[PROOFSTEP]
refine' StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on (hτ.measurableSet_le_stopping_time hσ) _ _ _
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ ∀ (t : Set Ω), MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t) → MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)
[PROOFSTEP]
intro t ht
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
t : Set Ω
ht : MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)
⊢ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)
[PROOFSTEP]
rw [Set.inter_comm _ t] at ht ⊢
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
t : Set Ω
ht : MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
[PROOFSTEP]
rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht 
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
t : Set Ω
ht : MeasurableSet (t ∩ {ω | τ ω ≤ σ ω}) ∧ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
[PROOFSTEP]
exact ht.2
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ StronglyMeasurable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
[PROOFSTEP]
refine' StronglyMeasurable.indicator _ (hτ.measurableSet_le_stopping_time hσ)
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ StronglyMeasurable (stoppedValue (fun n => f n) τ)
[PROOFSTEP]
refine' Measurable.stronglyMeasurable _
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ Measurable (stoppedValue (fun n => f n) τ)
[PROOFSTEP]
exact measurable_stoppedValue h.adapted.progMeasurable_of_discrete hτ
[GOAL]
case refine'_3
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
⊢ ∀ (x : Ω), ¬x ∈ {ω | τ ω ≤ σ ω} → Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ) x = 0
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_3
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
x : Ω
hx : ¬x ∈ {ω | τ ω ≤ σ ω}
⊢ Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ) x = 0
[PROOFSTEP]
simp only [hx, Set.indicator_of_not_mem, not_false_iff]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace hσ ≤ m))
hτ_le : ∀ (x : Ω), τ x ≤ n
h_int : Integrable (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ))
h_meas :
  AEStronglyMeasurable' (IsStoppingTime.measurableSpace hσ)
    (Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ)) μ
⊢ μ[Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue (fun n => f n) τ)|IsStoppingTime.measurableSpace hσ] =ᵐ[μ]
    Set.indicator {ω | τ ω ≤ σ ω} (stoppedValue f τ)
[PROOFSTEP]
exact condexp_of_aestronglyMeasurable' hσ.measurableSpace_le h_meas h_int
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ (stoppedValue f fun x => min (σ x) (τ x)) =ᵐ[μ] μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
refine' (h.stoppedValue_ae_eq_condexp_of_le hτ (hσ.min hτ) (fun x => min_le_right _ _) hτ_le).trans _
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))] =ᵐ[μ]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
refine' ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} _ _
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ ∀ᵐ (x : Ω) ∂Measure.restrict μ {x | σ x ≤ τ x},
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
exact condexp_min_stopping_time_ae_eq_restrict_le hσ hτ
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ ∀ᵐ (x : Ω) ∂Measure.restrict μ {x | σ x ≤ τ x}ᶜ,
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
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
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  μ[stoppedValue f
        τ|IsStoppingTime.measurableSpace
        (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
⊢ ∀ᵐ (x : Ω) ∂Measure.restrict μ {x | σ x ≤ τ x}ᶜ,
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  μ[stoppedValue f
        τ|IsStoppingTime.measurableSpace
        (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ {ω | σ ω ≤ τ ω}ᶜ →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
rw [Filter.EventuallyEq, ae_restrict_iff'] at this 
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ {ω | σ ω ≤ τ ω}ᶜ →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  ∀ᵐ (x : Ω) ∂Measure.restrict μ {x | τ x ≤ σ x},
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
⊢ MeasurableSet {x | τ x ≤ σ x}
[PROOFSTEP]
swap
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  ∀ᵐ (x : Ω) ∂Measure.restrict μ {x | τ x ≤ σ x},
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
⊢ MeasurableSet {x | τ x ≤ σ x}
[PROOFSTEP]
exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ {ω | σ ω ≤ τ ω}ᶜ →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
filter_upwards [this] with x hx hx_mem
[GOAL]
case h
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
x : Ω
hx :
  τ x ≤ σ x →
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
hx_mem : x ∈ {ω | σ ω ≤ τ ω}ᶜ
⊢ (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx_mem 
[GOAL]
case h
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} →
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
        (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
x : Ω
hx :
  τ x ≤ σ x →
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
      (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
hx_mem : τ x < σ x
⊢ (μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))]) x =
    (μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]) x
[PROOFSTEP]
exact hx hx_mem.le
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ μ[stoppedValue f
        τ|IsStoppingTime.measurableSpace
        (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
apply Filter.EventuallyEq.trans _ ((condexp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _)
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ Ω → E
[PROOFSTEP]
exact stoppedValue f τ
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ μ[stoppedValue f
        τ|IsStoppingTime.measurableSpace
        (_ : IsStoppingTime ℱ fun ω => min (σ ω) (τ ω))] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω))]
[PROOFSTEP]
rw [IsStoppingTime.measurableSpace_min hσ, IsStoppingTime.measurableSpace_min hτ, inf_comm]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ μ[stoppedValue f τ|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
have h1 : μ[stoppedValue f τ|hτ.measurableSpace] = stoppedValue f τ :=
  by
  refine' condexp_of_stronglyMeasurable hτ.measurableSpace_le _ _
  · refine' Measurable.stronglyMeasurable _
    exact measurable_stoppedValue h.adapted.progMeasurable_of_discrete hτ
  · exact integrable_stoppedValue ι hτ h.integrable hτ_le
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ μ[stoppedValue f τ|IsStoppingTime.measurableSpace hτ] = stoppedValue f τ
[PROOFSTEP]
refine' condexp_of_stronglyMeasurable hτ.measurableSpace_le _ _
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ StronglyMeasurable (stoppedValue f τ)
[PROOFSTEP]
refine' Measurable.stronglyMeasurable _
[GOAL]
case refine'_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ Measurable (stoppedValue f τ)
[PROOFSTEP]
exact measurable_stoppedValue h.adapted.progMeasurable_of_discrete hτ
[GOAL]
case refine'_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
⊢ Integrable (stoppedValue f τ)
[PROOFSTEP]
exact integrable_stoppedValue ι hτ h.integrable hτ_le
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
h1 : μ[stoppedValue f τ|IsStoppingTime.measurableSpace hτ] = stoppedValue f τ
⊢ μ[stoppedValue f τ|IsStoppingTime.measurableSpace hτ] =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}]
    μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
rw [h1]
[GOAL]
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → ι
f : ι → Ω → E
i n✝ : ι
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ n
h_sf_min :
  SigmaFinite (Measure.trim μ (_ : IsStoppingTime.measurableSpace (_ : IsStoppingTime ℱ fun ω => min (τ ω) (σ ω)) ≤ m))
h1 : μ[stoppedValue f τ|IsStoppingTime.measurableSpace hτ] = stoppedValue f τ
⊢ stoppedValue f τ =ᵐ[Measure.restrict μ {x | τ x ≤ σ x}] μ[stoppedValue f τ|IsStoppingTime.measurableSpace hσ]
[PROOFSTEP]
exact (condexp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm
