ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>x ∉ κ.mutuallySingularSetSlice η a ↔ κ.rnDerivAux (κ + η) a x < 1
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<GOAL>MeasurableSet (κ.mutuallySingularSet η)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<GOAL>MeasurableSet (κ.mutuallySingularSetSlice η a)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(η a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>κ.rnDeriv η a x = ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<GOAL>κ.rnDeriv η = fun a x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<GOAL>Measurable fun p => κ.rnDeriv η p.1 p.2
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<GOAL>Measurable fun x => κ.rnDeriv η a x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>κ.rnDeriv η a x = ⊤ ↔ (a, x) ∈ κ.mutuallySingularSet η
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>κ.rnDeriv η a x = ⊤ ↔ x ∈ κ.mutuallySingularSetSlice η a
<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>κ.singularPart η = (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<GOAL>Measurable fun p => ↑(κ.rnDerivAux (κ + η) p.1 p.2).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) p.1 p.2).toNNReal * κ.rnDeriv η p.1 p.2
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<GOAL>Measurable fun x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<GOAL>((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>((κ.singularPart η) a) s = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ κ.mutuallySingularSetSlice η a<GOAL>((κ.singularPart η) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : s ⊆ κ.mutuallySingularSetSlice η a<GOAL>((η.withDensity (κ.rnDeriv η)) a) s = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>((η.withDensity (κ.rnDeriv η)) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a ⟂ₘ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<GOAL>η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a = 0 ↔ κ a ≪ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ κ a ⟂ₘ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<GOAL>MeasurableSet {a | κ a ≪ η a}
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<GOAL>MeasurableSet {a | κ a ⟂ₘ η a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<GOAL>MeasureTheory.HasFiniteIntegral (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<GOAL>MeasureTheory.Integrable (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f : β × γ → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>δ : Type u_5<VAR>TopologicalSpace δ<VAR>f : β × γ → δ<VAR>hf : MeasureTheory.AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>∀ᵐ (x : β) ∂κ a, MeasureTheory.AEStronglyMeasurable (fun y => f (x, y)) (η (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧ MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : MeasureTheory.AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>MeasureTheory.HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧ MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>MeasureTheory.Integrable f ((κ ⊗ₖ η) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable (fun y => f (x, y)) (η (a, x))) ∧ MeasureTheory.Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<GOAL>∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable (fun y => f (x, y)) (η (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x)) ∂κ a = ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a = ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f g : β × γ → E<VAR>F : E → ℝ≥0∞<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫⁻ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a = ∫⁻ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f g : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), ∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x) ∂κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f g : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f g : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), ∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x) ∂κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a - ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f g : β × γ → E<VAR>hf : MeasureTheory.Integrable f ((κ ⊗ₖ η) a)<VAR>hg : MeasureTheory.Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), ∫ (y : γ), (f - g) (x, y) ∂η (a, x) ∂κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a - ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<GOAL>Continuous fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f : β × γ → E<GOAL>MeasureTheory.Integrable f ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f : β × γ → E<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)<GOAL>∫ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f : β × γ → E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ((κ ⊗ₖ η) a)<GOAL>∫ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>NormedAddCommGroup E<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>NormedSpace ℝ E<VAR>f : β × γ → E<VAR>t : Set γ<VAR>ht : MeasurableSet t<VAR>hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ ⊗ₖ η) a)<GOAL>∫ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>m : MeasurableSpace Ω<VAR>self : MeasureTheory.Filtration ι m<VAR>i : ι<GOAL>↑self i ≤ m
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>m : MeasurableSpace Ω<VAR>self : MeasureTheory.Filtration ι m<GOAL>Monotone ↑self
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>i j : ι<VAR>f : MeasureTheory.Filtration ι m<VAR>hij : i ≤ j<GOAL>↑f i ≤ ↑f j
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>i : ι<GOAL>↑f i ≤ m
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f g : MeasureTheory.Filtration ι m<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>m' : MeasurableSpace Ω<VAR>hm' : m' ≤ m<VAR>i : ι<GOAL>↑(MeasureTheory.Filtration.const ι m' hm') i = m'
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f g : MeasureTheory.Filtration ι m<GOAL>↑(f ⊔ g) = ↑f ⊔ ↑g
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f g : MeasureTheory.Filtration ι m<GOAL>↑(f ⊓ g) = ↑f ⊓ ↑g
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>s : Set (MeasureTheory.Filtration ι m)<VAR>i : ι<GOAL>↑(sSup s) i = sSup ((fun f => ↑f i) '' s)
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>s : Set (MeasureTheory.Filtration ι m)<VAR>i : ι<GOAL>↑(sInf s) i = if s.Nonempty then sInf ((fun f => ↑f i) '' s) else m
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>s : Set Ω<VAR>i : ι<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>μ : MeasureTheory.Measure Ω<VAR>f : MeasureTheory.Filtration ι m<VAR>self : MeasureTheory.SigmaFiniteFiltration μ f<VAR>i : ι<GOAL>MeasureTheory.SigmaFinite (μ.trim ⋯)
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : MeasureTheory.Filtration ι m<VAR>g : Ω → ℝ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.UniformIntegrable (fun i => μ[g|↑f i]) 1 μ