ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>a : α<VAR>s : Set β<GOAL>∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>(κ.restrict hs) a = (κ a).restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s t : Set β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hs : MeasurableSet s<VAR>a : α<VAR>ht : MeasurableSet t<GOAL>((κ.restrict hs) a) t = (κ a) (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>κ.restrict ⋯ = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hs : MeasurableSet s<VAR>a : α<VAR>f : β → ℝ≥0∞<GOAL>∫⁻ (b : β), f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in s, f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hs : MeasurableSet s<VAR>a : α<VAR>f : β → ℝ≥0∞<VAR>t : Set β<GOAL>∫⁻ (b : β) in t, f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>s : Set β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : β → E<VAR>a : α<VAR>hs : MeasurableSet s<VAR>t : Set β<GOAL>∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>a : α<GOAL>(κ.comapRight hf) a = MeasureTheory.Measure.comap f (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>((κ.comapRight hf) a) t = (κ a) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>κ.comapRight ⋯ = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>hκ : ∀ (a : α), (κ a) (Set.range f) = 1<GOAL>ProbabilityTheory.IsMarkovKernel (κ.comapRight hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<GOAL>(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then κ a else η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>t : Set β<GOAL>((ProbabilityTheory.Kernel.piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>g : β → ℝ≥0∞<GOAL>∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>t : Set β<GOAL>∫⁻ (b : β) in t, g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>DecidablePred fun x => x ∈ s<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>g : β → E<GOAL>∫ (b : β), g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>DecidablePred fun x => x ∈ s<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>g : β → E<VAR>t : Set β<GOAL>∫ (b : β) in t, g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>ProbabilityTheory.gaussianPDFReal μ v = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))
<VAR>m : ℝ<GOAL>ProbabilityTheory.gaussianPDFReal m 0 = 0
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>x : ℝ<VAR>hv : v ≠ 0<GOAL>0 < ProbabilityTheory.gaussianPDFReal μ v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>x : ℝ<GOAL>0 ≤ ProbabilityTheory.gaussianPDFReal μ v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>Measurable (ProbabilityTheory.gaussianPDFReal μ v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>MeasureTheory.StronglyMeasurable (ProbabilityTheory.gaussianPDFReal μ v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>MeasureTheory.Integrable (ProbabilityTheory.gaussianPDFReal μ v) MeasureTheory.volume
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<GOAL>∫⁻ (x : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>∫ (x : ℝ), ProbabilityTheory.gaussianPDFReal μ v x = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>x y : ℝ<GOAL>ProbabilityTheory.gaussianPDFReal μ v (x - y) = ProbabilityTheory.gaussianPDFReal (μ + y) v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>x y : ℝ<GOAL>ProbabilityTheory.gaussianPDFReal μ v (x + y) = ProbabilityTheory.gaussianPDFReal (μ - y) v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>ProbabilityTheory.gaussianPDFReal μ v (c⁻¹ * x) = |c| * ProbabilityTheory.gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>ProbabilityTheory.gaussianPDFReal μ v (c * x) = |c⁻¹| * ProbabilityTheory.gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>ProbabilityTheory.gaussianPDF μ v = fun x => ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x)
<VAR>μ : ℝ<GOAL>ProbabilityTheory.gaussianPDF μ 0 = 0
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>x : ℝ<GOAL>0 < ProbabilityTheory.gaussianPDF μ v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>Measurable (ProbabilityTheory.gaussianPDF μ v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<GOAL>∫⁻ (x : ℝ), ProbabilityTheory.gaussianPDF μ v x = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>ProbabilityTheory.gaussianReal μ v = MeasureTheory.volume.withDensity (ProbabilityTheory.gaussianPDF μ v)
<VAR>μ : ℝ<GOAL>ProbabilityTheory.gaussianReal μ 0 = MeasureTheory.Measure.dirac μ
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>(ProbabilityTheory.gaussianReal μ v) s = ∫⁻ (x : ℝ) in s, ProbabilityTheory.gaussianPDF μ v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>(ProbabilityTheory.gaussianReal μ v) s = ENNReal.ofReal (∫ (x : ℝ) in s, ProbabilityTheory.gaussianPDFReal μ v x)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>ProbabilityTheory.gaussianReal μ v ≪ MeasureTheory.volume
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>MeasureTheory.volume ≪ ProbabilityTheory.gaussianReal μ v
<VAR>μ : ℝ<VAR>v : ℝ≥0<GOAL>(ProbabilityTheory.gaussianReal μ v).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.gaussianPDF μ v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>f' : ℝ → ℝ<VAR>h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.comap f (ProbabilityTheory.gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * ProbabilityTheory.gaussianPDFReal μ v (f x))
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>f : ℝ ≃ᵐ ℝ<VAR>f' : ℝ → ℝ<VAR>h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.map (⇑f.symm) (ProbabilityTheory.gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * ProbabilityTheory.gaussianPDFReal μ v (f x))
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<GOAL>MeasureTheory.Measure.map (fun x => x + y) (ProbabilityTheory.gaussianReal μ v) = ProbabilityTheory.gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<GOAL>MeasureTheory.Measure.map (fun x => y + x) (ProbabilityTheory.gaussianReal μ v) = ProbabilityTheory.gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<GOAL>MeasureTheory.Measure.map (fun x => c * x) (ProbabilityTheory.gaussianReal μ v) = ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<GOAL>MeasureTheory.Measure.map (fun x => x * c) (ProbabilityTheory.gaussianReal μ v) = ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>MeasureTheory.MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v<VAR>y : ℝ<GOAL>MeasureTheory.Measure.map (fun ω => X ω + y) MeasureTheory.volume = ProbabilityTheory.gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>MeasureTheory.MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v<VAR>y : ℝ<GOAL>MeasureTheory.Measure.map (fun ω => y + X ω) MeasureTheory.volume = ProbabilityTheory.gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>MeasureTheory.MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v<VAR>c : ℝ<GOAL>MeasureTheory.Measure.map (fun ω => c * X ω) MeasureTheory.volume = ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>MeasureTheory.MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v<VAR>c : ℝ<GOAL>MeasureTheory.Measure.map (fun ω => X ω * c) MeasureTheory.volume = ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ρ.IicSnd r) s = ρ (s ×ˢ Set.Iic r)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℝ<GOAL>(ρ.IicSnd r) Set.univ = ρ (Set.univ ×ˢ Set.Iic r)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r r' : ℝ<VAR>h_le : r ≤ r'<GOAL>ρ.IicSnd r ≤ ρ.IicSnd r'
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℝ<GOAL>ρ.IicSnd r ≤ ρ.fst
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℝ<GOAL>ρ.IicSnd r ≪ ρ.fst
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>r : ℝ<GOAL>MeasureTheory.IsFiniteMeasure (ρ.IicSnd r)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>t : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>⨅ r, (ρ.IicSnd ↑↑r) s = (ρ.IicSnd ↑t) s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Filter.Tendsto (fun r => (ρ.IicSnd ↑r) s) Filter.atTop (𝓝 (ρ.fst s))
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Filter.Tendsto (fun r => (ρ.IicSnd ↑r) s) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℚ<GOAL>Measurable (ProbabilityTheory.preCDF ρ r)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<GOAL>Measurable fun a r => (ProbabilityTheory.preCDF ρ r a).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℚ<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>ρ.fst.withDensity (ProbabilityTheory.preCDF ρ r) = ρ.IicSnd ↑r
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>∫⁻ (x : α) in s, ProbabilityTheory.preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℚ<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>∫⁻ (x : α), ProbabilityTheory.preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) Set.univ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, Monotone fun r => ProbabilityTheory.preCDF ρ r a
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), ProbabilityTheory.preCDF ρ r a ≤ 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>∫ (x : α) in s, (ProbabilityTheory.preCDF ρ r x).toReal ∂ρ.fst = ((ρ.IicSnd ↑r) s).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>r : ℚ<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>∫ (x : α), (ProbabilityTheory.preCDF ρ r x).toReal ∂ρ.fst = ((ρ.IicSnd ↑r) Set.univ).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>x : ℚ<GOAL>MeasureTheory.Integrable (fun a => (ProbabilityTheory.preCDF ρ x a).toReal) ρ.fst
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>ProbabilityTheory.IsRatCondKernelCDFAux (fun p r => (ProbabilityTheory.preCDF ρ r p.2).toReal) (ProbabilityTheory.Kernel.const Unit ρ) (ProbabilityTheory.Kernel.const Unit ρ.fst)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>ProbabilityTheory.IsRatCondKernelCDF (fun p r => (ProbabilityTheory.preCDF ρ r p.2).toReal) (ProbabilityTheory.Kernel.const Unit ρ) (ProbabilityTheory.Kernel.const Unit ρ.fst)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<GOAL>ProbabilityTheory.condCDF ρ a = ProbabilityTheory.stieltjesOfMeasurableRat (fun p r => (ProbabilityTheory.preCDF ρ r p.2).toReal) ⋯ ((), a)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>ProbabilityTheory.IsCondKernelCDF (fun p => ProbabilityTheory.condCDF ρ p.2) (ProbabilityTheory.Kernel.const Unit ρ) (ProbabilityTheory.Kernel.const Unit ρ.fst)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<VAR>r : ℝ<GOAL>0 ≤ ↑(ProbabilityTheory.condCDF ρ a) r
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.condCDF ρ a) x ≤ 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<GOAL>Filter.Tendsto (↑(ProbabilityTheory.condCDF ρ a)) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<GOAL>Filter.Tendsto (↑(ProbabilityTheory.condCDF ρ a)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>r : ℚ<GOAL>(fun a => ↑(ProbabilityTheory.condCDF ρ a) ↑r) =ᵐ[ρ.fst] fun a => (ProbabilityTheory.preCDF ρ r a).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>r : ℚ<GOAL>(fun a => ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) ↑r)) =ᵐ[ρ.fst] ProbabilityTheory.preCDF ρ r
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>x : ℝ<GOAL>Measurable fun a => ↑(ProbabilityTheory.condCDF ρ a) x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>x : ℝ<GOAL>MeasureTheory.StronglyMeasurable fun a => ↑(ProbabilityTheory.condCDF ρ a) x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>x : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x) ∂ρ.fst = ρ (s ×ˢ Set.Iic x)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>x : ℝ<GOAL>∫⁻ (a : α), ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x) ∂ρ.fst = ρ (Set.univ ×ˢ Set.Iic x)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>x : ℝ<GOAL>MeasureTheory.Integrable (fun a => ↑(ProbabilityTheory.condCDF ρ a) x) ρ.fst
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>x : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (a : α) in s, ↑(ProbabilityTheory.condCDF ρ a) x ∂ρ.fst = (ρ (s ×ˢ Set.Iic x)).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>x : ℝ<GOAL>∫ (a : α), ↑(ProbabilityTheory.condCDF ρ a) x ∂ρ.fst = (ρ (Set.univ ×ˢ Set.Iic x)).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<VAR>x : ℝ<GOAL>(ProbabilityTheory.condCDF ρ a).measure (Set.Iic x) = ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>a : α<GOAL>(ProbabilityTheory.condCDF ρ a).measure Set.univ = 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<GOAL>Measurable fun a => (ProbabilityTheory.condCDF ρ a).measure
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → F<VAR>TopologicalSpace F<VAR>hm : m ≤ mΩ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (id ω, id ω)) μ)
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → F<VAR>NormedAddCommGroup F<VAR>hm : m ≤ mΩ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (id ω, id ω)) μ)
<VAR>Ω : Type u_3<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>m : MeasurableSpace Ω<GOAL>ProbabilityTheory.condexpKernel μ m = (ProbabilityTheory.condDistrib id id μ).comap id ⋯
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ω : Ω<GOAL>(ProbabilityTheory.condexpKernel μ m) ω = (ProbabilityTheory.condDistrib id id μ) (id ω)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>Measurable fun ω => ((ProbabilityTheory.condexpKernel μ m) ω) s
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.StronglyMeasurable fun ω => ((ProbabilityTheory.condexpKernel μ m) ω) s
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>NormedSpace ℝ F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>NormedSpace ℝ F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>∀ᵐ (ω : Ω) ∂μ, MeasureTheory.Integrable f ((ProbabilityTheory.condexpKernel μ m) ω)
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>NormedSpace ℝ F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun ω => ‖∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω‖) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>NormedSpace ℝ F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (fun ω => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(fun ω => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hm : m ≤ mΩ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(fun ω => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω => 1|m]
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hm : m ≤ mΩ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(fun ω => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ.trim hm] μ[s.indicator fun ω => 1|m]
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω