[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


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a'✝ a' : α
⊢ a' ∈ support (pure a) ↔ a' ∈ {a}
[PROOFSTEP]
simp [mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
⊢ a' ∈ support (pure a) ↔ a' = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
⊢ ↑(toOuterMeasure (pure a)) s = if a ∈ s then 1 else 0
[PROOFSTEP]
refine' (toOuterMeasure_apply (pure a) s).trans _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
⊢ ∑' (x : α), Set.indicator s (↑(pure a)) x = if a ∈ s then 1 else 0
[PROOFSTEP]
split_ifs with ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), Set.indicator s (↑(pure a)) x = 1
[PROOFSTEP]
refine' (tsum_congr fun b => _).trans (tsum_ite_eq a 1)
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = if b = a then 1 else 0
[PROOFSTEP]
exact ite_eq_left_iff.2 fun hb => symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : ¬a ∈ s
⊢ ∑' (x : α), Set.indicator s (↑(pure a)) x = 0
[PROOFSTEP]
refine' (tsum_congr fun b => _).trans tsum_zero
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : ¬a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = 0
[PROOFSTEP]
exact ite_eq_right_iff.2 fun hb => ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (pure a)) s = ↑↑(Measure.dirac a) s
[PROOFSTEP]
rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = Set.indicator s 1 a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ Measure.toPmf (Measure.dirac a) = pure a
[PROOFSTEP]
rw [toPmf_eq_iff_toMeasure_eq, toMeasure_pure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
⊢ ∑' (b : α) (a : β), ↑p b * ↑(f b) a = 1
[PROOFSTEP]
simp only [ENNReal.tsum_mul_left, tsum_coe, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : β
⊢ b ∈ support (bind p f) ↔ b ∈ ⋃ (a : α) (_ : a ∈ support p), support (f a)
[PROOFSTEP]
simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : β
⊢ b ∈ support (bind p f) ↔ ∃ a, a ∈ support p ∧ b ∈ support (f a)
[PROOFSTEP]
simp only [support_bind, Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
⊢ bind (pure a) f = f a
[PROOFSTEP]
have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by split_ifs with h <;> simp; subst h;
  simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
⊢ (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : a' = a
⊢ ↑(f a') b = ↑(f a) b
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : ¬a' = a
⊢ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : a' = a
⊢ ↑(f a') b = ↑(f a) b
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
f : α → Pmf β
b : β
a' : α
⊢ ↑(f a') b = ↑(f a') b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
⊢ bind (pure a) f = f a
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
b : β
⊢ ↑(bind (pure a) f) b = ↑(f a) b
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
x y : α
hy : y ≠ x
⊢ ↑p y * ↑(pure y) x = 0
[PROOFSTEP]
rw [pure_apply_of_ne _ _ hy.symm, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
x : α
⊢ ↑p x * ↑(pure x) x = ↑p x
[PROOFSTEP]
rw [pure_apply_self, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f : α → Pmf β
g : β → Pmf γ
p : Pmf α
q : Pmf β
x : β
⊢ ↑(bind p fun x => q) x = ↑q x
[PROOFSTEP]
rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : γ
⊢ ↑(bind (bind p f) g) b = ↑(bind p fun a => bind (f a) g) b
[PROOFSTEP]
simpa only [ENNReal.coe_eq_coe.symm, bind_apply, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm, mul_assoc,
  mul_left_comm, mul_comm] using ENNReal.tsum_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
p : Pmf α
q : Pmf β
f : α → β → Pmf γ
b : γ
⊢ ↑(bind p fun a => bind q (f a)) b = ↑(bind q fun b => bind p fun a => f a b) b
[PROOFSTEP]
simpa only [ENNReal.coe_eq_coe.symm, bind_apply, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm, mul_assoc,
  mul_left_comm, mul_comm] using ENNReal.tsum_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
⊢ ↑(toOuterMeasure (bind p f)) s = ∑' (b : β), if b ∈ s then ∑' (a : α), ↑p a * ↑(f a) b else 0
[PROOFSTEP]
simp [toOuterMeasure_apply, Set.indicator_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), ↑p a * ↑(f a) b else 0) = ∑' (a : α), ↑p a * if b ∈ s then ↑(f a) b else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
h✝ : b ∈ s
⊢ ∑' (a : α), ↑p a * ↑(f a) b = ∑' (a : α), ↑p a * ↑(f a) b
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
h✝ : ¬b ∈ s
⊢ 0 = ∑' (a : α), ↑p a * 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
⊢ (if b ∈ s then ↑(f a) b else 0) = if b ∈ s then ↑(f a) b else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
h✝ : b ∈ s
⊢ ↑(f a) b = ↑(f a) b
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
h✝ : ¬b ∈ s
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
⊢ (↑p a * ∑' (b : β), if b ∈ s then ↑(f a) b else 0) = ↑p a * ↑(toOuterMeasure (f a)) s
[PROOFSTEP]
simp only [toOuterMeasure_apply, Set.indicator_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
⊢ (∑' (b : β) (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 1
[PROOFSTEP]
refine' ENNReal.tsum_comm.trans (_root_.trans (tsum_congr fun a => _) p.tsum_coe)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
⊢ (∑' (a_1 : β), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = ↑p a
[PROOFSTEP]
simp_rw [ENNReal.tsum_mul_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
⊢ (↑p a * ∑' (i : β), if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) i) = ↑p a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
h : ↑p a = 0
⊢ ↑p a * ∑' (i : β), 0 = ↑p a
[PROOFSTEP]
simp only [h, zero_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
h : ¬↑p a = 0
⊢ ↑p a * ∑' (i : β), ↑(f a (_ : ¬↑p a = 0)) i = ↑p a
[PROOFSTEP]
rw [(f a h).tsum_coe, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
⊢ support (bindOnSupport p f) = ⋃ (a : α) (h : a ∈ support p), support (f a h)
[PROOFSTEP]
refine' Set.ext fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ b ∈ ⋃ (a : α) (h : a ∈ support p), support (f a h)
[PROOFSTEP]
simp only [ENNReal.tsum_eq_zero, not_or, mem_support_iff, bindOnSupport_apply, Ne.def, not_forall, mul_eq_zero,
  Set.mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0) ↔
    ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
[PROOFSTEP]
exact
  ⟨fun hb =>
    let ⟨a, ⟨ha, ha'⟩⟩ := hb
    ⟨a, ha, by simpa [ha] using ha'⟩,
    fun hb =>
    let ⟨a, ha, ha'⟩ := hb
    ⟨a, ⟨ha, by simpa [(mem_support_iff _ a).1 ha] using ha'⟩⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
hb : ∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0
a : α
ha : ¬↑p a = 0
ha' : ¬(if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) b) = 0
⊢ ¬↑(f a (_ : a ∈ support p)) b = 0
[PROOFSTEP]
simpa [ha] using ha'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
hb : ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
a : α
ha : ¬↑p a = 0
ha' : ¬↑(f a (_ : a ∈ support p)) b = 0
⊢ ¬(if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) b) = 0
[PROOFSTEP]
simpa [(mem_support_iff _ a).1 ha] using ha'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ ∃ a h, b ∈ support (f a h)
[PROOFSTEP]
simp only [support_bindOnSupport, Set.mem_setOf_eq, Set.mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
⊢ (bindOnSupport p fun a x => f a) = bind p f
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
[PROOFSTEP]
have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b := fun a =>
  ite_eq_right_iff.2 fun h => h.symm ▸ symm (zero_mul <| f a b)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
this : ∀ (a : α), (if ↑p a = 0 then 0 else ↑p a * ↑(f a) b) = ↑p a * ↑(f a) b
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
[PROOFSTEP]
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite, mul_zero, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ ↑(bindOnSupport p f) b = 0 ↔ ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
[PROOFSTEP]
simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∀ (i : α), ¬↑p i = 0 → (if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0)) b) = 0) ↔
    ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
[PROOFSTEP]
exact ⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha), fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
⊢ bindOnSupport (pure a) f = f a (_ : a ∈ support (pure a))
[PROOFSTEP]
refine' Pmf.ext fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ ↑(bindOnSupport (pure a) f) b = ↑(f a (_ : a ∈ support (pure a))) b
[PROOFSTEP]
simp only [bindOnSupport_apply, pure_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ (∑' (a_1 : α),
      (if a_1 = a then 1 else 0) *
        if h : (if a_1 = a then 1 else 0) = 0 then 0 else ↑(f a_1 (_ : ¬↑(pure a) a_1 = 0)) b) =
    ↑(f a (_ : a ∈ support (pure a))) b
[PROOFSTEP]
refine' _root_.trans (tsum_congr fun a' => _) (tsum_ite_eq a _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
[PROOFSTEP]
by_cases h : a' = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
h : a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
h : ¬a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
⊢ (bindOnSupport p fun a x => pure a) = p
[PROOFSTEP]
simp only [Pmf.bind_pure, Pmf.bindOnSupport_eq_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
⊢ bindOnSupport (bindOnSupport p f) g =
    bindOnSupport p fun a ha => bindOnSupport (f a ha) fun b hb => g b (_ : b ∈ support (bindOnSupport p f))
[PROOFSTEP]
refine' Pmf.ext fun a => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ ↑(bindOnSupport (bindOnSupport p f) g) a =
    ↑(bindOnSupport p fun a ha => bindOnSupport (f a ha) fun b hb => g b (_ : b ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
dsimp only [bindOnSupport_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ (∑' (a_1 : β),
      (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) *
        if h : (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = 0 then 0 else ↑(g a_1 h) a) =
    ∑' (a_1 : α),
      ↑p a_1 *
        if h : ↑p a_1 = 0 then 0
        else
          ∑' (a_2 : β),
            ↑(f a_1 h) a_2 * if h : ↑(f a_1 h) a_2 = 0 then 0 else ↑(g a_2 (_ : a_2 ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
simp only [← tsum_dite_right, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) a_1) *
        if h : (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = 0 then 0 else ↑(g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      ↑p a_1 *
        if h : ↑p a_1 = 0 then 0
        else ↑(f a_1 h) i * if h : ↑(f a_1 h) i = 0 then 0 else ↑(g i (_ : i ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
simp only [ENNReal.tsum_eq_zero, dite_eq_left_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) a_1) *
        if h : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) a_1) = 0 then 0
        else ↑(g a_1 (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = 0)) a) =
    ∑' (a_1 : α) (i : β),
      ↑p a_1 *
        if h : ↑p a_1 = 0 then 0
        else ↑(f a_1 h) i * if h : ↑(f a_1 h) i = 0 then 0 else ↑(g i (_ : i ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
refine' ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
⊢ ((↑p a' * if h : ↑p a' = 0 then 0 else ↑(f a' h) b) *
      if h : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0 then 0
      else ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a) =
    ↑p a' *
      if h : ↑p a' = 0 then 0
      else ↑(f a' h) b * if h : ↑(f a' h) b = 0 then 0 else ↑(g b (_ : b ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
split_ifs with h _ h_1 _ h_2
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * 0 = ↑p a' * 0
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a = ↑p a' * 0
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * 0)
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * 0)
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
any_goals ring1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * 0 = ↑p a' * 0
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a = ↑p a' * 0
[PROOFSTEP]
ring1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * 0)
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
ring1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * 0)
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
have := h_1 a'
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
this : (↑p a' * if h : ↑p a' = 0 then 0 else ↑(f a' h) b) = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
simp [h] at this
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
this : ↑(f a' (_ : ¬↑p a' = 0)) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
contradiction
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * 0)
[PROOFSTEP]
simp [h_2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ (bindOnSupport p fun a ha => bindOnSupport q (f a ha)) =
    bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb
[PROOFSTEP]
apply Pmf.ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ ∀ (x : γ),
    ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) x =
      ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) x
[PROOFSTEP]
rintro c
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) c =
    ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) c
[PROOFSTEP]
simp only [ENNReal.coe_eq_coe.symm, bindOnSupport_apply, ← tsum_dite_right, ENNReal.tsum_mul_left.symm,
  ENNReal.tsum_mul_right.symm]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ (∑' (a : α) (i : β),
      ↑p a *
        if h : ↑p a = 0 then 0 else ↑q i * if h : ↑q i = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) i (_ : ¬↑q i = 0)) c) =
    ∑' (a : β) (i : α),
      ↑q a * if h : ↑q a = 0 then 0 else ↑p i * if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0) a (_ : ¬↑q a = 0)) c
[PROOFSTEP]
refine' _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => _)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
⊢ (↑p a * if h : ↑p a = 0 then 0 else ↑q b * if h : ↑q b = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c) =
    ↑q b * if h : ↑q b = 0 then 0 else ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c
[PROOFSTEP]
split_ifs with h1 h2 h2
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ↑p a = 0
h2 : ↑q b = 0
⊢ ↑p a * 0 = ↑q b * 0
[PROOFSTEP]
ring
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ↑p a = 0
h2 : ¬↑q b = 0
⊢ ↑p a * 0 = ↑q b * (↑p a * 0)
[PROOFSTEP]
ring
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ¬↑p a = 0
h2 : ↑q b = 0
⊢ ↑p a * (↑q b * 0) = ↑q b * 0
[PROOFSTEP]
ring
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ¬↑p a = 0
h2 : ¬↑q b = 0
⊢ ↑p a * (↑q b * ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c) =
    ↑q b * (↑p a * ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ ↑(toOuterMeasure (bindOnSupport p f)) s = ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(toOuterMeasure (f a h)) s
[PROOFSTEP]
simp only [toOuterMeasure_apply, Set.indicator_apply, bindOnSupport_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ (∑' (x : β), if x ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) x else 0) =
    ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ∑' (x : β), if x ∈ s then ↑(f a (_ : ¬↑p a = 0)) x else 0
[PROOFSTEP]
calc
  (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
      ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    tsum_congr fun b => by split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]
  _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 := ENNReal.tsum_comm
  _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
  _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
    tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ∑' (a : α), if b ∈ s then ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0
[PROOFSTEP]
split_ifs with hbs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
hbs : b ∈ s
⊢ (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) =
    ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b
[PROOFSTEP]
simp only [eq_self_iff_true, tsum_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
hbs : ¬b ∈ s
⊢ 0 = ∑' (a : α), 0
[PROOFSTEP]
simp only [eq_self_iff_true, tsum_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
⊢ (∑' (b : β), if b ∈ s then ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ↑p a * ∑' (b : β), if b ∈ s then if h : ↑p a = 0 then 0 else ↑(f a h) b else 0
[PROOFSTEP]
simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
⊢ (↑p a * ∑' (b : β), if b ∈ s then if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ↑p a * if h : ↑p a = 0 then 0 else ∑' (b : β), if b ∈ s then ↑(f a h) b else 0
[PROOFSTEP]
split_ifs with ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
ha : ↑p a = 0
⊢ (↑p a * ∑' (b : β), if b ∈ s then 0 else 0) = ↑p a * 0
[PROOFSTEP]
simp only [ite_self, tsum_zero, eq_self_iff_true]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
ha : ¬↑p a = 0
⊢ (↑p a * ∑' (b : β), if b ∈ s then ↑(f a ha) b else 0) = ↑p a * ∑' (b : β), if b ∈ s then ↑(f a ha) b else 0
[PROOFSTEP]
simp only [ite_self, tsum_zero, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
inst✝ : MeasurableSpace β
hs : MeasurableSet s
⊢ ↑↑(toMeasure (bindOnSupport p f)) s = ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑↑(toMeasure (f a h)) s
[PROOFSTEP]
simp only [toMeasure_apply_eq_toOuterMeasure_apply _ _ hs, toOuterMeasure_bindOnSupport_apply]