prove fDiv_map_measurableEmbedding

TestingLowerBounds/FDiv.lean

@@ -499,14 +499,20 @@ lemma fDiv_map_measurableEmbedding [IsFiniteMeasure μ] [IsFiniteMeasure ν]
   · rw [fDiv_of_integrable h_int, fDiv_of_integrable]
     swap
     · rw [hg.integrable_map_iff]
-      sorry
+      refine (integrable_congr ?_).mpr h_int
+      filter_upwards [hg.rnDeriv_map μ ν] with a ha
+      simp [ha]
     rw [hg.integral_map]
     congr 2
     · refine integral_congr_ae ?_
-      sorry
-    · sorry
+      filter_upwards [hg.rnDeriv_map μ ν] with a ha
+      simp [ha]
+    · rw [hg.singularPart_map μ ν, hg.map_apply]
+      simp
   · rw [fDiv_of_not_integrable h_int, fDiv_of_not_integrable]
     rw [hg.integrable_map_iff]
-    sorry
+    rwa [(integrable_congr ?_)]
+    filter_upwards [hg.rnDeriv_map μ ν] with a ha
+    simp [ha]
 
 end ProbabilityTheory

TestingLowerBounds/ForMathlib/RnDeriv.lean

@@ -184,3 +184,78 @@ example [SigmaFinite μ] [SigmaFinite ν] :
   rfl
 
 end MeasureTheory.Measure
+
+namespace MeasurableEmbedding
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+  {μ ν : Measure α} {κ η : kernel α β} {f g : ℝ → ℝ}
+
+lemma _root_.MeasurableEmbedding.absolutelyContinuous_map (hμν : μ ≪ ν)
+    [SigmaFinite μ] [SigmaFinite ν]
+    {g : α → β} (hg : MeasurableEmbedding g) :
+    μ.map g ≪ ν.map g := by
+  intro t ht
+  rw [hg.map_apply] at ht ⊢
+  exact hμν ht
+
+lemma _root_.MeasurableEmbedding.mutuallySingular_map (hμν : μ ⟂ₘ ν)
+    [SigmaFinite μ] [SigmaFinite ν]
+    {g : α → β} (hg : MeasurableEmbedding g) :
+    μ.map g ⟂ₘ ν.map g := by
+  refine ⟨g '' hμν.nullSet, hg.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩
+  · rw [hg.map_apply, hg.injective.preimage_image, hμν.measure_nullSet]
+  · rw [hg.map_apply, Set.preimage_compl, hg.injective.preimage_image, hμν.measure_compl_nullSet]
+
+lemma _root_.MeasurableEmbedding.rnDeriv_map_aux (hμν : μ ≪ ν)
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    {g : α → β} (hg : MeasurableEmbedding g) :
+    (fun x ↦ (μ.map g).rnDeriv (ν.map g) (g x)) =ᵐ[ν] μ.rnDeriv ν := by
+  refine ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)
+  · exact (Measure.measurable_rnDeriv _ _).comp hg.measurable
+  · exact Measure.measurable_rnDeriv _ _
+  rw [← hg.lintegral_map, Measure.set_lintegral_rnDeriv hμν]
+  have hs_eq : s = g ⁻¹' (g '' s) := by rw [hg.injective.preimage_image]
+  rw [hs_eq, ← hg.restrict_map, Measure.set_lintegral_rnDeriv (hg.absolutelyContinuous_map hμν),
+    hg.map_apply]
+
+lemma _root_.MeasurableEmbedding.rnDeriv_map (μ ν : Measure α)
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    {g : α → β} (hg : MeasurableEmbedding g) :
+    (fun x ↦ (μ.map g).rnDeriv (ν.map g) (g x)) =ᵐ[ν] μ.rnDeriv ν := by
+  rw [μ.haveLebesgueDecomposition_add ν, Measure.map_add _ _ hg.measurable]
+  have h_add := Measure.rnDeriv_add ((μ.singularPart ν).map g) ((ν.withDensity (μ.rnDeriv ν)).map g)
+    (ν.map g)
+  rw [EventuallyEq, hg.ae_map_iff, ← EventuallyEq] at h_add
+  refine h_add.trans ((Measure.rnDeriv_add _ _ _).trans ?_).symm
+  refine EventuallyEq.add ?_ ?_
+  · refine (Measure.rnDeriv_singularPart μ ν).trans ?_
+    symm
+    suffices (fun x ↦ ((μ.singularPart ν).map g).rnDeriv (ν.map g) x) =ᵐ[ν.map g] 0 by
+      rw [EventuallyEq, hg.ae_map_iff] at this
+      exact this
+    refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl
+    exact hg.mutuallySingular_map (μ.mutuallySingular_singularPart ν)
+  · exact (hg.rnDeriv_map_aux (withDensity_absolutelyContinuous _ _)).symm
+
+lemma _root_.MeasurableEmbedding.map_withDensity_rnDeriv (μ ν : Measure α)
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    {g : α → β} (hg : MeasurableEmbedding g) :
+    (ν.withDensity (μ.rnDeriv ν)).map g = (ν.map g).withDensity ((μ.map g).rnDeriv (ν.map g)) := by
+  ext s hs
+  rw [hg.map_apply, withDensity_apply _ (hg.measurable hs), withDensity_apply _ hs,
+    set_lintegral_map hs (Measure.measurable_rnDeriv _ _) hg.measurable]
+  refine set_lintegral_congr_fun (hg.measurable hs) ?_
+  filter_upwards [hg.rnDeriv_map μ ν] with a ha _ using ha.symm
+
+lemma _root_.MeasurableEmbedding.singularPart_map (μ ν : Measure α)
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    {g : α → β} (hg : MeasurableEmbedding g) :
+    (μ.map g).singularPart (ν.map g) = (μ.singularPart ν).map g := by
+  have h_add : μ.map g = (μ.singularPart ν).map g
+      + (ν.map g).withDensity ((μ.map g).rnDeriv (ν.map g)) := by
+    conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
+    rw [Measure.map_add _ _ hg.measurable, ← hg.map_withDensity_rnDeriv μ ν]
+  refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm
+  exact hg.mutuallySingular_map (μ.mutuallySingular_singularPart ν)
+
+end MeasurableEmbedding

blueprint/src/sections/f_divergence.tex

@@ -112,7 +112,7 @@ \section{Definition and basic properties}
   Let $\mu$ and $\nu$ be two measures on $\mathcal X$ and let $g : \mathcal X \to \mathcal Y$ be a measurable embedding. Then $D_f(g \cdot \mu, g \cdot \nu) = D_f(\mu, \nu)$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
 \end{proof}
 
 \section{Conditional f-divergence}