ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>t : Set α<GOAL>(PMF.ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(Multiset.card s)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>t : Set α<VAR>MeasurableSpace α<VAR>ht : MeasurableSet t<GOAL>(PMF.ofMultiset s hs).toMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(Multiset.card s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>m n : ℕ∞<VAR>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (Function.uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>m n : ℕ∞<VAR>x₀ : M<VAR>f : M → M'<VAR>hf : ContMDiffAt I I' n f x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiffAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderiv I I' f) x₀) x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>m n : ℕ∞<VAR>x₀ : N'<VAR>f : N → M → M'<VAR>g : N → M<VAR>g₁ : N' → N<VAR>g₂ : N' → E<VAR>hf : ContMDiffAt (J.prod I) I' n (Function.uncurry f) (g₁ x₀, g (g₁ x₀))<VAR>hg : ContMDiffAt J I m g (g₁ x₀)<VAR>hg₁ : ContMDiffAt J' J m g₁ x₀<VAR>hg₂ : ContMDiffAt J' 𝓘(𝕜, E) m g₂ x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiffAt J' 𝓘(𝕜, E') m (fun x => (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) (g₁ x₀) (g₁ x)) (g₂ x)) x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>s : Set M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>m n : ℕ∞<VAR>hf : ContMDiff I I' n f<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiff I.tangent I'.tangent m (tangentMap I I' f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>n : ℕ∞<VAR>hf : ContMDiff I I' n f<VAR>hmn : 1 ≤ n<GOAL>Continuous (tangentMap I I' f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>p : TangentBundle I M<GOAL>tangentMap I I.tangent (Bundle.zeroSection E (TangentSpace I)) p = { proj := { proj := p.proj, snd := 0 }, snd := (p.snd, 0) }
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>f : C^n⟮I, M; I', M'⟯<VAR>hn : 1 ≤ n<GOAL>MDifferentiable I I' ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : C^⊤⟮I, M; I', M'⟯<GOAL>MDifferentiable I I' ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : C^⊤⟮I, M; I', M'⟯<VAR>x : M<GOAL>MDifferentiableAt I I' (⇑f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>(μ + ν).bind ⇑κ = μ.bind ⇑κ + ν.bind ⇑κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<GOAL>(r • μ).bind ⇑κ = r • μ.bind ⇑κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>μ : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.const α (μ.bind ⇑κ) = κ ∘ₖ ProbabilityTheory.Kernel.const α μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>μ : MeasureTheory.Measure α<VAR>a : α<GOAL>(κ ∘ₖ ProbabilityTheory.Kernel.const α μ) a = μ.bind ⇑κ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>κ : ProbabilityTheory.Kernel α α<VAR>μ : MeasureTheory.Measure α<VAR>hκ : κ.Invariant μ<GOAL>μ.bind ⇑κ = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>κ : ProbabilityTheory.Kernel α α<VAR>μ : MeasureTheory.Measure α<VAR>hκ : κ.Invariant μ<GOAL>κ ∘ₖ ProbabilityTheory.Kernel.const α μ = ProbabilityTheory.Kernel.const α μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>κ η : ProbabilityTheory.Kernel α α<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hκ : κ.Invariant μ<VAR>hη : η.Invariant μ<GOAL>(κ ∘ₖ η).Invariant μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>self : ProbabilityTheory.Kernel α β<GOAL>Measurable self.toFun
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>Measurable ⇑κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>⇑0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<GOAL>⇑(κ + η) = ⇑κ + ⇑η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>n : ℕ<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>⇑(n • κ) = n • ⇑κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>a : α<GOAL>0 a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>a : α<GOAL>(κ + η) a = κ a + η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>n : ℕ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>a : α<GOAL>(n • κ) a = n • κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>I : Finset ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<GOAL>⇑(∑ i ∈ I, κ i) = ∑ i ∈ I, ⇑(κ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>I : Finset ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<VAR>a : α<GOAL>(∑ i ∈ I, κ i) a = ∑ i ∈ I, (κ i) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>I : Finset ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<VAR>a : α<VAR>s : Set β<GOAL>((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsMarkovKernel κ<VAR>a : α<GOAL>MeasureTheory.IsProbabilityMeasure (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsFiniteKernel κ<GOAL>∃ C < ⊤, ∀ (a : α), (κ a) Set.univ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>h : ProbabilityTheory.IsFiniteKernel κ<GOAL>ProbabilityTheory.IsFiniteKernel.bound κ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>ProbabilityTheory.IsFiniteKernel.bound κ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>h : ProbabilityTheory.IsFiniteKernel κ<VAR>a : α<VAR>s : Set β<GOAL>(κ a) s ≤ ProbabilityTheory.IsFiniteKernel.bound κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ ν : ProbabilityTheory.Kernel α β<VAR>hν : ProbabilityTheory.IsFiniteKernel ν<VAR>hκν : κ ≤ ν<GOAL>ProbabilityTheory.IsFiniteKernel κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>h : ∀ (a : α), κ a = η a<GOAL>κ = η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<GOAL>κ = η ↔ ∀ (a : α), κ a = η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<GOAL>κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a<GOAL>κ = η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<GOAL>κ = η ↔ ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f 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<GOAL>Measurable fun a => (κ a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>y' y : α<VAR>hy' : y' ∈ measurableAtom y<GOAL>κ y' = κ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (fun x => ((κ x) s).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (fun x => ((κ x) s).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<VAR>a : α<GOAL>(ProbabilityTheory.Kernel.sum κ) a = MeasureTheory.Measure.sum fun n => (κ n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((ProbabilityTheory.Kernel.sum κ) a) s = ∑' (n : ι), ((κ n) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<GOAL>(ProbabilityTheory.Kernel.sum fun x => 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κ : ι → ι → ProbabilityTheory.Kernel α β<GOAL>(ProbabilityTheory.Kernel.sum fun n => ProbabilityTheory.Kernel.sum (κ n)) = ProbabilityTheory.Kernel.sum fun m => ProbabilityTheory.Kernel.sum fun n => κ n m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Fintype ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<GOAL>ProbabilityTheory.Kernel.sum κ = ∑ i : ι, κ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κ η : ι → ProbabilityTheory.Kernel α β<GOAL>(ProbabilityTheory.Kernel.sum fun n => κ n + η n) = ProbabilityTheory.Kernel.sum κ + ProbabilityTheory.Kernel.sum η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsSFiniteKernel κ<GOAL>∃ κs, (∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κs n)) ∧ κ = ProbabilityTheory.Kernel.sum κs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>h : ProbabilityTheory.IsSFiniteKernel κ<GOAL>ProbabilityTheory.Kernel.sum κ.seq = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>h : ProbabilityTheory.IsSFiniteKernel κ<VAR>a : α<GOAL>(MeasureTheory.Measure.sum fun n => (κ.seq n) a) = κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κs : ι → ProbabilityTheory.Kernel α β<VAR>I : Finset ι<VAR>h : ∀ i ∈ I, ProbabilityTheory.IsSFiniteKernel (κs i)<GOAL>ProbabilityTheory.IsSFiniteKernel (∑ i ∈ I, κs i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Denumerable ι<VAR>κs : ι → ProbabilityTheory.Kernel α β<VAR>hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n)<GOAL>ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.sum κs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κs : ι → ProbabilityTheory.Kernel α β<VAR>hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n)<GOAL>ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.sum κs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>a : α<GOAL>(ProbabilityTheory.Kernel.deterministic f hf) a = MeasureTheory.Measure.dirac (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((ProbabilityTheory.Kernel.deterministic f hf) a) s = s.indicator (fun x => 1) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : Measurable f<GOAL>∫⁻ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>MeasurableSingletonClass β<GOAL>∫⁻ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>Decidable (g a ∈ s)<GOAL>∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>MeasurableSingletonClass β<VAR>s : Set β<VAR>Decidable (g a ∈ s)<GOAL>∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
<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>CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>∫ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
<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>CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>MeasurableSingletonClass β<GOAL>∫ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
<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>CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>Decidable (g a ∈ s)<GOAL>∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
<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>CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>MeasurableSingletonClass β<VAR>s : Set β<VAR>Decidable (g a ∈ s)<GOAL>∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μβ : MeasureTheory.Measure β<VAR>a : α<GOAL>(ProbabilityTheory.Kernel.const α μβ) a = μβ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>ProbabilityTheory.Kernel.const α 0 = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>β : Type u_4<VAR>MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.const β (μ + ν) = ProbabilityTheory.Kernel.const β μ + ProbabilityTheory.Kernel.const β ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure β<GOAL>(ProbabilityTheory.Kernel.sum fun n => ProbabilityTheory.Kernel.const α (μ n)) = ProbabilityTheory.Kernel.const α (MeasureTheory.Measure.sum μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Nonempty α<VAR>μβ : MeasureTheory.Measure β<GOAL>ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.const α μβ) ↔ MeasureTheory.SFinite μβ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>μ : MeasureTheory.Measure β<VAR>a : α<GOAL>∫⁻ (x : β), f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫⁻ (x : β), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<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>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>a : α<GOAL>∫ (x : β), f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β), f x ∂μ