chain rule for rnDeriv

TestingLowerBounds/ForMathlib/AbsolutelyContinuous.lean

@@ -15,17 +15,17 @@ open ProbabilityTheory MeasurableSpace Set
 
 open scoped ENNReal
 
-namespace MeasureTheory
+namespace MeasureTheory.Measure
 
 variable {α γ : Type*} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
   {μ ν : Measure α} {κ η : Kernel α γ}
 
-lemma Measure.absolutelyContinuous_compProd_left_iff
+lemma absolutelyContinuous_compProd_left_iff
     [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] :
     μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν :=
-  ⟨Measure.absolutelyContinuous_of_compProd, fun h ↦ Measure.absolutelyContinuous_compProd_left h _⟩
+  ⟨absolutelyContinuous_of_compProd, fun h ↦ absolutelyContinuous_compProd_left h _⟩
 
-lemma Measure.mutuallySingular_compProd_left (hμν : μ ⟂ₘ ν) (κ η : Kernel α γ) :
+lemma mutuallySingular_compProd_left (hμν : μ ⟂ₘ ν) (κ η : Kernel α γ) :
     μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by
   by_cases hμ : SFinite μ
   swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
@@ -36,13 +36,81 @@ lemma Measure.mutuallySingular_compProd_left (hμν : μ ⟂ₘ ν) (κ η : Ker
   by_cases hη : IsSFiniteKernel η
   swap; · rw [compProd_of_not_isSFiniteKernel _ _ hη]; simp
   refine ⟨hμν.nullSet ×ˢ univ, hμν.measurableSet_nullSet.prod .univ, ?_⟩
-  rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]
-  simp only [Measure.MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ,
+  rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]
+  simp only [MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ,
     prod_empty, union_empty, true_and]
-  rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet.compl .univ]
+  rw [compProd_apply_prod hμν.measurableSet_nullSet.compl .univ]
   simp
 
-lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α γ]
+lemma mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α}
+    [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η]
+    (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η) (hμ : ξ ≪ μ) (hν : ξ ≪ ν) :
+    ∀ᵐ x ∂ξ, κ x ⟂ₘ η x := by
+  have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet
+  have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet
+  have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet
+  rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
+  · filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν
+    exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prod_mk_left hs, ⟨hxμ, hxν⟩⟩
+  · exact Kernel.measurable_kernel_prod_mk_left hs.compl |>.aemeasurable
+  · exact Kernel.measurable_kernel_prod_mk_left hs |>.aemeasurable
+  · exact hs.compl
+  · exact hs
+
+lemma mutuallySingular_compProd_iff_of_same_right (μ ν : Measure α) [IsFiniteMeasure μ]
+    [IsFiniteMeasure ν] (κ : Kernel α γ) [IsFiniteKernel κ] [hκ : ∀ x, NeZero (κ x)] :
+    μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν := by
+  refine ⟨fun h ↦ ?_, fun h ↦ mutuallySingular_compProd_left h _ _⟩
+  rw [← withDensity_rnDeriv_eq_zero]
+  have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_ (ξ  := ν.withDensity (∂μ/∂ν))
+  rotate_left
+  · exact absolutelyContinuous_of_le (μ.withDensity_rnDeriv_le ν)
+  · exact withDensity_absolutelyContinuous _ _
+  simp_rw [MutuallySingular.self_iff, (hκ _).ne] at hh
+  exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)
+
+lemma absolutelyContinuous_of_add_of_mutuallySingular {ν₁ ν₂ : Measure α}
+    (h_ms : μ ⟂ₘ ν₂) (h : μ ≪ ν₁ + ν₂) : μ ≪ ν₁ := by
+  refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
+  let t := h_ms.nullSet
+  have ht : MeasurableSet t := h_ms.measurableSet_nullSet
+  have htμ : μ t = 0 := h_ms.measure_nullSet
+  have htν₂ : ν₂ tᶜ = 0 := h_ms.measure_compl_nullSet
+  have : μ s = μ (s ∩ tᶜ) := by
+    conv_lhs => rw [← inter_union_compl s t]
+    rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]
+    · exact (disjoint_compl_right.inter_right' _ ).inter_left' _
+    · exact hs.inter ht.compl
+  rw [this]
+  refine h ?_
+  simp only [Measure.coe_add, Pi.add_apply, add_eq_zero]
+  exact ⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩
+
+lemma absolutelyContinuous_compProd_of_compProd [SFinite ν] [IsSFiniteKernel η]
+    (hμν : μ ≪ ν) (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) :
+    μ ⊗ₘ κ ≪ ν ⊗ₘ η := by
+  by_cases hμ : SFinite μ
+  swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
+  refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
+  suffices (μ ⊗ₘ η) s = 0 from hκη this
+  rw [measure_zero_iff_ae_nmem, ae_compProd_iff hs.compl] at hs_zero ⊢
+  exact hμν.ae_le hs_zero
+
+lemma absolutelyContinuous_compProd_of_compProd'
+    [SigmaFinite μ] [SigmaFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η]
+    (hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
+    μ ⊗ₘ κ ≪ μ ⊗ₘ η := by
+  rw [ν.haveLebesgueDecomposition_add μ, compProd_add_left, add_comm] at hκη
+  have h := absolutelyContinuous_of_add_of_mutuallySingular ?_ hκη
+  · refine h.trans ?_
+    refine absolutelyContinuous_compProd_left ?_ _
+    exact withDensity_absolutelyContinuous _ _
+  · refine mutuallySingular_compProd_left ?_ _ _
+    exact (mutuallySingular_singularPart _ _).symm
+
+variable [CountableOrCountablyGenerated α γ]
+
+lemma mutuallySingular_compProd_right
     (μ ν : Measure α) {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η]
     (hκη : ∀ᵐ a ∂μ, κ a ⟂ₘ η a) :
     μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by
@@ -54,7 +122,7 @@ lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α
   have hs : MeasurableSet s := Kernel.measurableSet_mutuallySingularSet κ η
   symm
   refine ⟨s, hs, ?_⟩
-  rw [Measure.compProd_apply hs, Measure.compProd_apply hs.compl]
+  rw [compProd_apply hs, compProd_apply hs.compl]
   have h_eq a : Prod.mk a ⁻¹' s = Kernel.mutuallySingularSetSlice κ η a := rfl
   have h1 a : η a (Prod.mk a ⁻¹' s) = 0 := by rw [h_eq, Kernel.measure_mutuallySingularSetSlice]
   have h2 : ∀ᵐ a ∂ μ, κ a (Prod.mk a ⁻¹' s)ᶜ = 0 := by
@@ -64,88 +132,56 @@ lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α
     exact ha
   simp [h1, lintegral_congr_ae h2]
 
-lemma Measure.mutuallySingular_compProd_right' [CountableOrCountablyGenerated α γ]
+lemma mutuallySingular_compProd_right'
     (μ ν : Measure α) {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η]
     (hκη : ∀ᵐ a ∂ν, κ a ⟂ₘ η a) :
     μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by
   by_cases hμ : SFinite μ
   swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
   by_cases hν : SFinite ν
   swap; · rw [compProd_of_not_sfinite _ _ hν]; simp
-  refine (Measure.mutuallySingular_compProd_right _ _ ?_).symm
-  simp_rw [Measure.MutuallySingular.comm, hκη]
+  refine (mutuallySingular_compProd_right _ _ ?_).symm
+  simp_rw [MutuallySingular.comm, hκη]
 
-lemma Measure.mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α}
-    [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η]
-    (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η) (hμ : ξ ≪ μ) (hν : ξ ≪ ν) :
-    ∀ᵐ x ∂ξ, κ x ⟂ₘ η x := by
-  have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet
-  have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet
-  have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet
-  rw [Measure.compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
-  · filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν
-    exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prod_mk_left hs, ⟨hxμ, hxν⟩⟩
-  · exact Kernel.measurable_kernel_prod_mk_left hs.compl |>.aemeasurable
-  · exact Kernel.measurable_kernel_prod_mk_left hs |>.aemeasurable
-  · exact hs.compl
-  · exact hs
-
-lemma Measure.mutuallySingular_compProd_iff_of_same_left
-    [CountableOrCountablyGenerated α γ] (μ : Measure α) [SFinite μ]
+lemma mutuallySingular_compProd_iff_of_same_left (μ : Measure α) [SFinite μ]
     (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
     μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ⟂ₘ η a := by
   refine ⟨fun h ↦ ?_, fun h ↦ mutuallySingular_compProd_right _ _ h⟩
   exact mutuallySingular_of_mutuallySingular_compProd h (fun _ a ↦ a) (fun _ a ↦ a)
 
-lemma Measure.mutuallySingular_compProd_iff_of_same_right (μ ν : Measure α) [IsFiniteMeasure μ]
-    [IsFiniteMeasure ν] (κ : Kernel α γ) [IsFiniteKernel κ] [hκ : ∀ x, NeZero (κ x)] :
-    μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν := by
-  refine ⟨fun h ↦ ?_, fun h ↦ mutuallySingular_compProd_left h _ _⟩
-  rw [← Measure.withDensity_rnDeriv_eq_zero]
-  have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_ (ξ  := ν.withDensity (∂μ/∂ν))
-  rotate_left
-  · exact Measure.absolutelyContinuous_of_le (μ.withDensity_rnDeriv_le ν)
-  · exact MeasureTheory.withDensity_absolutelyContinuous _ _
-  simp_rw [Measure.MutuallySingular.self_iff, (hκ _).ne] at hh
-  exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)
-
-variable [CountableOrCountablyGenerated α γ]
-
 section MeasureCompProd
 
-lemma Measure.absolutelyContinuous_kernel_of_compProd
+lemma absolutelyContinuous_kernel_of_compProd
     [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η]
     (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
     ∀ᵐ a ∂μ, κ a ≪ η a := by
   suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by
     filter_upwards [this] with a ha
     rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha
-  rw [← κ.rnDeriv_add_singularPart η, Measure.compProd_add_right,
-    Measure.AbsolutelyContinuous.add_left_iff] at h
+  rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h
   have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η :=
-    Measure.mutuallySingular_compProd_right μ ν
-      (.of_forall <| Kernel.mutuallySingular_singularPart _ _)
+    mutuallySingular_compProd_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _)
   have h_zero : μ ⊗ₘ κ.singularPart η = 0 :=
-    Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
-  simp_rw [← Measure.measure_univ_eq_zero]
+    eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
+  simp_rw [← measure_univ_eq_zero]
   refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_
-  rw [← setLIntegral_univ, ← Measure.compProd_apply_prod .univ .univ, h_zero]
+  rw [← setLIntegral_univ, ← compProd_apply_prod .univ .univ, h_zero]
   simp
 
-lemma Measure.absolutelyContinuous_compProd_iff
+lemma absolutelyContinuous_compProd_iff
     [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η] [∀ a, NeZero (κ a)] :
     μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a :=
-  ⟨fun h ↦ ⟨Measure.absolutelyContinuous_of_compProd h, absolutelyContinuous_kernel_of_compProd h⟩,
-    fun h ↦ Measure.absolutelyContinuous_compProd h.1 h.2⟩
+  ⟨fun h ↦ ⟨absolutelyContinuous_of_compProd h, absolutelyContinuous_kernel_of_compProd h⟩,
+    fun h ↦ absolutelyContinuous_compProd h.1 h.2⟩
 
-lemma Measure.absolutelyContinuous_compProd_right_iff
+lemma absolutelyContinuous_compProd_right_iff
     {μ : Measure α} {κ η : Kernel α γ} [SFinite μ] [IsFiniteKernel κ] [IsFiniteKernel η] :
     μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a :=
-  ⟨absolutelyContinuous_kernel_of_compProd, fun h ↦ Measure.absolutelyContinuous_compProd_right h⟩
+  ⟨absolutelyContinuous_kernel_of_compProd, fun h ↦ absolutelyContinuous_compProd_right h⟩
 
 end MeasureCompProd
 
-end MeasureTheory
+end MeasureTheory.Measure
 
 open MeasureTheory
 

TestingLowerBounds/ForMathlib/RNDerivEqCondexp.lean

@@ -46,4 +46,55 @@ lemma toReal_rnDeriv_comp [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ
   filter_upwards [Kernel.rnDeriv_measure_compProd_left μ ν κ] with x hx
   rw [hx]
 
+theorem _root_.Measurable.setLIntegral_kernel_prod_right' [IsSFiniteKernel κ]
+    {f : α × β → ℝ≥0∞} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
+    Measurable fun a => ∫⁻ b in s, f (a, b) ∂κ a := by
+  simp_rw [← Kernel.lintegral_restrict κ hs]; exact hf.lintegral_kernel_prod_right'
+
+lemma rnDeriv_compProd [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    (hμν : μ ≪ ν) [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η) :
+    (fun p ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p)
+      =ᵐ[ν ⊗ₘ η] (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) := by
+  have h_ac1 : μ ⊗ₘ κ ≪ ν ⊗ₘ η := Measure.absolutelyContinuous_compProd_of_compProd hμν h_ac
+  have h_meas : Measurable fun p ↦ (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p :=
+    ((Measure.measurable_rnDeriv _ _).comp measurable_fst).mul (Measure.measurable_rnDeriv _ _)
+  have h_eq t₁ t₂ : MeasurableSet t₁ → MeasurableSet t₂ →
+      ∫⁻ p in t₁ ×ˢ t₂, (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p ∂ν ⊗ₘ η
+        = ∫⁻ p in t₁ ×ˢ t₂, (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p ∂ν ⊗ₘ η := by
+    intro ht₁ ht₂
+    rw [Measure.setLIntegral_compProd h_meas ht₁ ht₂]
+    simp only
+    have : ∀ a, ∫⁻ b in t₂, (∂μ/∂ν) a * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) (a, b) ∂η a
+        = (∂μ/∂ν) a * ∫⁻ b in t₂, (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) (a, b) ∂η a := fun a ↦ by
+      rw [lintegral_const_mul]
+      exact (Measure.measurable_rnDeriv _ _).comp measurable_prod_mk_left
+    simp_rw [this]
+    rw [setLIntegral_rnDeriv_mul hμν _ ht₁]
+    swap
+    · exact ((Measure.measurable_rnDeriv _ _).setLIntegral_kernel_prod_right' ht₂).aemeasurable
+    rw [← Measure.setLIntegral_compProd (Measure.measurable_rnDeriv _ _) ht₁ ht₂,
+      Measure.setLIntegral_rnDeriv h_ac1, Measure.setLIntegral_rnDeriv h_ac]
+  refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite h_meas ?_ ?_
+  · exact Measure.measurable_rnDeriv _ _
+  · intro s hs _
+    apply induction_on_inter generateFrom_prod.symm isPiSystem_prod _ _ _ _ hs
+    · simp
+    · rintro _ ⟨t₁, ht₁, t₂, ht₂, rfl⟩
+      exact h_eq t₁ t₂ ht₁ ht₂
+    · intro t ht ht_eq
+      have h_ne_top : ∫⁻ p in t, (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p ∂ν ⊗ₘ η ≠ ⊤ := by
+        rw [Measure.setLIntegral_rnDeriv]
+        · exact measure_ne_top _ _
+        · exact h_ac1
+      rw [setLintegral_compl ht h_ne_top, setLintegral_compl ht, ht_eq]
+      swap; · rw [ht_eq]; exact h_ne_top
+      congr 1
+      have h := h_eq .univ .univ .univ .univ
+      simp only [univ_prod_univ, Measure.restrict_univ] at h
+      exact h
+    · intro f' hf_disj hf_meas hf_eq
+      rw [lintegral_iUnion hf_meas hf_disj, lintegral_iUnion hf_meas hf_disj]
+      congr with i
+      exact hf_eq i
+
 end ProbabilityTheory