|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Paulo Rauber. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Paulo Rauber |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Probability.Kernel.CompProdEqIff |
| 9 | +public import Mathlib.Probability.Kernel.Composition.MeasureComp |
| 10 | + |
| 11 | +@[expose] public section |
| 12 | + |
| 13 | +open MeasureTheory ProbabilityTheory |
| 14 | + |
| 15 | +open scoped ENNReal |
| 16 | + |
| 17 | +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} |
| 18 | +variable {μ : Measure α} |
| 19 | + |
| 20 | +namespace MeasureTheory |
| 21 | + |
| 22 | +lemma map_withDensity_comp {g : α → γ} {f : γ → ℝ≥0∞} (hg : Measurable g) (hf : Measurable f) : |
| 23 | + (μ.withDensity (f ∘ g)).map g = (μ.map g).withDensity f := by |
| 24 | + ext s hs |
| 25 | + rw [Measure.map_apply hg hs, withDensity_apply _ (hg hs), withDensity_apply _ hs, |
| 26 | + setLIntegral_map hs hf hg] |
| 27 | + rfl |
| 28 | + |
| 29 | +lemma map_equiv_withDensity {e : α ≃ᵐ β} {f : α → ℝ≥0∞} (hf : Measurable f) : |
| 30 | + (μ.withDensity f).map e = (μ.map e).withDensity (f ∘ e.symm) := by |
| 31 | + simp_rw [← map_withDensity_comp e.measurable (hf.comp e.symm.measurable), |
| 32 | + Function.comp_assoc, MeasurableEquiv.symm_comp_self] |
| 33 | + rfl |
| 34 | + |
| 35 | +lemma map_swap_withDensity_comp_snd {μ : Measure (α × β)} {f : β → ℝ≥0∞} (hf : Measurable f) : |
| 36 | + (μ.withDensity (fun ab ↦ f ab.2)).map Prod.swap = |
| 37 | + (μ.map Prod.swap).withDensity (fun ba ↦ f ba.1) := by |
| 38 | + rw [← map_withDensity_comp measurable_swap (by fun_prop)] |
| 39 | + rfl |
| 40 | + |
| 41 | +end MeasureTheory |
| 42 | + |
| 43 | +namespace MeasureTheory.Measure |
| 44 | + |
| 45 | +lemma compProd_withDensity_left [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] {f : α → ℝ≥0∞} |
| 46 | + (hf : Measurable f) : (μ.withDensity f) ⊗ₘ κ = (μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1) := by |
| 47 | + refine ext_of_lintegral _ fun g hg ↦ ?_ |
| 48 | + calc ∫⁻ ab, g ab ∂((μ.withDensity f) ⊗ₘ κ) |
| 49 | + = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂(μ.withDensity f) := |
| 50 | + lintegral_compProd hg |
| 51 | + _ = ∫⁻ a, f a * ∫⁻ b, g (a, b) ∂κ a ∂μ := |
| 52 | + lintegral_withDensity_eq_lintegral_mul _ hf hg.lintegral_kernel_prod_right' |
| 53 | + _ = ∫⁻ a, ∫⁻ b, f a * g (a, b) ∂κ a ∂μ := |
| 54 | + lintegral_congr fun a ↦ (lintegral_const_mul _ (by fun_prop)).symm |
| 55 | + _ = ∫⁻ ab, (fun ab ↦ f ab.1) ab * g ab ∂(μ ⊗ₘ κ) := |
| 56 | + (lintegral_compProd ((hf.comp measurable_fst).mul hg)).symm |
| 57 | + _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)) := |
| 58 | + (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_fst) hg).symm |
| 59 | + |
| 60 | +lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] |
| 61 | + {f : α → ℝ≥0∞} {g : α → β → ℝ≥0∞} (hf : Measurable f) (hg : Measurable (Function.uncurry g)) |
| 62 | + [IsSFiniteKernel (κ.withDensity g)] : |
| 63 | + (μ.withDensity f) ⊗ₘ (κ.withDensity g) = |
| 64 | + (μ ⊗ₘ κ).withDensity (fun ac ↦ f ac.1 * g ac.1 ac.2) := by |
| 65 | + rw [compProd_withDensity hg, compProd_withDensity_left hf] |
| 66 | + exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm |
| 67 | + |
| 68 | +lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α β} [IsSFiniteKernel κ] |
| 69 | + [IsSFiniteKernel η] {f : β → ℝ≥0∞} (hf : Measurable f) |
| 70 | + (h : κ =ᵐ[μ] η.withDensity (fun _ b ↦ f b)) : |
| 71 | + μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2) := by |
| 72 | + /- A proof based on `compProd_congr` requires `IsSFiniteKernel (η.withDensity fun _ b ↦ f b)`. -/ |
| 73 | + refine ext_of_lintegral _ fun g hg ↦ ?_ |
| 74 | + calc ∫⁻ ab, g ab ∂(μ ⊗ₘ κ) |
| 75 | + = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂μ := |
| 76 | + lintegral_compProd hg |
| 77 | + _ = ∫⁻ a, ∫⁻ b, g (a, b) ∂((η a).withDensity f) ∂μ := by |
| 78 | + apply lintegral_congr_ae |
| 79 | + filter_upwards [h] with a ha |
| 80 | + rw [ha, Kernel.withDensity_apply _ (by fun_prop)] |
| 81 | + _ = ∫⁻ a, ∫⁻ b, f b * g (a, b) ∂η a ∂μ := by |
| 82 | + congr with a |
| 83 | + exact lintegral_withDensity_eq_lintegral_mul _ hf (by fun_prop) |
| 84 | + _ = ∫⁻ ab, f ab.2 * g ab ∂(μ ⊗ₘ η) := |
| 85 | + (lintegral_compProd ((hf.comp measurable_snd).mul hg)).symm |
| 86 | + _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2)) := |
| 87 | + (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_snd) hg).symm |
| 88 | + |
| 89 | +end MeasureTheory.Measure |
| 90 | + |
| 91 | +namespace ProbabilityTheory.Kernel |
| 92 | + |
| 93 | +lemma comp_withDensity_eq_withDensity_comp {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞} |
| 94 | + (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f := by |
| 95 | + refine Measure.ext_of_lintegral _ fun g hg ↦ ?_ |
| 96 | + calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ) |
| 97 | + = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ := |
| 98 | + Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable |
| 99 | + _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by |
| 100 | + congr with a |
| 101 | + exact lintegral_withDensity _ (by fun_prop) _ hg |
| 102 | + _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) := |
| 103 | + (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm |
| 104 | + _ = ∫⁻ b, g b ∂((κ ∘ₘ μ).withDensity f) := |
| 105 | + (lintegral_withDensity_eq_lintegral_mul _ hf hg).symm |
| 106 | + |
| 107 | +lemma compProd_withDensity_left {κ : Kernel α β} {η : Kernel (α × β) γ} {f : α → β → ℝ≥0∞} |
| 108 | + [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (κ.withDensity f)] |
| 109 | + (hf : Measurable (Function.uncurry f)) : |
| 110 | + (κ.withDensity f) ⊗ₖ η = (κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1) := by |
| 111 | + ext a : 1 |
| 112 | + calc ((κ.withDensity f) ⊗ₖ η) a |
| 113 | + = (κ a).withDensity (f a) ⊗ₘ η.sectR a := by |
| 114 | + rw [compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ hf] |
| 115 | + _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun bc ↦ f a bc.1) := |
| 116 | + Measure.compProd_withDensity_left (by fun_prop) |
| 117 | + _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)) a := by |
| 118 | + rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)] |
| 119 | + |
| 120 | +lemma withDensity_rnDeriv_eq' {κ η : Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β] |
| 121 | + [IsFiniteKernel κ] [IsFiniteKernel η] (h : ∀ a, κ a ≪ η a) : |
| 122 | + η.withDensity (κ.rnDeriv η) = κ := |
| 123 | + Kernel.ext fun a ↦ withDensity_rnDeriv_eq (h a) |
| 124 | + |
| 125 | +end ProbabilityTheory.Kernel |
0 commit comments