ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop (𝓝 (MeasureTheory.Filtration.limitProcess f ℱ μ ω))
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R<GOAL>MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hunif : MeasureTheory.UniformIntegrable f 1 μ<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - MeasureTheory.Filtration.limitProcess f ℱ μ) 1 μ) Filter.atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hunif : MeasureTheory.UniformIntegrable f 1 μ<GOAL>∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop (𝓝 (MeasureTheory.Filtration.limitProcess f ℱ μ ω))
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>g : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hgtends : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (𝓝 0)<VAR>n : ℕ<GOAL>f n =ᵐ[μ] μ[g|↑ℱ n]
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hbdd : MeasureTheory.UniformIntegrable f 1 μ<VAR>n : ℕ<GOAL>f n =ᵐ[μ] μ[MeasureTheory.Filtration.limitProcess f ℱ μ|↑ℱ n]
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hgmeas : MeasureTheory.StronglyMeasurable g<GOAL>∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun n => (μ[g|↑ℱ n]) x) Filter.atTop (𝓝 (g x))
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hgmeas : MeasureTheory.StronglyMeasurable g<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (μ[g|↑ℱ n] - g) 1 μ) Filter.atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>g : Ω → ℝ<GOAL>∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun n => (μ[g|↑ℱ n]) x) Filter.atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>g : Ω → ℝ<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) Filter.atTop (𝓝 0)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>t : Finset ι<VAR>h : t.Nonempty<VAR>I : ι → Ideal R<GOAL>⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j = ⊤ ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>a : α<GOAL>κ.compProdFun η a ∅ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : ℕ → Set (β × γ)<VAR>hf_meas : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf_disj : Pairwise (Disjoint on f)<GOAL>κ.compProdFun η a (⋃ i, f i) = ∑' (i : ℕ), κ.compProdFun η a (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>κ.compProdFun η a s = ∑' (n : ℕ), κ.compProdFun (η.seq n) a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>a : α<VAR>s : Set (β × γ)<GOAL>κ.compProdFun η a s = ∑' (n : ℕ), (κ.seq n).compProdFun η a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>κ.compProdFun η a s = ∑' (n : ℕ) (m : ℕ), (κ.seq n).compProdFun (η.seq m) a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => κ.compProdFun η a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => κ.compProdFun η a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>((κ.compProd η) a) s = κ.compProdFun η a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>h : ¬ProbabilityTheory.IsSFiniteKernel κ<GOAL>κ.compProd η = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>h : ¬ProbabilityTheory.IsSFiniteKernel η<GOAL>κ.compProd η = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>((κ.compProd η) a) s = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<GOAL>∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a ≤ ((κ.compProd η) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel (α × β) γ<GOAL>ProbabilityTheory.Kernel.compProd 0 κ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>γ : Type u_5<VAR>MeasurableSpace γ<GOAL>κ.compProd 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>h2s : ((κ.compProd η) a) s ≠ ⊤<GOAL>∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>((κ.compProd η) a) s = 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>h : ((κ.compProd η) a) s = 0<GOAL>(fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>h : ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc<GOAL>∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>hp : MeasurableSet {x | p x}<VAR>h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)<GOAL>∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>hp : MeasurableSet {x | p x}<GOAL>(∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc) ↔ ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(κ.restrict hs).compProd (η.restrict ht) = (κ.compProd η).restrict ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ.restrict hs).compProd η = (κ.compProd η).restrict ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>κ.compProd (η.restrict ht) = (κ.compProd η).restrict ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<GOAL>∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (bc : β × γ), f bc ∂(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : AEMeasurable f ((κ.compProd η) a)<GOAL>∫⁻ (z : β × γ), f z ∂(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>((κ.compProd η) a) s = ∑' (n : ℕ) (m : ℕ), (((κ.seq n).compProd (η.seq m)) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>κ.compProd η = ProbabilityTheory.Kernel.sum fun n => ProbabilityTheory.Kernel.sum fun m => (κ.seq n).compProd (η.seq m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<GOAL>κ.compProd η = ProbabilityTheory.Kernel.sum fun n => (κ.seq n).compProd η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>κ.compProd η = ProbabilityTheory.Kernel.sum fun n => κ.compProd (η.seq n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>((κ.compProd η) a) Set.univ ≤ (κ a) Set.univ * ProbabilityTheory.IsFiniteKernel.bound η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>μ κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>(μ + κ).compProd η = μ.compProd η + κ.compProd η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>μ : ProbabilityTheory.Kernel α β<VAR>κ η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>μ.compProd (κ + η) = μ.compProd κ + μ.compProd η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<GOAL>(κ.compProd η).comapRight ⋯ = κ.compProd (η.comapRight hf)
<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 : Measurable f<VAR>a : α<GOAL>(κ.map f hf) a = MeasureTheory.Measure.map 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 : Measurable f<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((κ.map f hf) a) s = (κ a) (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>hf : Measurable f<GOAL>ProbabilityTheory.Kernel.map 0 f hf = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>κ.map id ⋯ = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>κ.map (fun a => 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 : Measurable f<VAR>a : α<VAR>g' : γ → ℝ≥0∞<VAR>hg : Measurable g'<GOAL>∫⁻ (b : γ), g' b ∂(κ.map f hf) a = ∫⁻ (a : β), g' (f a) ∂κ 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>ProbabilityTheory.IsSFiniteKernel κ<VAR>hf : Measurable f<GOAL>(ProbabilityTheory.Kernel.sum fun n => (κ.seq n).map f hf) = κ.map f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>(ProbabilityTheory.Kernel.const γ μ).map f hf = ProbabilityTheory.Kernel.const γ (MeasureTheory.Measure.map f μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>g : γ → α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hg : Measurable g<VAR>c : γ<GOAL>(κ.comap g hg) c = κ (g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>g : γ → α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hg : Measurable g<VAR>c : γ<VAR>s : Set β<GOAL>((κ.comap g hg) c) s = (κ (g c)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>g : γ → α<VAR>hg : Measurable g<GOAL>ProbabilityTheory.Kernel.comap 0 g hg = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>κ.comap id ⋯ = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>κ.comap (fun a => a) ⋯ = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>g : γ → α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hg : Measurable g<VAR>c : γ<VAR>g' : β → ℝ≥0∞<GOAL>∫⁻ (b : β), g' b ∂(κ.comap g hg) c = ∫⁻ (b : β), g' b ∂κ (g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>g : γ → α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hg : Measurable g<GOAL>(ProbabilityTheory.Kernel.sum fun n => (κ.seq n).comap g hg) = κ.comap g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>κ : ProbabilityTheory.Kernel β γ<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(κ.map g hg).comap f hf = (κ.comap f hf).map g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ca : γ × α<GOAL>(ProbabilityTheory.Kernel.prodMkLeft γ κ) ca = κ ca.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ca : α × γ<GOAL>(ProbabilityTheory.Kernel.prodMkRight γ κ) ca = κ ca.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ca : γ × α<VAR>s : Set β<GOAL>((ProbabilityTheory.Kernel.prodMkLeft γ κ) ca) s = (κ ca.2) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ca : α × γ<VAR>s : Set β<GOAL>((ProbabilityTheory.Kernel.prodMkRight γ κ) ca) s = (κ ca.1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<GOAL>ProbabilityTheory.Kernel.prodMkLeft α 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<GOAL>ProbabilityTheory.Kernel.prodMkRight α 0 = 0