ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>p.toOuterMeasure.caratheodory = ⊤
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Finset α<GOAL>p.toOuterMeasure ↑s = ∑ x ∈ s, p x
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>p.toOuterMeasure {a} = p a
<VAR>α : Type u_1<GOAL>Function.Injective PMF.toOuterMeasure
<VAR>α : Type u_1<VAR>p q : PMF α<GOAL>p.toOuterMeasure = q.toOuterMeasure ↔ p = q
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<GOAL>p.toOuterMeasure s = 0 ↔ Disjoint p.support s
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<GOAL>p.toOuterMeasure s = 1 ↔ p.support ⊆ s
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<GOAL>p.toOuterMeasure (s ∩ p.support) = p.toOuterMeasure s
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s t : Set α<VAR>h : s ∩ p.support ⊆ t<GOAL>p.toOuterMeasure s ≤ p.toOuterMeasure t
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s t : Set α<VAR>h : s ∩ p.support = t ∩ p.support<GOAL>p.toOuterMeasure s = p.toOuterMeasure t
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>Fintype α<GOAL>p.toOuterMeasure s = ∑ x : α, s.indicator (⇑p) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<GOAL>p.toOuterMeasure s ≤ p.toMeasure s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>p.toMeasure s = p.toOuterMeasure s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>p.toMeasure s = ∑' (x : α), s.indicator (⇑p) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>a : α<VAR>h : MeasurableSet {a}<GOAL>p.toMeasure {a} = p a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>p.toMeasure s = 0 ↔ Disjoint p.support s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>p.toMeasure s = 1 ↔ p.support ⊆ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hp : MeasurableSet p.support<GOAL>p.toMeasure (s ∩ p.support) = p.toMeasure s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>p : PMF α<GOAL>p.toMeasure.restrict p.support = p.toMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : s ∩ p.support ⊆ t<GOAL>p.toMeasure s ≤ p.toMeasure t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : s ∩ p.support = t ∩ p.support<GOAL>p.toMeasure s = p.toMeasure t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<GOAL>Function.Injective PMF.toMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>p q : PMF α<GOAL>p.toMeasure = q.toMeasure ↔ p = q
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>MeasurableSingletonClass α<VAR>s : Finset α<GOAL>p.toMeasure ↑s = ∑ x ∈ s, p x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>MeasurableSingletonClass α<VAR>hs : s.Finite<GOAL>p.toMeasure s = ∑' (x : α), s.indicator (⇑p) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : PMF α<VAR>s : Set α<VAR>MeasurableSingletonClass α<VAR>Fintype α<GOAL>p.toMeasure s = ∑ x : α, s.indicator (⇑p) x
<VAR>α : Type u_1<VAR>Countable α<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>x : α<GOAL>μ.toPMF x = μ {x}
<VAR>α : Type u_1<VAR>Countable α<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>μ.toPMF.toMeasure = μ
<VAR>α : Type u_1<VAR>Countable α<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>p : PMF α<GOAL>p.toMeasure.toPMF = p
<VAR>α : Type u_1<VAR>Countable α<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>p : PMF α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>p.toMeasure = μ ↔ p = μ.toPMF
<VAR>α : Type u_1<VAR>Countable α<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>p : PMF α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>μ.toPMF = p ↔ μ = p.toMeasure
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>p : ℕ<VAR>μ : MeasureTheory.Measure Ω<VAR>hp : p ≠ 0<GOAL>ProbabilityTheory.moment 0 p μ = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>p : ℕ<VAR>μ : MeasureTheory.Measure Ω<VAR>hp : p ≠ 0<GOAL>ProbabilityTheory.centralMoment 0 p μ = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_int : MeasureTheory.Integrable X μ<GOAL>ProbabilityTheory.centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.centralMoment X 1 μ = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hX : MeasureTheory.Memℒp X 2 μ<GOAL>ProbabilityTheory.centralMoment X 2 μ = ProbabilityTheory.variance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<GOAL>ProbabilityTheory.mgf 0 μ t = (μ Set.univ).toReal
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<GOAL>ProbabilityTheory.cgf 0 μ t = Real.log (μ Set.univ).toReal
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>t : ℝ<GOAL>ProbabilityTheory.mgf X 0 t = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>t : ℝ<GOAL>ProbabilityTheory.cgf X 0 t = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>c : ℝ<GOAL>ProbabilityTheory.mgf (fun x => c) μ t = (μ Set.univ).toReal * rexp (t * c)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>c : ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.mgf (fun x => c) μ t = rexp (t * c)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>c : ℝ<GOAL>ProbabilityTheory.cgf (fun x => c) μ t = Real.log (μ Set.univ).toReal + t * c
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>c : ℝ<GOAL>ProbabilityTheory.cgf (fun x => c) μ t = t * c
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.mgf X μ 0 = (μ Set.univ).toReal
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.mgf X μ 0 = 1
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.cgf X μ 0 = Real.log (μ Set.univ).toReal
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.cgf X μ 0 = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>hX : ¬MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>ProbabilityTheory.mgf X μ t = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>hX : ¬MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>ProbabilityTheory.cgf X μ t = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<GOAL>0 ≤ ProbabilityTheory.mgf X μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>hμ : μ ≠ 0<VAR>h_int_X : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>0 < ProbabilityTheory.mgf X μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_int_X : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>0 < ProbabilityTheory.mgf X μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<GOAL>ProbabilityTheory.mgf (-X) μ t = ProbabilityTheory.mgf X μ (-t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<GOAL>ProbabilityTheory.cgf (-X) μ t = ProbabilityTheory.cgf X μ (-t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>X Y : Ω → ℝ<VAR>h_indep : ProbabilityTheory.IndepFun X Y μ<VAR>s t : ℝ<GOAL>ProbabilityTheory.IndepFun (fun ω => rexp (s * X ω)) (fun ω => rexp (t * Y ω)) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : ProbabilityTheory.IndepFun X Y μ<VAR>hX : MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ<VAR>hY : MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ<GOAL>ProbabilityTheory.mgf (X + Y) μ t = ProbabilityTheory.mgf X μ t * ProbabilityTheory.mgf Y μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : ProbabilityTheory.IndepFun X Y μ<VAR>hX : MeasureTheory.AEStronglyMeasurable X μ<VAR>hY : MeasureTheory.AEStronglyMeasurable Y μ<GOAL>ProbabilityTheory.mgf (X + Y) μ t = ProbabilityTheory.mgf X μ t * ProbabilityTheory.mgf Y μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : ProbabilityTheory.IndepFun X Y μ<VAR>h_int_X : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<VAR>h_int_Y : MeasureTheory.Integrable (fun ω => rexp (t * Y ω)) μ<GOAL>ProbabilityTheory.cgf (X + Y) μ t = ProbabilityTheory.cgf X μ t + ProbabilityTheory.cgf Y μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_int_X : MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ<VAR>h_int_Y : MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * (X + Y) ω)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>X : ι → Ω → ℝ<VAR>s : Finset ι<VAR>h_int : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : ProbabilityTheory.IndepFun X Y μ<VAR>h_int_X : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<VAR>h_int_Y : MeasureTheory.Integrable (fun ω => rexp (t * Y ω)) μ<GOAL>MeasureTheory.Integrable (fun ω => rexp (t * (X + Y) ω)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>X : ι → Ω → ℝ<VAR>h_indep : ProbabilityTheory.iIndepFun (fun i => inferInstance) X μ<VAR>h_meas : ∀ (i : ι), Measurable (X i)<VAR>s : Finset ι<VAR>h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun ω => rexp (t * X i ω)) μ<GOAL>MeasureTheory.Integrable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>X : ι → Ω → ℝ<VAR>h_indep : ProbabilityTheory.iIndepFun (fun i => inferInstance) X μ<VAR>h_meas : ∀ (i : ι), Measurable (X i)<VAR>s : Finset ι<GOAL>ProbabilityTheory.mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, ProbabilityTheory.mgf (X i) μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>X : ι → Ω → ℝ<VAR>h_indep : ProbabilityTheory.iIndepFun (fun i => inferInstance) X μ<VAR>h_meas : ∀ (i : ι), Measurable (X i)<VAR>s : Finset ι<VAR>h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun ω => rexp (t * X i ω)) μ<GOAL>ProbabilityTheory.cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, ProbabilityTheory.cgf (X i) μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : 0 ≤ t<VAR>h_int : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * ProbabilityTheory.mgf X μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | X ω ≤ ε}).toReal ≤ rexp (-t * ε) * ProbabilityTheory.mgf X μ t
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : 0 ≤ t<VAR>h_int : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε + ProbabilityTheory.cgf X μ t)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>t : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : MeasureTheory.Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | X ω ≤ ε}).toReal ≤ rexp (-t * ε + ProbabilityTheory.cgf X μ t)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>ProbabilityTheory.condCount ∅ = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>s : Set Ω<GOAL>(ProbabilityTheory.condCount s) ∅ = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>s t : Set Ω<VAR>h : (ProbabilityTheory.condCount s) t ≠ 0<GOAL>s.Finite
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>Fintype Ω<VAR>s : Set Ω<GOAL>(ProbabilityTheory.condCount Set.univ) s = MeasureTheory.Measure.count s / ↑(Fintype.card Ω)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.condCount s)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>ω : Ω<VAR>t : Set Ω<VAR>Decidable (ω ∈ t)<GOAL>(ProbabilityTheory.condCount {ω}) t = if ω ∈ t then 1 else 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t : Set Ω<VAR>hs : s.Finite<GOAL>(ProbabilityTheory.condCount s) (s ∩ t) = (ProbabilityTheory.condCount s) t
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>(ProbabilityTheory.condCount s) s = 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<VAR>ht : s ⊆ t<GOAL>(ProbabilityTheory.condCount s) t = 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t : Set Ω<VAR>h : (ProbabilityTheory.condCount s) t = 1<GOAL>s ⊆ t
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t : Set Ω<VAR>hs : s.Finite<GOAL>(ProbabilityTheory.condCount s) t = 0 ↔ s ∩ t = ∅
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>(ProbabilityTheory.condCount s) Set.univ = 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<GOAL>(ProbabilityTheory.condCount s) (t ∩ u) = (ProbabilityTheory.condCount (s ∩ t)) u * (ProbabilityTheory.condCount s) t
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<GOAL>(ProbabilityTheory.condCount s) (t ∩ u) = (ProbabilityTheory.condCount (s ∩ u)) t * (ProbabilityTheory.condCount s) u
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>htu : Disjoint t u<GOAL>(ProbabilityTheory.condCount s) (t ∪ u) = (ProbabilityTheory.condCount s) t + (ProbabilityTheory.condCount s) u
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>t : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>(ProbabilityTheory.condCount s) t + (ProbabilityTheory.condCount s) tᶜ = 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<GOAL>(ProbabilityTheory.condCount s) u * (ProbabilityTheory.condCount (s ∪ t)) s + (ProbabilityTheory.condCount t) u * (ProbabilityTheory.condCount (s ∪ t)) t = (ProbabilityTheory.condCount (s ∪ t)) u
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>u t : Set Ω<VAR>hs : s.Finite<GOAL>(ProbabilityTheory.condCount (s ∩ u)) t * (ProbabilityTheory.condCount s) u + (ProbabilityTheory.condCount (s ∩ uᶜ)) t * (ProbabilityTheory.condCount s) uᶜ = (ProbabilityTheory.condCount s) t
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<GOAL>MeasureTheory.predictablePart f ℱ μ 0 = 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<GOAL>MeasureTheory.Adapted ℱ fun n => MeasureTheory.predictablePart f ℱ μ (n + 1)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<GOAL>MeasureTheory.Adapted ℱ fun n => MeasureTheory.predictablePart f ℱ μ n
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ℕ → Ω → E<GOAL>MeasureTheory.martingalePart f ℱ μ + MeasureTheory.predictablePart f ℱ μ = f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<GOAL>MeasureTheory.martingalePart f ℱ μ = fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<GOAL>MeasureTheory.Adapted ℱ (MeasureTheory.martingalePart f ℱ μ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf_int : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>n : ℕ<GOAL>MeasureTheory.Integrable (MeasureTheory.martingalePart f ℱ μ n) μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<GOAL>MeasureTheory.Martingale (MeasureTheory.martingalePart f ℱ μ) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hg : MeasureTheory.Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ<VAR>n : ℕ<GOAL>MeasureTheory.martingalePart (f + g) ℱ μ n =ᵐ[μ] f n
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hg : MeasureTheory.Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ<VAR>n : ℕ<GOAL>MeasureTheory.predictablePart (f + g) ℱ μ n =ᵐ[μ] g n
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>R : ℝ≥0<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |MeasureTheory.predictablePart f ℱ μ (i + 1) ω - MeasureTheory.predictablePart f ℱ μ i ω| ≤ ↑R
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>R : ℝ≥0<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |MeasureTheory.martingalePart f ℱ μ (i + 1) ω - MeasureTheory.martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>Filter.atTop.IsCountablyGenerated<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<VAR>hin : i ≤ n<GOAL>μ[f n|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] f i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>μ[f n|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] f i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>MeasureTheory.stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_countable_range : (Set.range τ).Countable<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>MeasureTheory.stoppedValue f τ =ᵐ[μ] μ[f n|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>Countable ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>MeasureTheory.stoppedValue f τ =ᵐ[μ] μ[f n|hτ.measurableSpace]