ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>ρ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel ρ<VAR>κ : ProbabilityTheory.Kernel (α × β) Ω<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<GOAL>∀ᵐ (x : β) ∂ρ.fst a, κ (a, x) = ρ.condKernel (a, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>h : ¬MeasureTheory.SFinite μ<GOAL>μ ⊗ₘ κ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>h : ¬ProbabilityTheory.IsSFiniteKernel κ<GOAL>μ ⊗ₘ κ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>0 ⊗ₘ κ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<GOAL>μ ⊗ₘ 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ ⊗ₘ κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) t ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>h : ⇑κ =ᵐ[μ] ⇑η<GOAL>μ ⊗ₘ κ = μ ⊗ₘ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>p : α × β → Prop<VAR>hp : MeasurableSet {x | p x}<VAR>h : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)<GOAL>∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>p : α × β → Prop<VAR>h : ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x<GOAL>∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>p : α × β → Prop<VAR>hp : MeasurableSet {x | p x}<GOAL>(∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x) ↔ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>(μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : α × β), f x ∂μ ⊗ₘ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : α × β → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ ⊗ₘ κ)<GOAL>MeasureTheory.Integrable f (μ ⊗ₘ κ) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) (κ x)) ∧ MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ ⊗ₘ κ)<GOAL>∫ (x : α × β), f x ∂μ ⊗ₘ κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasureTheory.SFinite μ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>f : α × β → E<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)<GOAL>∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.dirac a ⊗ₘ κ) s = (κ a) (Prod.mk a ⁻¹' s)
<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel Unit β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>MeasureTheory.Measure.dirac () ⊗ₘ κ = MeasureTheory.Measure.map (Prod.mk ()) (κ ())
<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.Measure.dirac () ⊗ₘ ProbabilityTheory.Kernel.const Unit μ = MeasureTheory.Measure.map (Prod.mk ()) μ
<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>(MeasureTheory.Measure.dirac () ⊗ₘ ProbabilityTheory.Kernel.const Unit μ).snd = μ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × ℝ)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>ProbabilityTheory.IsRatCondKernelCDFAux (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × ℝ)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>ProbabilityTheory.IsRatCondKernelCDF (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × ℝ)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>ProbabilityTheory.IsCondKernelCDF κ.condKernelCDF κ κ.fst
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × ℝ)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ κ.condKernelReal = κ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>κ : ProbabilityTheory.Kernel Unit (α × ℝ)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ κ.condKernelUnitReal = κ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>Ω : Type u_5<VAR>Nonempty Ω<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>η : ProbabilityTheory.Kernel α ℝ<VAR>a : α<GOAL>(ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) a = if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (η a) else MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (MeasureTheory.Measure.dirac (Exists.choose ⋯))
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>Ω : Type u_5<VAR>Nonempty Ω<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>η : ProbabilityTheory.Kernel α ℝ<VAR>a : α<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>((ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) a) s = if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then (η a) (MeasureTheory.embeddingReal Ω '' s) else (MeasureTheory.embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) ℝ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) ⋯<GOAL>κ.fst ⊗ₖ ProbabilityTheory.Kernel.borelMarkovFromReal Ω η = ((κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) ⋯).fst ⊗ₖ η).comapRight ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) ℝ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) ⋯<GOAL>κ.fst ⊗ₖ ProbabilityTheory.Kernel.borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>κ : ProbabilityTheory.Kernel α (γ × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ κ.condKernelBorel = κ
<VAR>α : Type u_1<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>κ : ProbabilityTheory.Kernel Unit (α × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ κ.condKernelUnitBorel = κ
<VAR>α : Type u_5<VAR>Ω : Type u_6<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>ρ.condKernel = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel.comap (fun a => ((), a)) ⋯
<VAR>α : Type u_1<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>a : α<GOAL>ρ.condKernel a = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel ((), a)
<VAR>α : Type u_1<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<GOAL>ρ.fst ⊗ₘ ρ.condKernel = ρ
<VAR>α : Type u_1<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<GOAL>(ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>Countable α<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ ProbabilityTheory.Kernel.condKernelCountable (fun a => (κ a).condKernel) ⋯ = κ
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Ω : Type u_7<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>h : MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.condKernel = if hα : Countable α then ProbabilityTheory.Kernel.condKernelCountable (fun a => (κ a).condKernel) ⋯ else κ.condKernelBorel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>h : MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ κ.condKernel = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>a : α<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (κ.condKernel (a, x)) {y | (x, y) ∈ s} ∂κ.fst a = (κ a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>hf : MeasureTheory.AEStronglyMeasurable f (κ a)<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>hf : MeasureTheory.Integrable f (κ a)<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : α<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a)<GOAL>∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ρ s
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hf : MeasureTheory.AEStronglyMeasurable f ρ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hf : MeasureTheory.Integrable f ρ<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ<GOAL>∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ<GOAL>∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ