Radon-Nikodym derivative and Lebesgue decomposition for kernels

theorem ProbabilityTheory.Kernel.ae_compProd_of_ae_fst {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} (κ : ProbabilityTheory.Kernel α γ) {p : α → Prop} (hp : MeasurableSet {x : α | p x}) (h : ∀ᵐ (a : α) ∂μ, p a) : ∀ᵐ (x : α × γ) ∂μ.compProd κ, p x.1

theorem ProbabilityTheory.Kernel.ae_eq_compProd_of_ae_eq_fst {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {β : Type u_3} : ∀ {x : MeasurableSpace β} [inst : AddGroup β] [inst_1 : MeasurableSingletonClass β] [inst : MeasurableSub₂ β] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) {f g : α → β}, Measurable f → Measurable g → f =ᵐ[μ] g → (fun (p : α × γ) => f p.1) =ᵐ[μ.compProd κ] fun (p : α × γ) => g p.1

theorem ProbabilityTheory.Kernel.ae_eq_compProd_of_forall_ae_eq {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {β : Type u_3} : ∀ {x : MeasurableSpace β} [inst : AddGroup β] [inst_1 : MeasurableSingletonClass β] [inst : MeasurableSub₂ β] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) {f g : α → γ → β}, Measurable (Function.uncurry f) → Measurable (Function.uncurry g) → (∀ (a : α), f a =ᵐ[κ a] g a) → (fun (p : α × γ) => f p.1 p.2) =ᵐ[μ.compProd κ] fun (p : α × γ) => g p.1 p.2

theorem ProbabilityTheory.Kernel.ENNReal.ae_eq_compProd_of_ae_eq_fst {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) {f : α → ENNReal} {g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) (h : f =ᵐ[μ] g) : (fun (p : α × γ) => f p.1) =ᵐ[μ.compProd κ] fun (p : α × γ) => g p.1

theorem ProbabilityTheory.Kernel.ENNReal.ae_eq_compProd_of_forall_ae_eq {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) {f : α → γ → ENNReal} {g : α → γ → ENNReal} (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) (h : ∀ (a : α), f a =ᵐ[κ a] g a) : (fun (p : α × γ) => f p.1 p.2) =ᵐ[μ.compProd κ] fun (p : α × γ) => g p.1 p.2

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd_left_of_ac {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (hμν : μ.AbsolutelyContinuous ν) (κ : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] : (μ.compProd κ).rnDeriv (ν.compProd κ) =ᵐ[ν.compProd κ] fun (p : α × γ) => μ.rnDeriv ν p.1

theorem ProbabilityTheory.Kernel.todo {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ((ν.withDensity (μ.rnDeriv ν)).compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] (μ.compProd κ).rnDeriv (ν.compProd η)

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd_left {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] : (μ.compProd κ).rnDeriv (ν.compProd κ) =ᵐ[ν.compProd κ] fun (p : α × γ) => μ.rnDeriv ν p.1

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd_left' {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] : ∀ᵐ (a : α) ∂ν, (fun (b : γ) => (μ.compProd κ).rnDeriv (ν.compProd κ) (a, b)) =ᵐ[κ a] fun (x : γ) => μ.rnDeriv ν a

theorem ProbabilityTheory.Kernel.rnDeriv_compProd {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α γ} {η : ProbabilityTheory.Kernel α γ} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_ac : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : (fun (p : α × γ) => μ.rnDeriv ν p.1 * (μ.compProd κ).rnDeriv (μ.compProd η) p) =ᵐ[ν.compProd η] (μ.compProd κ).rnDeriv (ν.compProd η)

theorem ProbabilityTheory.Kernel.rnDeriv_compProd' {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α γ} {η : ProbabilityTheory.Kernel α γ} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_ac : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : ∀ᵐ (a : α) ∂ν, (fun (b : γ) => μ.rnDeriv ν a * (μ.compProd κ).rnDeriv (μ.compProd η) (a, b)) =ᵐ[η a] fun (b : γ) => (μ.compProd κ).rnDeriv (ν.compProd η) (a, b)

theorem ProbabilityTheory.Kernel.todo' {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (μ.compProd (η.withDensity (κ.rnDeriv η))).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] (μ.compProd κ).rnDeriv (ν.compProd η)

theorem ProbabilityTheory.Kernel.todo1 {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ((ν.withDensity (μ.rnDeriv ν)).compProd (η.withDensity (κ.rnDeriv η))).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] (μ.compProd κ).rnDeriv (ν.compProd η)

theorem ProbabilityTheory.Kernel.todo2 {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (fun (p : α × γ) => (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν p.1 * (η.withDensity (κ.rnDeriv η)).rnDeriv η p.1 p.2) =ᵐ[ν.compProd η] fun (p : α × γ) => μ.rnDeriv ν p.1 * κ.rnDeriv η p.1 p.2

theorem ProbabilityTheory.Kernel.setLIntegral_rnDeriv_right {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α γ} {η : ProbabilityTheory.Kernel α γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {a : α} (hκη : (κ a).AbsolutelyContinuous (η a)) (t : Set γ) : ∫⁻ (b : γ) in t, κ.rnDeriv η a b ∂η a = (κ a) t

theorem ProbabilityTheory.Kernel.setLIntegral_rnDeriv_compProd {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α γ} {η : ProbabilityTheory.Kernel α γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) {s : Set α} (hs : MeasurableSet s) {t : Set γ} (ht : MeasurableSet t) : ∫⁻ (p : α × γ) in s ×ˢ t, κ.rnDeriv η p.1 p.2 ∂μ.compProd η = (μ.compProd κ) (s ×ˢ t)

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd_right_of_ac {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) {κ : ProbabilityTheory.Kernel α γ} {η : ProbabilityTheory.Kernel α γ} (h_ac : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (μ.compProd κ).rnDeriv (μ.compProd η) =ᵐ[μ.compProd η] fun (p : α × γ) => κ.rnDeriv η p.1 p.2

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd_right {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (μ.compProd κ).rnDeriv (μ.compProd η) =ᵐ[μ.compProd η] fun (p : α × γ) => κ.rnDeriv η p.1 p.2

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd_right' {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ∀ᵐ (a : α) ∂μ, (fun (x : γ) => (μ.compProd κ).rnDeriv (μ.compProd η) (a, x)) =ᵐ[η a] fun (x : γ) => (κ a).rnDeriv (η a) x

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (μ.compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] fun (p : α × γ) => μ.rnDeriv ν p.1 * κ.rnDeriv η p.1 p.2

theorem ProbabilityTheory.Kernel.rnDeriv_measure_compProd' {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountableOrCountablyGenerated α γ] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α γ) (η : ProbabilityTheory.Kernel α γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ∀ᵐ (a : α) ∂ν, (fun (b : γ) => (μ.compProd κ).rnDeriv (ν.compProd η) (a, b)) =ᵐ[η a] fun (b : γ) => μ.rnDeriv ν a * (κ a).rnDeriv (η a) b