diff --git a/TestingLowerBounds/FDiv.lean b/TestingLowerBounds/FDiv.lean
index 43f38091..7327d74a 100644
--- a/TestingLowerBounds/FDiv.lean
+++ b/TestingLowerBounds/FDiv.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.MeasureTheory.Measure.Tilted
+import TestingLowerBounds.ForMathlib.EReal
 import Mathlib.Analysis.Convex.Integral
 import Mathlib.Analysis.Calculus.MeanValue
 import TestingLowerBounds.SoonInMathlib.RadonNikodym
@@ -45,78 +45,309 @@ Most results will require these conditions on `f`:
 Foobars, barfoos
 -/
 
-open Real MeasureTheory
+open Real MeasureTheory Filter
 
-open scoped ENNReal
+open scoped ENNReal NNReal
 
 namespace ProbabilityTheory
 
 variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
   {μ ν : Measure α} {κ η : kernel α β} {f g : ℝ → ℝ}
 
-/-- f-Divergence of two measures, real-valued. -/
+lemma integrable_toReal_iff {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
+    Integrable (fun x ↦ (f x).toReal) μ ↔ ∫⁻ x, f x ∂μ ≠ ∞ := by
+  refine ⟨fun h ↦ ?_, fun h ↦ integrable_toReal_of_lintegral_ne_top hf h⟩
+  rw [Integrable, HasFiniteIntegral] at h
+  have : ∀ᵐ x ∂μ, f x = ↑‖(f x).toReal‖₊ := by
+    filter_upwards [hf_ne_top] with x hx
+    rw [← ofReal_norm_eq_coe_nnnorm, norm_of_nonneg ENNReal.toReal_nonneg, ENNReal.ofReal_toReal hx]
+  rw [lintegral_congr_ae this]
+  exact h.2.ne
+
+-- we put the coe outside the limsup to ensure it's not ⊥
+open Classical in
 noncomputable
-def fDivReal (f : ℝ → ℝ) (μ ν : Measure α) : ℝ := ∫ x, f (μ.rnDeriv ν x).toReal ∂ν
+def derivInfty (f : ℝ → ℝ) : EReal :=
+  if Tendsto (fun x ↦ f x / x) atTop atTop then ⊤ else ↑(limsup (fun x ↦ f x / x) atTop)
+
+lemma bot_lt_derivInfty : ⊥ < derivInfty f := by
+  rw [derivInfty]
+  split_ifs with h <;> simp
+
+lemma derivInfty_ne_bot : derivInfty f ≠ ⊥ := bot_lt_derivInfty.ne'
+
+@[simp]
+lemma derivInfty_const (c : ℝ) : derivInfty (fun _ ↦ c) = 0 := by
+  sorry
+
+@[simp]
+lemma derivInfty_id : derivInfty id = 1 := by
+  rw [derivInfty, if_neg]
+  · norm_cast
+    sorry
+  · sorry
+
+@[simp]
+lemma derivInfty_id' : derivInfty (fun x ↦ x) = 1 := derivInfty_id
+
+lemma derivInfty_add : derivInfty (fun x ↦ f x + g x) = derivInfty f + derivInfty g := by
+  sorry
+
+lemma derivInfty_add' : derivInfty (f + g) = derivInfty f + derivInfty g := by
+  sorry
+
+lemma derivInfty_const_mul (c : ℝ) :
+    derivInfty (fun x ↦ c * f x) = c * derivInfty f := by
+  sorry
+
+lemma le_add_derivInfty (h_cvx : ConvexOn ℝ (Set.Ici 0) f)
+    (h : ¬ Tendsto (fun x ↦ f x / x) atTop atTop) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
+    f x ≤ f y + (derivInfty f).toReal * (x - y) := by
+  sorry
+
+lemma le_add_derivInfty' (h_cvx : ConvexOn ℝ (Set.Ici 0) f)
+    (h : ¬ Tendsto (fun x ↦ f x / x) atTop atTop) {x u : ℝ} (hx : 0 ≤ x) (hu : 0 ≤ u) :
+    f x ≤ f (u * x) + (derivInfty f).toReal * x * (1 - u) := by
+  sorry
 
 open Classical in
-/-- f-Divergence of two measures, with value in `ℝ≥0∞`. Suitable for probability measures. -/
+/-- f-Divergence of two measures, real-valued.
+
+todo: if we add convexity in the hypotheses, then the if is not needed anymore for finite measures?
+
+todo: right now if f is not integrable because the integral tends to -∞ we don't have the natural
+value. But for convex functions and finite measures we don't care.
+-/
 noncomputable
-def fDiv (f : ℝ → ℝ) (μ ν : Measure α) : ℝ≥0∞ :=
-  if Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν then ENNReal.ofReal (fDivReal f μ ν) else ∞
+def fDivReal (f : ℝ → ℝ) (μ ν : Measure α) : EReal :=
+  if ¬ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν then ⊤
+  else ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivInfty f * μ.singularPart ν Set.univ
 
-lemma fDivReal_of_not_integrable (hf : ¬ Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) :
-    fDivReal f μ ν = 0 := by
-  rw [fDivReal, integral_undef hf]
+lemma fDivReal_of_not_integrable (hf : ¬ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν = ⊤ := if_pos hf
 
-lemma fDivReal_const (c : ℝ) (μ ν : Measure α) :
-    fDivReal (fun _ ↦ c) μ ν = (ν Set.univ).toReal * c := by
-  rw [fDivReal, integral_const, smul_eq_mul]
+lemma fDivReal_of_integrable (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivInfty f * μ.singularPart ν Set.univ :=
+  if_neg (not_not.mpr hf)
 
-lemma fDivReal_id [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
-    fDivReal id μ ν = (μ Set.univ).toReal := by
-  simp only [fDivReal, id_eq, Measure.integral_toReal_rnDeriv hμν]
+lemma fDivReal_of_eq_top (h : derivInfty f * μ.singularPart ν Set.univ = ⊤) :
+    fDivReal f μ ν = ⊤ := by
+  by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+  · rw [fDivReal, if_neg (not_not.mpr hf), h, EReal.coe_add_top]
+  · exact fDivReal_of_not_integrable hf
 
-lemma fDivReal_id' [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
-    fDivReal (fun x ↦ x) μ ν = (μ Set.univ).toReal := fDivReal_id hμν
+@[simp]
+lemma fDivReal_zero (μ ν : Measure α) : fDivReal (fun _ ↦ 0) μ ν = 0 := by
+  rw [fDivReal]
+  simp
 
-lemma fDivReal_mul (c : ℝ) (f : ℝ → ℝ) (μ ν : Measure α) :
+@[simp]
+lemma fDivReal_const (c : ℝ) (μ ν : Measure α) [IsFiniteMeasure ν] :
+    fDivReal (fun _ ↦ c) μ ν = ν Set.univ * c := by
+  rw [fDivReal_of_integrable (integrable_const c), integral_const]
+  simp only [smul_eq_mul, EReal.coe_mul, derivInfty_const, zero_mul, add_zero]
+  congr
+  rw [EReal.coe_ennreal_toReal]
+  exact measure_ne_top _ _
+
+@[simp]
+lemma fDivReal_const' {c : ℝ} (hc : 0 ≤ c) (μ ν : Measure α) :
+    fDivReal (fun _ ↦ c) μ ν = ν Set.univ * c := by
+  by_cases hν : IsFiniteMeasure ν
+  · exact fDivReal_const c μ ν
+  · have : ν Set.univ = ∞ := by
+      by_contra h_univ
+      exact absurd ⟨Ne.lt_top h_univ⟩ hν
+    rw [this]
+    by_cases hc0 : c = 0
+    · simp [hc0]
+    rw [fDivReal_of_not_integrable]
+    · simp only [EReal.coe_ennreal_top]
+      rw [EReal.top_mul_of_pos]
+      refine lt_of_le_of_ne ?_ (Ne.symm ?_)
+      · exact mod_cast hc
+      · exact mod_cast hc0
+    · rw [integrable_const_iff]
+      simp [hc0, this]
+
+lemma fDivReal_of_mutuallySingular [SigmaFinite μ] [IsFiniteMeasure ν] (h : μ ⟂ₘ ν) :
+    fDivReal f μ ν = (f 0 : EReal) * ν Set.univ + derivInfty f * μ Set.univ := by
+  have : μ.singularPart ν = μ := (μ.singularPart_eq_self ν).mpr h
+  have hf_rnDeriv : (fun x ↦ f ((∂μ/∂ν) x).toReal) =ᵐ[ν] fun _ ↦ f 0 := by
+    filter_upwards [Measure.rnDeriv_eq_zero_of_mutuallySingular h Measure.AbsolutelyContinuous.rfl]
+      with x hx using by simp [hx]
+  have h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by
+      rw [integrable_congr hf_rnDeriv]
+      exact integrable_const _
+  rw [fDivReal_of_integrable h_int, integral_congr_ae hf_rnDeriv]
+  simp only [integral_const, smul_eq_mul, EReal.coe_mul, this]
+  rw [mul_comm]
+  congr
+  rw [EReal.coe_ennreal_toReal]
+  exact measure_ne_top _ _
+
+lemma fDivReal_of_absolutelyContinuous [SigmaFinite μ] [SigmaFinite ν]
+    [Decidable (Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)] (h : μ ≪ ν) :
+    fDivReal f μ ν = if Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+      then (↑(∫ x, f ((∂μ/∂ν) x).toReal ∂ν) : EReal) else ⊤ := by
+  split_ifs with h_int
+  · rw [fDivReal_of_integrable h_int, Measure.singularPart_eq_zero_of_ac h]
+    simp only [Measure.zero_toOuterMeasure, OuterMeasure.coe_zero, Pi.zero_apply, mul_zero,
+      ENNReal.zero_toReal, add_zero]
+    simp [Measure.singularPart_eq_zero_of_ac h]
+  · rw [fDivReal_of_not_integrable h_int]
+
+lemma fDivReal_add_const
+    (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν] (c : ℝ) :
+    fDivReal (fun x ↦ f x + c) μ ν = fDivReal f μ ν + c * ν Set.univ := by
+  by_cases hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+  · rw [fDivReal_of_integrable hf_int, fDivReal_of_integrable]
+    swap; · exact hf_int.add (integrable_const _)
+    rw [integral_add hf_int (integrable_const _)]
+    simp only [integral_const, smul_eq_mul, EReal.coe_add, EReal.coe_mul]
+    rw [add_assoc, add_assoc]
+    congr 1
+    rw [add_comm, derivInfty_add, derivInfty_const, add_zero]
+    congr 1
+    rw [mul_comm]
+    congr
+    rw [EReal.coe_ennreal_toReal]
+    exact measure_ne_top _ _
+  · rw [fDivReal_of_not_integrable hf_int, fDivReal_of_not_integrable]
+    · sorry
+    · have : (fun x ↦ f ((∂μ/∂ν) x).toReal) = (fun x ↦ (f ((∂μ/∂ν) x).toReal + c) - c) := by
+        ext; simp
+      rw [this] at hf_int
+      exact fun h_int ↦ hf_int (h_int.sub (integrable_const _))
+
+lemma fDivReal_sub_const
+    (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν] (c : ℝ) :
+    fDivReal (fun x ↦ f x - c) μ ν = fDivReal f μ ν - c * ν Set.univ := by
+  have : f = fun x ↦ (f x - c) + c := by ext; simp
+  conv_rhs => rw [this, fDivReal_add_const]
+  sorry
+
+lemma fDivReal_eq_add_withDensity_singularPart
+    (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν]
+    (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν = fDivReal f (ν.withDensity (∂μ/∂ν)) ν + fDivReal f (μ.singularPart ν) ν
+      - f 0 * ν Set.univ := by
+  have h_int_iff : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+      ↔ Integrable (fun x ↦ f ((∂(ν.withDensity (∂μ/∂ν))/∂ν) x).toReal) ν := by
+    refine integrable_congr ?_
+    filter_upwards [Measure.rnDeriv_withDensity ν (μ.measurable_rnDeriv ν)] with x hx
+    rw [hx]
+  classical
+  rw [fDivReal_of_mutuallySingular (Measure.mutuallySingular_singularPart _ _)]
+  by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+  · rw [fDivReal_of_absolutelyContinuous (withDensity_absolutelyContinuous _ _), if_pos,
+      fDivReal_of_integrable hf]
+    swap
+    · exact h_int_iff.mp hf
+    rw [add_sub_assoc]
+    congr 2
+    · refine integral_congr_ae ?_
+      filter_upwards [Measure.rnDeriv_withDensity ν (μ.measurable_rnDeriv ν)] with x hx
+      rw [hx]
+    sorry
+  · rw [fDivReal_of_not_integrable hf, fDivReal_of_not_integrable]
+    · sorry
+    · rwa [← h_int_iff]
+
+lemma fDivReal_eq_add_withDensity_singularPart'
+    (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν]
+    (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν = fDivReal (fun x ↦ f x - f 0) (ν.withDensity (∂μ/∂ν)) ν
+      + fDivReal f (μ.singularPart ν) ν := by
+  rw [fDivReal_eq_add_withDensity_singularPart _ _ hf, fDivReal_sub_const, add_sub_assoc,
+    sub_eq_add_neg, sub_eq_add_neg, add_assoc]
+  congr 1
+  rw [add_comm]
+
+lemma fDivReal_eq_add_withDensity_singularPart''
+    (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν]
+    (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν = fDivReal f (ν.withDensity (∂μ/∂ν)) ν
+      + fDivReal (fun x ↦ f x - f 0) (μ.singularPart ν) ν := by
+  rw [fDivReal_eq_add_withDensity_singularPart _ _ hf, fDivReal_sub_const, add_sub_assoc,
+    sub_eq_add_neg]
+
+lemma fDivReal_id (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    fDivReal id μ ν = μ Set.univ := by
+  by_cases h_int : Integrable (fun x ↦ ((∂μ/∂ν) x).toReal) ν
+  · rw [fDivReal_of_integrable h_int]
+    simp only [id_eq, derivInfty_id, one_mul]
+    rw [← integral_univ, Measure.set_integral_toReal_rnDeriv_eq_withDensity]
+    have h_lt_top : (Measure.withDensity ν (∂μ/∂ν)) Set.univ < ∞ := by
+      sorry -- use h_int
+    sorry
+  · rw [fDivReal_of_not_integrable h_int]
+    norm_cast
+    symm
+    by_contra h_ne_top
+    have : IsFiniteMeasure μ := ⟨Ne.lt_top ?_⟩
+    swap; · rw [← EReal.coe_ennreal_top] at h_ne_top; exact mod_cast h_ne_top
+    refine h_int ?_
+    refine integrable_toReal_of_lintegral_ne_top (μ.measurable_rnDeriv ν).aemeasurable ?_
+    exact (Measure.lintegral_rnDeriv_lt_top _ _).ne
+
+lemma fDivReal_id' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    fDivReal (fun x ↦ x) μ ν = μ Set.univ := fDivReal_id μ ν
+
+lemma fDivReal_mul {c : ℝ} (hc : 0 ≤ c) (f : ℝ → ℝ) (μ ν : Measure α) :
     fDivReal (fun x ↦ c * f x) μ ν = c * fDivReal f μ ν := by
-  rw [fDivReal, integral_mul_left, fDivReal]
+  by_cases hc0 : c = 0
+  · simp [hc0]
+  by_cases h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+  · rw [fDivReal_of_integrable h_int, fDivReal_of_integrable]
+    swap; · exact h_int.const_mul _
+    rw [integral_mul_left, derivInfty_const_mul]
+    simp only [EReal.coe_mul]
+    sorry
+  · rw [fDivReal_of_not_integrable h_int, fDivReal_of_not_integrable]
+    · rw [EReal.mul_top_of_pos]
+      norm_cast
+      exact lt_of_le_of_ne hc (Ne.symm hc0)
+    · refine fun h ↦ h_int ?_
+      have : (fun x ↦ f ((∂μ/∂ν) x).toReal) = (fun x ↦ c⁻¹ * (c * f ((∂μ/∂ν) x).toReal)) := by
+        ext; rw [← mul_assoc, inv_mul_cancel hc0, one_mul]
+      rw [this]
+      exact h.const_mul _
 
 -- TODO: in the case where both functions are convex, integrability of the sum is equivalent to
 -- integrability of both, and we don't need hf and hg.
 lemma fDivReal_add (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
     (hg : Integrable (fun x ↦ g ((∂μ/∂ν) x).toReal) ν) :
     fDivReal (fun x ↦ f x + g x) μ ν = fDivReal f μ ν + fDivReal g μ ν := by
-  rw [fDivReal, integral_add hf hg, fDivReal, fDivReal]
-
--- TODO: in the case where both functions are convex, integrability of the sum is equivalent to
--- integrability of both, and we don't need hf and hg.
-lemma fDivReal_sub (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
-    (hg : Integrable (fun x ↦ g ((∂μ/∂ν) x).toReal) ν) :
-    fDivReal (fun x ↦ f x - g x) μ ν = fDivReal f μ ν - fDivReal g μ ν := by
-  rw [fDivReal, integral_sub hf hg, fDivReal, fDivReal]
-
-lemma fDivReal_withDensity_rnDeriv (μ ν : Measure α) [SigmaFinite ν] :
-    fDivReal f (ν.withDensity (∂μ/∂ν)) ν = fDivReal f μ ν := by
-  refine integral_congr_ae ?_
-  filter_upwards [Measure.rnDeriv_withDensity ν (Measure.measurable_rnDeriv μ ν)] with a ha
-  rw [ha]
+  rw [fDivReal_of_integrable (hf.add hg), integral_add hf hg, fDivReal_of_integrable hf,
+    fDivReal_of_integrable hg, derivInfty_add]
+  simp only [EReal.coe_add]
+  rw [add_assoc, add_assoc]
+  congr 1
+  conv_rhs => rw [← add_assoc, add_comm, ← add_assoc, add_comm]
+  congr 1
+  sorry
 
-lemma fDivReal_add_linear' (c : ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ ≪ ν)
+lemma fDivReal_add_linear' {c : ℝ} (hc : 0 ≤ c) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     fDivReal (fun x ↦ f x + c * (x - 1)) μ ν
       = fDivReal f μ ν + c * ((μ Set.univ).toReal - (ν Set.univ).toReal) := by
   rw [fDivReal_add hf]
-  · rw [fDivReal_mul, fDivReal_sub Measure.integrable_toReal_rnDeriv (integrable_const _),
-      fDivReal_const, fDivReal_id' hμν, mul_one]
+  · simp_rw [sub_eq_add_neg]
+    rw [fDivReal_mul hc, fDivReal_add Measure.integrable_toReal_rnDeriv (integrable_const _),
+      fDivReal_const, fDivReal_id']
+    simp only [EReal.coe_neg, EReal.coe_one, mul_neg, mul_one]
+    congr
+    · sorry
+    · sorry
   · exact (Measure.integrable_toReal_rnDeriv.sub (integrable_const _)).const_mul c
 
-lemma fDivReal_add_linear (c : ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ ≪ ν)
+lemma fDivReal_add_linear {c : ℝ} (hc : 0 ≤ c) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (h_eq : μ Set.univ = ν Set.univ) :
     fDivReal (fun x ↦ f x + c * (x - 1)) μ ν = fDivReal f μ ν := by
   by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
-  · rw [fDivReal_add_linear' c hμν hf, h_eq, sub_self, mul_zero, add_zero]
+  · rw [fDivReal_add_linear' hc hf, h_eq, ← EReal.coe_sub, sub_self]
+    simp
   · rw [fDivReal_of_not_integrable hf,fDivReal_of_not_integrable]
     refine fun h_int ↦ hf ?_
     have : (fun x ↦ f ((∂μ/∂ν) x).toReal)
@@ -127,62 +358,188 @@ lemma fDivReal_add_linear (c : ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h
     rw [this]
     exact h_int.add ((Measure.integrable_toReal_rnDeriv.sub (integrable_const _)).const_mul c).neg
 
+lemma fDivReal_self (hf_one : f 1 = 0) (μ : Measure α) [SigmaFinite μ] : fDivReal f μ μ = 0 := by
+  have h : (fun x ↦ f (μ.rnDeriv μ x).toReal) =ᵐ[μ] 0 := by
+    filter_upwards [Measure.rnDeriv_self μ] with x hx
+    rw [hx, ENNReal.one_toReal, hf_one]
+    rfl
+  rw [fDivReal_of_integrable]
+  swap; · rw [integrable_congr h]; exact integrable_zero _ _ _
+  rw [integral_congr_ae h]
+  simp only [Pi.zero_apply, integral_zero, EReal.coe_zero, zero_add]
+  rw [Measure.singularPart_self]
+  simp
+
+lemma fDivReal_lt_top_of_ac [SigmaFinite μ] [SigmaFinite ν] (h : μ ≪ ν)
+    (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν < ⊤ := by
+  classical
+  rw [fDivReal_of_absolutelyContinuous h, if_pos h_int]
+  simp
+
+section DerivInftyTop
+
+lemma fDivReal_of_not_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivInfty f = ⊤) (hμν : ¬ μ ≪ ν) :
+    fDivReal f μ ν = ⊤ := by
+  rw [fDivReal]
+  split_ifs with h_int
+  · rw [hf]
+    suffices Measure.singularPart μ ν Set.univ ≠ 0 by
+      rw [EReal.top_mul_of_pos, EReal.coe_add_top]
+      refine lt_of_le_of_ne (EReal.coe_ennreal_nonneg _) ?_
+      exact mod_cast this.symm
+    simp only [ne_eq, Measure.measure_univ_eq_zero]
+    rw [Measure.singularPart_eq_zero]
+    exact hμν
+  · rfl
+
+lemma fDivReal_lt_top_iff_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivInfty f = ⊤)
+    (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν < ⊤ ↔ μ ≪ ν := by
+  refine ⟨fun h ↦ ?_, fun h ↦ fDivReal_lt_top_of_ac h h_int⟩
+  by_contra h_not_ac
+  refine h.ne (fDivReal_of_not_ac hf h_not_ac)
+
+lemma fDivReal_ne_top_iff_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivInfty f = ⊤)
+    (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν ≠ ⊤ ↔ μ ≪ ν := by
+  rw [← fDivReal_lt_top_iff_ac hf h_int, lt_top_iff_ne_top]
+
+lemma fDivReal_eq_top_iff_not_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivInfty f = ⊤)
+    (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν = ⊤ ↔ ¬ μ ≪ ν := by
+  rw [← fDivReal_ne_top_iff_ac hf h_int, not_not]
+
+lemma fDivReal_of_derivInfty_eq_top [SigmaFinite μ] [SigmaFinite ν] (hf : derivInfty f = ⊤)
+    [Decidable (Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν ∧ μ ≪ ν)] :
+    fDivReal f μ ν = if (Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν ∧ μ ≪ ν)
+      then ((∫ x, f ((∂μ/∂ν) x).toReal ∂ν : ℝ) : EReal)
+      else ⊤ := by
+  split_ifs with h
+  · rw [fDivReal_of_integrable h.1, Measure.singularPart_eq_zero_of_ac h.2]
+    simp
+  · push_neg at h
+    by_cases hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+    · exact fDivReal_of_not_ac hf (h hf_int)
+    · exact fDivReal_of_not_integrable hf_int
+
+end DerivInftyTop
+
+lemma fDivReal_lt_top_of_derivInfty_ne_top [IsFiniteMeasure μ] [SigmaFinite ν]
+    (hf : derivInfty f ≠ ⊤) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
+    fDivReal f μ ν < ⊤ := by
+  rw [fDivReal_of_integrable h_int]
+  refine EReal.add_lt_top ?_ ?_
+  · simp
+  · have : μ.singularPart ν Set.univ < (⊤ : EReal) := by
+      rw [← EReal.coe_ennreal_top]
+      norm_cast
+      exact measure_lt_top _ _
+    rw [ne_eq, EReal.mul_eq_top]
+    simp only [derivInfty_ne_bot, false_and, EReal.coe_ennreal_ne_bot, and_false, hf,
+      EReal.coe_ennreal_pos, Measure.measure_univ_pos, ne_eq, EReal.coe_ennreal_eq_top_iff,
+      false_or, not_and]
+    exact fun _ ↦ measure_ne_top _ _
+
+lemma fDivReal_lt_top_iff_of_derivInfty_ne_top [IsFiniteMeasure μ] [SigmaFinite ν]
+    (hf : derivInfty f ≠ ⊤) :
+    fDivReal f μ ν < ⊤ ↔ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by
+  refine ⟨fun h ↦ ?_, fDivReal_lt_top_of_derivInfty_ne_top hf⟩
+  by_contra h_not_int
+  rw [fDivReal_of_not_integrable h_not_int] at h
+  simp at h
+
+lemma fDivReal_ne_top_iff_of_derivInfty_ne_top [IsFiniteMeasure μ] [SigmaFinite ν]
+    (hf : derivInfty f ≠ ⊤) :
+    fDivReal f μ ν ≠ ⊤ ↔ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by
+  rw [← fDivReal_lt_top_iff_of_derivInfty_ne_top hf, lt_top_iff_ne_top]
+
+lemma fDivReal_eq_top_iff_of_derivInfty_ne_top [IsFiniteMeasure μ] [SigmaFinite ν]
+    (hf : derivInfty f ≠ ⊤) :
+    fDivReal f μ ν = ⊤ ↔ ¬ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by
+  rw [← fDivReal_ne_top_iff_of_derivInfty_ne_top hf, not_not]
+
+lemma fDivReal_eq_top_iff [IsFiniteMeasure μ] [SigmaFinite ν] :
+    fDivReal f μ ν = ⊤
+      ↔ (¬ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) ∨ (derivInfty f = ⊤ ∧ ¬ μ ≪ ν) := by
+  by_cases h : derivInfty f = ⊤
+  · simp only [h, true_and]
+    by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
+    · simp only [hf, not_true_eq_false, false_or]
+      exact fDivReal_eq_top_iff_not_ac h hf
+    · simp [hf, fDivReal_of_not_integrable hf]
+  · simp only [h, false_and, or_false]
+    exact fDivReal_eq_top_iff_of_derivInfty_ne_top h
+
+lemma fDivReal_ne_top_iff [IsFiniteMeasure μ] [SigmaFinite ν] :
+    fDivReal f μ ν ≠ ⊤
+      ↔ (Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) ∧ (derivInfty f = ⊤ → μ ≪ ν) := by
+  rw [ne_eq, fDivReal_eq_top_iff]
+  push_neg
+  rfl
+
+lemma integrable_of_fDivReal_ne_top (h : fDivReal f μ ν ≠ ⊤) :
+    Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by
+  by_contra h_not
+  exact h (fDivReal_of_not_integrable h_not)
+
+lemma fDivReal_of_ne_top (h : fDivReal f μ ν ≠ ⊤) :
+    fDivReal f μ ν = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivInfty f * μ.singularPart ν Set.univ := by
+  rw [fDivReal_of_integrable]
+  exact integrable_of_fDivReal_ne_top h
+
+/-
+-- todo: extend beyond μ ≪ ν
 lemma le_fDivReal [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
     (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
-    (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) (hμν : μ ≪ ν) :
+    (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) (hμν : μ ≪ ν) :
     f (μ Set.univ).toReal ≤ fDivReal f μ ν := by
+  classical
+  rw [fDivReal_of_absolutelyContinuous hμν, if_pos hf_int]
   calc f (μ Set.univ).toReal
-    = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
-  _ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by
+    = f (∫ x, ((∂μ/∂ν) x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
+  _ ≤ ∫ x, f ((∂μ/∂ν) x).toReal ∂ν := by
     rw [← average_eq_integral, ← average_eq_integral]
     exact ConvexOn.map_average_le hf_cvx hf_cont isClosed_Ici (by simp)
       Measure.integrable_toReal_rnDeriv hf_int
-  _ = ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := rfl
+  _ = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν := rfl
 
 lemma fDivReal_nonneg [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
     (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0)
-    (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) (hμν : μ ≪ ν) :
+    (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) (hμν : μ ≪ ν) :
     0 ≤ fDivReal f μ ν :=
   calc 0 = f (μ Set.univ).toReal := by simp [hf_one]
-  _ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := le_fDivReal hf_cvx hf_cont hf_int hμν
-
-lemma fDivReal_self (hf_one : f 1 = 0) (μ : Measure α) [SigmaFinite μ] : fDivReal f μ μ = 0 := by
-  have h : (fun x ↦ f (μ.rnDeriv μ x).toReal) =ᵐ[μ] 0 := by
-    filter_upwards [Measure.rnDeriv_self μ] with x hx
-    rw [hx, ENNReal.one_toReal, hf_one]
-    rfl
-  rw [fDivReal, integral_congr_ae h]
-  simp
+  _ ≤ ∫ x, f ((∂μ/∂ν) x).toReal ∂ν := le_fDivReal hf_cvx hf_cont hf_int hμν
+-/
 
 section Conditional
 
 open Classical in
-/- Conditinal f-divergence.
-
-We enforce `∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a)`, to ensure
-that `condFDivReal f κ η μ` and `fDivReal f (μ ⊗ₘ κ) (μ ⊗ₘ η)` are well defined under the same
-conditions (these two quantities are then always equal). -/
+/- Conditinal f-divergence. -/
 noncomputable
-def condFDivReal (f : ℝ → ℝ) (κ η : kernel α β) (μ : Measure α) : ℝ :=
-  if ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a)
-  then μ[fun x ↦ fDivReal f (κ x) (η x)]
-  else 0
-
-lemma condFDivReal_of_not_ae_integrable
-    (hf : ¬ ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a)) :
-    condFDivReal f κ η μ = 0 := by
-  rw [condFDivReal, if_neg hf]
-
-lemma condFDivReal_eq
-    (hf : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a)) :
-    condFDivReal f κ η μ = μ[fun x ↦ fDivReal f (κ x) (η x)] :=
-  if_pos hf
-
-lemma condFDivReal_of_not_integrable (hf : ¬ Integrable (fun x ↦ fDivReal f (κ x) (η x)) μ) :
-    condFDivReal f κ η μ = 0 := by
-  by_cases hf' : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a)
-  · rw [condFDivReal, if_pos hf', integral_undef hf]
-  · exact condFDivReal_of_not_ae_integrable hf'
+def condFDivReal (f : ℝ → ℝ) (κ η : kernel α β) (μ : Measure α) : EReal :=
+  if (∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤)
+    ∧ (Integrable (fun x ↦ (fDivReal f (κ x) (η x)).toReal) μ)
+  then ((μ[fun x ↦ (fDivReal f (κ x) (η x)).toReal] : ℝ) : EReal)
+  else ⊤
+
+lemma condFDivReal_of_not_ae_finite (hf : ¬ ∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤) :
+    condFDivReal f κ η μ = ⊤ := by
+  rw [condFDivReal, if_neg]
+  push_neg
+  exact fun h ↦ absurd h hf
+
+lemma condFDivReal_of_not_integrable
+    (hf : ¬ Integrable (fun x ↦ (fDivReal f (κ x) (η x)).toReal) μ) :
+    condFDivReal f κ η μ = ⊤ := by
+  rw [condFDivReal, if_neg]
+  push_neg
+  exact fun _ ↦ hf
+
+lemma condFDivReal_eq (hf_ae : ∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤)
+    (hf : Integrable (fun x ↦ (fDivReal f (κ x) (η x)).toReal) μ) :
+    condFDivReal f κ η μ = ((μ[fun x ↦ (fDivReal f (κ x) (η x)).toReal] : ℝ) : EReal) :=
+  if_pos ⟨hf_ae, hf⟩
 
 variable [MeasurableSpace.CountablyGenerated β]
 
@@ -210,34 +567,6 @@ theorem _root_.MeasureTheory.Integrable.integral_compProd' [NormedAddCommGroup E
     Integrable (fun x ↦ ∫ y, f (x, y) ∂(κ x)) μ :=
   hf.integral_compProd
 
-lemma integrable_f_rnDeriv_of_integrable_compProd [IsFiniteMeasure μ] [IsFiniteKernel κ]
-    [IsFiniteKernel η] (hf : StronglyMeasurable f)
-    (hf_int : Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x).toReal) (μ ⊗ₘ η)) :
-    ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a) := by
-  have h := hf_int.integral_compProd'
-  rw [Measure.integrable_compProd_iff] at hf_int
-  swap
-  · exact (hf.comp_measurable (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable
-  have h := kernel.rnDeriv_measure_compProd_right' μ κ η
-  filter_upwards [h, hf_int.1] with a ha1 ha2
-  refine (integrable_congr ?_).mp ha2
-  filter_upwards [ha1] with b hb
-  rw [hb]
-
-lemma integrable_fDivReal_of_integrable_compProd [IsFiniteMeasure μ] [IsFiniteKernel κ]
-    [IsFiniteKernel η]
-    (hf_int : Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x).toReal) (μ ⊗ₘ η)) :
-    Integrable (fun x ↦ fDivReal f (κ x) (η x)) μ := by
-  have h := hf_int.integral_compProd
-  simp only [kernel.prodMkLeft_apply, kernel.const_apply] at h
-  have h_eq_compProd := kernel.rnDeriv_measure_compProd_right' μ κ η
-  refine (integrable_congr ?_).mp h
-  filter_upwards [h_eq_compProd] with a ha
-  rw [fDivReal]
-  refine integral_congr_ae ?_
-  filter_upwards [ha] with b hb
-  rw [hb]
-
 lemma f_compProd_congr (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ η : kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
     ∀ᵐ a ∂ν, (fun b ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal)
@@ -261,8 +590,34 @@ lemma integral_f_compProd_right_congr (μ : Measure α) [IsFiniteMeasure μ]
   rw [ha]
   simp_rw [h_eq_one, one_mul]
 
+lemma integral_f_compProd_left_congr (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    (κ : kernel α β) [IsFiniteKernel κ]  :
+    (fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) (a, b)).toReal ∂(κ a))
+      =ᵐ[ν] fun a ↦ (κ a Set.univ).toReal * f ((∂μ/∂ν) a).toReal := by
+  filter_upwards [integral_f_compProd_congr (f := f) μ ν κ κ] with a ha
+  have h_one := (κ a).rnDeriv_self
+  rw [ha, ← smul_eq_mul,  ← integral_const]
+  refine integral_congr_ae ?_
+  filter_upwards [h_one] with b hb
+  simp [hb]
+
+lemma integrable_f_rnDeriv_of_integrable_compProd [IsFiniteMeasure μ] [IsFiniteKernel κ]
+    [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (hf_int : Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x).toReal) (μ ⊗ₘ η)) :
+    ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a) := by
+  have h := hf_int.integral_compProd'
+  rw [Measure.integrable_compProd_iff] at hf_int
+  swap
+  · exact (hf.comp_measurable (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable
+  have h := kernel.rnDeriv_measure_compProd_right' μ κ η
+  filter_upwards [h, hf_int.1] with a ha1 ha2
+  refine (integrable_congr ?_).mp ha2
+  filter_upwards [ha1] with b hb
+  rw [hb]
+
 lemma integrable_f_rnDeriv_compProd_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) :
+    [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
     Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
       ↔ (∀ᵐ a ∂ν, Integrable (fun x ↦ f ((∂μ/∂ν) a * (∂κ a/∂η a) x).toReal) (η a))
         ∧ Integrable (fun a ↦ ∫ b, f ((∂μ/∂ν) a * (∂κ a/∂η a) b).toReal ∂(η a)) ν := by
@@ -294,106 +649,323 @@ lemma integrable_f_rnDeriv_compProd_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν
       -- finite the integral is finite.
       sorry
 
-lemma integrable_f_rnDeriv_compProd_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ]
-    [IsFiniteKernel η] (hf : StronglyMeasurable f) :
-    Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x).toReal) (μ ⊗ₘ η)
-      ↔ (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((κ a).rnDeriv (η a) x).toReal) (η a))
-        ∧ Integrable (fun a ↦ fDivReal f (κ a) (η a)) μ := by
-  rw [integrable_f_rnDeriv_compProd_iff hf]
-  have h_self : ∂μ/∂μ =ᵐ[μ] fun _ ↦ 1 := Measure.rnDeriv_self μ
-  refine ⟨fun ⟨h1, h2⟩ ↦ ⟨?_, ?_⟩, fun ⟨h1, h2⟩ ↦ ⟨?_, ?_⟩⟩
-  · filter_upwards [h_self, h1] with a h_eq_one ha
-    simp_rw [h_eq_one, one_mul] at ha
-    exact ha
-  · refine (integrable_congr ?_).mpr h2
-    filter_upwards [h_self] with a ha
-    simp_rw [ha, one_mul]
-    rfl
-  · filter_upwards [h_self, h1] with a h_eq_one ha
-    simp_rw [h_eq_one, one_mul]
-    exact ha
+lemma fDivReal_compProd_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+  fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ η) ≠ ⊤ ↔
+    (∀ᵐ a ∂ν, Integrable (fun x ↦ f ((∂μ/∂ν) a * (∂κ a/∂η a) x).toReal) (η a))
+      ∧ Integrable (fun a ↦ ∫ b, f ((∂μ/∂ν) a * (∂κ a/∂η a) b).toReal ∂(η a)) ν
+      ∧ (derivInfty f = ⊤ → μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a) := by
+  rw [fDivReal_ne_top_iff, integrable_f_rnDeriv_compProd_iff hf h_cvx,
+    kernel.Measure.absolutelyContinuous_compProd_iff, and_assoc]
+
+lemma fDivReal_compProd_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ η) = ⊤ ↔
+    (∀ᵐ a ∂ν, Integrable (fun x ↦ f ((∂μ/∂ν) a * (∂κ a/∂η a) x).toReal) (η a)) →
+      Integrable (fun a ↦ ∫ b, f ((∂μ/∂ν) a * (∂κ a/∂η a) b).toReal ∂η a) ν →
+      derivInfty f = ⊤ ∧ (μ ≪ ν → ¬∀ᵐ a ∂μ, κ a ≪ η a) := by
+  rw [← not_iff_not, ← ne_eq, fDivReal_compProd_ne_top_iff hf h_cvx]
+  push_neg
+  rfl
+
+lemma fDivReal_compProd_right_ne_top_iff [IsFiniteMeasure μ]
+    [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+  fDivReal f (μ ⊗ₘ κ) (μ ⊗ₘ η) ≠ ⊤ ↔
+    (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a))
+      ∧ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a)) μ
+      ∧ (derivInfty f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) := by
+  rw [fDivReal_compProd_ne_top_iff hf h_cvx]
+  have h_self := μ.rnDeriv_self
+  refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨?_, ?_, ?_⟩⟩
+  · filter_upwards [h_self, h.1] with a ha1 ha2
+    simp_rw [ha1, one_mul] at ha2
+    exact ha2
+  · refine (integrable_congr ?_).mp h.2.1
+    filter_upwards [h_self] with a ha1
+    simp_rw [ha1, one_mul]
+  · simp only [Measure.AbsolutelyContinuous.rfl, true_and] at h
+    exact h.2.2
+  · filter_upwards [h_self, h.1] with a ha1 ha2
+    simp_rw [ha1, one_mul]
+    exact ha2
+  · refine (integrable_congr ?_).mp h.2.1
+    filter_upwards [h_self] with a ha1
+    simp_rw [ha1, one_mul]
+  · simp only [Measure.AbsolutelyContinuous.rfl, true_and]
+    exact h.2.2
+
+lemma fDivReal_compProd_right_eq_top_iff [IsFiniteMeasure μ]
+    [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    fDivReal f (μ ⊗ₘ κ) (μ ⊗ₘ η) = ⊤ ↔
+    (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) →
+      Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ →
+      derivInfty f = ⊤ ∧ ¬∀ᵐ a ∂μ, κ a ≪ η a := by
+  rw [← not_iff_not, ← ne_eq, fDivReal_compProd_right_ne_top_iff hf h_cvx]
+  push_neg
+  rfl
+
+lemma fDivReal_compProd_left_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    [IsMarkovKernel κ] (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+  fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ κ) ≠ ⊤ ↔
+    Integrable (fun a ↦ f ((∂μ/∂ν) a).toReal) ν ∧ (derivInfty f = ⊤ → μ ≪ ν) := by
+  rw [fDivReal_compProd_ne_top_iff hf h_cvx]
+  have h_one : ∀ a, ∂(κ a)/∂(κ a) =ᵐ[κ a] 1 := fun a ↦ Measure.rnDeriv_self (κ a)
+  simp only [ENNReal.toReal_mul, Measure.AbsolutelyContinuous.rfl, eventually_true, and_true]
+  have : ∀ a, ∫ b, f (((∂μ/∂ν) a).toReal * ((∂κ a/∂κ a) b).toReal) ∂κ a
+        = ∫ _, f (((∂μ/∂ν) a).toReal) ∂κ a := by
+      refine fun a ↦ integral_congr_ae ?_
+      filter_upwards [h_one a] with b hb
+      simp [hb]
+  refine ⟨fun ⟨_, h2, h3⟩ ↦ ⟨?_, h3⟩, fun ⟨h1, h2⟩ ↦ ⟨?_, ?_, h2⟩⟩
   · refine (integrable_congr ?_).mpr h2
-    filter_upwards [h_self] with a ha
-    simp_rw [ha, one_mul]
+    refine ae_of_all _ (fun a ↦ ?_)
+    simp only
+    simp [this]
+  · refine ae_of_all _ (fun a ↦ ?_)
+    have : (fun x ↦ f (((∂μ/∂ν) a).toReal * ((∂κ a/∂κ a) x).toReal))
+        =ᵐ[κ a] (fun _ ↦ f ((∂μ/∂ν) a).toReal) := by
+      filter_upwards [h_one a] with b hb
+      simp [hb]
+    rw [integrable_congr this]
+    simp
+  · simp only [this, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul]
+    exact h1
+
+lemma fDivReal_compProd_left_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    [IsMarkovKernel κ] (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+  fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = ⊤ ↔
+    Integrable (fun a ↦ f ((∂μ/∂ν) a).toReal) ν → (derivInfty f = ⊤ ∧ ¬ μ ≪ ν) := by
+  rw [← not_iff_not, ← ne_eq, fDivReal_compProd_left_ne_top_iff hf h_cvx]
+  push_neg
+  rfl
+
+lemma integrable_singularPart [IsFiniteMeasure μ]
+    [IsFiniteKernel κ] [IsFiniteKernel η] :
+    Integrable (fun x ↦ ((κ x).singularPart (η x) Set.univ).toReal) μ := by
+  refine integrable_toReal_of_lintegral_ne_top ?_ (ne_of_lt ?_)
+  · simp_rw [← kernel.singularPart_eq_singularPart_measure]
+    exact (kernel.measurable_coe _ MeasurableSet.univ).aemeasurable
+  calc ∫⁻ x, (κ x).singularPart (η x) Set.univ ∂μ
+  _ ≤ ∫⁻ x, κ x Set.univ ∂μ := by
+        refine lintegral_mono (fun x ↦ ?_)
+        exact Measure.singularPart_le _ _ _
+  _ = (μ ⊗ₘ κ) Set.univ := by
+        rw [← Set.univ_prod_univ, Measure.compProd_apply_prod MeasurableSet.univ MeasurableSet.univ,
+          set_lintegral_univ]
+  _ < ⊤ := measure_lt_top _ _
+
+lemma integrable_fDivReal_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η]
+    (h_fin : ∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤) :
+    Integrable (fun x ↦ EReal.toReal (fDivReal f (κ x) (η x))) μ
+      ↔ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ := by
+  by_cases h_top : derivInfty f = ⊤
+  · classical
+    simp_rw [fDivReal_of_derivInfty_eq_top h_top]
+    simp only [fDivReal_ne_top_iff, h_top, forall_true_left] at h_fin
+    refine integrable_congr ?_
+    filter_upwards [h_fin] with a ha
+    rw [if_pos ha, EReal.toReal_coe]
+  · have h_fin' := h_fin
+    simp_rw [fDivReal_ne_top_iff_of_derivInfty_ne_top h_top] at h_fin
+    have : (fun x ↦ (fDivReal f (κ x) (η x)).toReal)
+        =ᵐ[μ] (fun x ↦ ∫ y, f ((∂κ x/∂η x) y).toReal ∂(η x)
+          + (derivInfty f).toReal * ((κ x).singularPart (η x) Set.univ).toReal) := by
+      filter_upwards [h_fin'] with x hx1
+      rw [fDivReal_of_ne_top hx1, EReal.toReal_add]
+      · simp only [EReal.toReal_coe, add_right_inj]
+        rw [EReal.toReal_mul]
+        simp
+      · simp
+      · simp
+      · simp [h_top, EReal.mul_eq_top, derivInfty_ne_bot, measure_ne_top]
+      · simp [EReal.mul_eq_bot, derivInfty_ne_bot, h_top, measure_ne_top]
+    rw [integrable_congr this]
+    have h_int : Integrable (fun x ↦ (derivInfty f).toReal
+        * ((κ x).singularPart (η x) Set.univ).toReal) μ := by
+      refine Integrable.const_mul ?_ (derivInfty f).toReal
+      exact integrable_singularPart
+    refine ⟨fun h ↦ ?_, fun h ↦ h.add h_int⟩
+    have : (fun x ↦ ∫ y, f ((∂κ x/∂η x) y).toReal ∂η x)
+        = (fun x ↦ (∫ y, f ((∂κ x/∂η x) y).toReal ∂η x +
+          (derivInfty f).toReal * ((κ x).singularPart (η x) Set.univ).toReal)
+          - (derivInfty f).toReal * ((κ x).singularPart (η x) Set.univ).toReal) := by
+      ext; simp
+    rw [this]
+    exact h.sub h_int
+
+lemma condFDivReal_ne_top_iff [IsFiniteMeasure μ] [IsMarkovKernel κ] [IsFiniteKernel η] :
+  condFDivReal f κ η μ ≠ ⊤ ↔
+    (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a))
+      ∧ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a)) μ
+      ∧ (derivInfty f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) := by
+  rw [condFDivReal]
+  split_ifs with h
+  · have h' := h
+    simp_rw [fDivReal_ne_top_iff] at h
+    simp only [ne_eq, EReal.coe_ne_top, not_false_eq_true, true_iff]
+    refine ⟨?_, ?_, ?_⟩
+    · filter_upwards [h.1] with a ha
+      exact ha.1
+    · have h_int := h.2
+      rwa [integrable_fDivReal_iff h'.1] at h_int
+    · intro h_top
+      filter_upwards [h.1] with a ha
+      exact ha.2 h_top
+  · simp only [ne_eq, not_true_eq_false, false_iff, not_and, not_forall, not_eventually,
+      exists_prop]
+    push_neg at h
+    intro hf_int h_int
+    simp_rw [fDivReal_ne_top_iff] at h
+    by_contra h_contra
+    simp only [not_and, not_frequently, not_not] at h_contra
+    rw [eventually_and] at h
+    simp only [hf_int, eventually_all, true_and] at h
+    specialize h h_contra
+    have h_top : ∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤ := by
+      simp only [ne_eq, fDivReal_ne_top_iff, eventually_and, eventually_all]
+      exact ⟨hf_int, h_contra⟩
+    rw [integrable_fDivReal_iff h_top] at h
+    exact h h_int
+
+lemma condFDivReal_ne_top_iff_fDivReal_compProd_ne_top [IsFiniteMeasure μ]
+    [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    condFDivReal f κ η μ ≠ ⊤ ↔ fDivReal f (μ ⊗ₘ κ) (μ ⊗ₘ η) ≠ ⊤ := by
+  rw [condFDivReal_ne_top_iff, fDivReal_compProd_right_ne_top_iff hf h_cvx]
+
+lemma condFDivReal_eq_top_iff_fDivReal_compProd_eq_top [IsFiniteMeasure μ]
+    [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    condFDivReal f κ η μ = ⊤ ↔ fDivReal f (μ ⊗ₘ κ) (μ ⊗ₘ η) = ⊤ := by
+  rw [← not_iff_not]
+  exact condFDivReal_ne_top_iff_fDivReal_compProd_ne_top hf h_cvx
+
+lemma condFDivReal_eq_add [IsFiniteMeasure μ]
+    [IsFiniteKernel κ] [IsFiniteKernel η] (hf_ae : ∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤)
+    (hf : Integrable (fun x ↦ (fDivReal f (κ x) (η x)).toReal) μ) :
+    condFDivReal f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ)
+      + (derivInfty f).toReal * (μ[fun a ↦ ((κ a).singularPart (η a) Set.univ).toReal] : ℝ) := by
+  rw [condFDivReal_eq hf_ae hf]
+  have : (fun x ↦ EReal.toReal (fDivReal f (κ x) (η x)))
+      =ᵐ[μ] fun x ↦ ∫ y, f ((∂(κ x)/∂(η x)) y).toReal ∂(η x)
+        + (derivInfty f * (κ x).singularPart (η x) Set.univ).toReal := by
+    filter_upwards [hf_ae] with x hx
+    rw [fDivReal_of_ne_top hx, EReal.toReal_add]
+    rotate_left
+    · simp
+    · simp
+    · simp only [ne_eq, EReal.mul_eq_top, derivInfty_ne_bot, false_and, EReal.coe_ennreal_ne_bot,
+        and_false, EReal.coe_ennreal_pos, Measure.measure_univ_pos, EReal.coe_ennreal_eq_top_iff,
+        measure_ne_top, or_false, false_or, not_and, not_not]
+      intro h_top
+      rw [fDivReal_ne_top_iff] at hx
+      simp [h_top, Measure.singularPart_eq_zero_of_ac (hx.2 h_top)]
+    · simp only [ne_eq, EReal.mul_eq_bot, derivInfty_ne_bot, EReal.coe_ennreal_pos,
+        Measure.measure_univ_pos, false_and, EReal.coe_ennreal_ne_bot, and_false,
+        EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_false, false_or, not_and, not_lt]
+      exact fun _ ↦ EReal.coe_ennreal_nonneg _
     rfl
+  rw [integral_congr_ae this]
+  rw [integral_add]
+  rotate_left
+  · rwa [integrable_fDivReal_iff hf_ae] at hf
+  · simp_rw [EReal.toReal_mul]
+    convert (integrable_singularPart (κ := κ) (η := η) (μ := μ)).const_mul (derivInfty f).toReal
+    rw [← EReal.coe_ennreal_toReal, EReal.toReal_coe]
+    exact measure_ne_top _ _
+  simp only [EReal.coe_add, EReal.toReal_mul]
+  rw [integral_mul_left]
+  simp only [_root_.EReal.toReal_coe_ennreal, EReal.coe_mul]
+
+lemma condFDivReal_of_derivInfty_eq_top [IsFiniteMeasure μ]
+    [IsFiniteKernel κ] [IsFiniteKernel η] (hf_ae : ∀ᵐ a ∂μ, fDivReal f (κ a) (η a) ≠ ⊤)
+    (hf : Integrable (fun x ↦ (fDivReal f (κ x) (η x)).toReal) μ) (h_top : derivInfty f = ⊤):
+    condFDivReal f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ) := by
+  rw [condFDivReal_eq_add hf_ae hf]
+  simp [h_top]
 
 end Integrable
 
 lemma fDivReal_compProd_left (μ : Measure α) [IsFiniteMeasure μ]
-    (κ η : kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) :
+    (κ η : kernel α β) [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
     fDivReal f (μ ⊗ₘ κ) (μ ⊗ₘ η) = condFDivReal f κ η μ := by
-  by_cases hf_int : Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x).toReal) (μ ⊗ₘ η)
-  swap
-  · rw [fDivReal_of_not_integrable hf_int]
-    rw [integrable_f_rnDeriv_compProd_right_iff hf] at hf_int
-    push_neg at hf_int
-    by_cases hf_int' : ∀ᵐ (a : α) ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)
-    · rw [condFDivReal_of_not_integrable (hf_int hf_int')]
-    · rw [condFDivReal_of_not_ae_integrable hf_int']
-  have hf_int' := (integrable_f_rnDeriv_compProd_right_iff hf).mp hf_int
-  rw [condFDivReal_eq hf_int'.1, fDivReal, Measure.integral_compProd hf_int]
-  rw [integral_congr_ae (integral_f_compProd_right_congr μ κ η)]
-  rfl
-
-lemma fDivReal_compProd_withDensity_rnDeriv (μ ν : Measure α) (κ η : kernel α β)
-    [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteKernel κ] [IsFiniteKernel η] :
-    fDivReal f ((ν.withDensity (∂μ/∂ν)) ⊗ₘ (kernel.withDensity η (kernel.rnDeriv κ η))) (ν ⊗ₘ η)
-      = fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
-  refine integral_congr_ae ?_
-  filter_upwards [kernel.todo1 μ ν κ η] with p hp
-  rw [hp]
-
-lemma condFDivReal_withDensity_rnDeriv (κ η : kernel α β) (μ : Measure α)
-    [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] :
-    condFDivReal f (kernel.withDensity η (kernel.rnDeriv κ η)) η μ = condFDivReal f κ η μ := by
-  sorry
+  by_cases hf_top : condFDivReal f κ η μ = ⊤
+  · rwa [hf_top, ← condFDivReal_eq_top_iff_fDivReal_compProd_eq_top hf h_cvx]
+  have hf_top' := hf_top
+  have hf_top'' := hf_top
+  have hf_top''' := hf_top
+  rw [← ne_eq, condFDivReal_ne_top_iff] at hf_top'
+  rw [condFDivReal_eq_top_iff_fDivReal_compProd_eq_top hf h_cvx, ← ne_eq, fDivReal_ne_top_iff]
+    at hf_top''
+  rw [condFDivReal_eq_top_iff_fDivReal_compProd_eq_top hf h_cvx] at hf_top'''
+  rcases hf_top' with ⟨h1, h2, h3⟩
+  rcases hf_top'' with ⟨h4, h5⟩
+  classical
+  by_cases h_deriv : derivInfty f = ⊤
+  · rw [fDivReal_of_derivInfty_eq_top h_deriv, if_pos ⟨h4, h5 h_deriv⟩,
+      condFDivReal_of_derivInfty_eq_top _ _ h_deriv]
+    sorry
+    sorry
+    sorry
+  · rw [fDivReal_of_ne_top, condFDivReal_eq_add]
+    rotate_left
+    · sorry
+    · sorry
+    · exact hf_top'''
+    congr
+    · sorry
+    · rw [EReal.coe_toReal h_deriv derivInfty_ne_bot]
+    · -- extract lemma
+      sorry
 
 end Conditional
 
 lemma fDivReal_compProd_right [MeasurableSpace.CountablyGenerated β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (κ : kernel α β) [IsMarkovKernel κ] (hf : StronglyMeasurable f) :
+    (κ : kernel α β) [IsMarkovKernel κ] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
     fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = fDivReal f μ ν := by
-  have h_compProd := kernel.rnDeriv_measure_compProd_left μ ν κ
-  by_cases hf_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) (ν ⊗ₘ κ)
-  swap
-  · rw [fDivReal_of_not_integrable hf_int, fDivReal_of_not_integrable]
-    have hf_int' : ¬ Integrable (fun p ↦ f ((∂μ/∂ν) p.1).toReal) (ν ⊗ₘ κ) := by
-      refine fun h_not ↦ hf_int ((integrable_congr ?_).mpr h_not)
-      filter_upwards [h_compProd] with p hp
-      rw [hp]
-    rw [Measure.integrable_compProd_iff] at hf_int'
-    swap
-    · exact (hf.comp_measurable ((Measure.measurable_rnDeriv _ _).comp
-        measurable_fst).ennreal_toReal).aestronglyMeasurable
-    push_neg at hf_int'
-    simp only [integrable_const, Filter.eventually_true, norm_eq_abs, integral_const, measure_univ,
-      ENNReal.one_toReal, smul_eq_mul, one_mul, forall_true_left] at hf_int'
-    sorry
-  rw [fDivReal, Measure.integral_compProd hf_int]
-  refine integral_congr_ae ?_
-  filter_upwards [Measure.ae_ae_of_ae_compProd h_compProd] with a ha
-  have : ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) (a, b)).toReal ∂κ a = ∫ b, f ((∂μ/∂ν) a).toReal ∂κ a := by
-    refine integral_congr_ae ?_
-    filter_upwards [ha] with b hb
-    rw [hb]
-  simp [this, integral_const]
+  by_cases h_top : fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = ⊤
+  · symm
+    rw [h_top, fDivReal_eq_top_iff]
+    have h_top' := (fDivReal_compProd_left_eq_top_iff hf h_cvx).mp h_top
+    by_cases h : Integrable (fun a ↦ f ((∂μ/∂ν) a).toReal) ν
+    · exact Or.inr (h_top' h)
+    · exact Or.inl h
+  · have h_top' := (fDivReal_compProd_left_ne_top_iff hf h_cvx).mp h_top
+    have h_top'' : fDivReal f μ ν ≠ ⊤ := by rwa [fDivReal_ne_top_iff]
+    rw [fDivReal_of_ne_top h_top, fDivReal_of_ne_top h_top'']
+    have h := integral_f_compProd_left_congr μ ν κ (f := f)
+    simp only [measure_univ, ENNReal.one_toReal, one_mul] at h
+    rw [integral_congr_ae h.symm, Measure.integral_compProd]
+    · congr
+      sorry  -- extract lemma
+    · sorry
 
 lemma f_rnDeriv_ae_le_integral [MeasurableSpace.CountablyGenerated β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (κ η : kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η]
+    (κ η : kernel α β) [IsFiniteKernel κ] [IsMarkovKernel η]
     (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
-    (hf : StronglyMeasurable f)
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
-    (hμν : μ ≪ ν) (hκη : ∀ᵐ a ∂ν, κ a ≪ η a) :
-    (fun a ↦ f ((∂μ/∂ν) a).toReal)
+    (hκη : ∀ᵐ a ∂ν, κ a ≪ η a) :
+    (fun a ↦ f ((∂μ/∂ν) a * κ a Set.univ).toReal)
       ≤ᵐ[ν] fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal ∂(η a) := by
   have h_compProd := kernel.rnDeriv_measure_compProd' μ ν κ η
   have h_lt_top := Measure.ae_ae_of_ae_compProd <| Measure.rnDeriv_lt_top (μ ⊗ₘ κ) (ν ⊗ₘ η)
-  filter_upwards [hκη, h_compProd, h_lt_top] with a h_ac h_eq h_lt_top
-  calc f ((∂μ/∂ν) a).toReal
-    = f ((∂μ/∂ν) a * κ a Set.univ).toReal  := by simp
-  _ = f ((∂μ/∂ν) a * ∫⁻ b, (∂κ a/∂η a) b ∂η a).toReal := by rw [Measure.lintegral_rnDeriv h_ac]
+  have := Measure.integrable_toReal_rnDeriv (μ := μ ⊗ₘ κ) (ν := ν ⊗ₘ η)
+  rw [Measure.integrable_compProd_iff] at this
+  swap
+  · refine (Measurable.stronglyMeasurable ?_).aestronglyMeasurable
+    exact (Measure.measurable_rnDeriv _ _).ennreal_toReal
+  filter_upwards [hκη, h_compProd, h_lt_top, h_int.compProd_mk_left_ae', this.1]
+    with a h_ac h_eq h_lt_top h_int' h_rnDeriv_int
+  calc f ((∂μ/∂ν) a * κ a Set.univ).toReal
+    = f ((∂μ/∂ν) a * ∫⁻ b, (∂κ a/∂η a) b ∂η a).toReal := by rw [Measure.lintegral_rnDeriv h_ac]
   _ = f (∫⁻ b,(∂μ/∂ν) a * (∂κ a/∂η a) b ∂η a).toReal := by
         rw [lintegral_const_mul _ (Measure.measurable_rnDeriv _ _)]
   _ = f (∫⁻ b, (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b) ∂η a).toReal := by rw [lintegral_congr_ae h_eq]
@@ -402,25 +974,7 @@ lemma f_rnDeriv_ae_le_integral [MeasurableSpace.CountablyGenerated β]
         exact ((Measure.measurable_rnDeriv _ _).comp measurable_prod_mk_left).aemeasurable
   _ ≤ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal ∂η a := by
         rw [← average_eq_integral, ← average_eq_integral]
-        rw [integrable_f_rnDeriv_compProd_iff hf] at h_int
-        refine ConvexOn.map_average_le hf_cvx hf_cont isClosed_Ici (by simp) ?_ ?_
-        · sorry  -- Integrable (fun x ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, x)).toReal) (η a)
-        · sorry  -- Integrable (fun x ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, x)).toReal) (η a)
-
-lemma le_fDivReal_compProd_aux [MeasurableSpace.CountablyGenerated β]
-    (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (κ η : kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η]
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
-    (hf : StronglyMeasurable f)
-    (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
-    (h_int_meas : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
-    (hμν : μ ≪ ν) (hκη : ∀ᵐ a ∂ν, κ a ≪ η a) :
-    fDivReal f μ ν ≤ fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
-  rw [fDivReal, fDivReal, Measure.integral_compProd h_int]
-  refine integral_mono_ae ?_ ?_ ?_
-  · exact h_int_meas
-  · sorry -- Integrable (fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal ∂η a) ν
-  exact f_rnDeriv_ae_le_integral μ ν κ η hf_cvx hf_cont hf h_int hμν hκη
+        exact ConvexOn.map_average_le hf_cvx hf_cont isClosed_Ici (by simp) h_rnDeriv_int h_int'
 
 lemma le_fDivReal_compProd [MeasurableSpace.CountablyGenerated β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
@@ -429,6 +983,12 @@ lemma le_fDivReal_compProd [MeasurableSpace.CountablyGenerated β]
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
     (h_int_meas : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     fDivReal f μ ν ≤ fDivReal f (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
+  let κ' := kernel.withDensity η (kernel.rnDeriv κ η)
+  have h : ∀ a, f ((∂μ/∂ν) a).toReal
+      ≤ f ((∂μ/∂ν) a * κ' a Set.univ).toReal
+        + (derivInfty f).toReal * ((∂μ/∂ν) a).toReal
+          * (kernel.singularPart κ η a Set.univ).toReal := by
+    sorry
   sorry
 
 end ProbabilityTheory
diff --git a/TestingLowerBounds/ForMathlib/EReal.lean b/TestingLowerBounds/ForMathlib/EReal.lean
new file mode 100644
index 00000000..35015fd2
--- /dev/null
+++ b/TestingLowerBounds/ForMathlib/EReal.lean
@@ -0,0 +1,59 @@
+import Mathlib.Data.Real.EReal
+
+open scoped ENNReal NNReal
+
+lemma EReal.mul_eq_top (a b : EReal) :
+    a * b = ⊤ ↔ (a = ⊥ ∧ b < 0) ∨ (a < 0 ∧ b = ⊥) ∨ (a = ⊤ ∧ 0 < b) ∨ (0 < a ∧ b = ⊤) := by
+  induction' a, b using EReal.induction₂_symm with a b h x hx x hx x hx x y x hx
+  · rw [mul_comm, h]
+    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+      <;> cases h with
+      | inl h => exact Or.inr (Or.inl ⟨h.2, h.1⟩)
+      | inr h => cases h with
+        | inl h => exact Or.inl ⟨h.2, h.1⟩
+        | inr h => cases h with
+          | inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
+          | inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))
+  · simp
+  · simp [EReal.top_mul_coe_of_pos hx, hx]
+  · simp
+  · simp [hx.le, EReal.top_mul_coe_of_neg hx]
+  · simp
+  · simp [hx.le, EReal.coe_mul_bot_of_pos hx]
+  · simp only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top,
+      EReal.coe_pos, or_self, iff_false]
+    rw [← EReal.coe_mul]
+    exact EReal.coe_ne_top _
+  · simp
+  · simp [hx, EReal.coe_mul_bot_of_neg hx]
+  · simp
+
+lemma EReal.mul_eq_bot (a b : EReal) :
+    a * b = ⊥ ↔ (a = ⊥ ∧ 0 < b) ∨ (0 < a ∧ b = ⊥) ∨ (a = ⊤ ∧ b < 0) ∨ (a < 0 ∧ b = ⊤) := by
+  induction' a, b using EReal.induction₂_symm with a b h x hx x hx x hx x y x hx
+  · rw [mul_comm, h]
+    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+      <;> cases h with
+      | inl h => exact Or.inr (Or.inl ⟨h.2, h.1⟩)
+      | inr h => cases h with
+        | inl h => exact Or.inl ⟨h.2, h.1⟩
+        | inr h => cases h with
+          | inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
+          | inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))
+  · simp
+  · simp [EReal.top_mul_coe_of_pos hx, hx.le]
+  · simp
+  · simp [hx, EReal.top_mul_coe_of_neg hx]
+  · simp
+  · simp [hx, EReal.coe_mul_bot_of_pos hx]
+  · simp only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top,
+      EReal.coe_pos, or_self, iff_false]
+    rw [← EReal.coe_mul]
+    exact EReal.coe_ne_bot _
+  · simp
+  · simp [hx.le, EReal.coe_mul_bot_of_neg hx]
+  · simp
+
+lemma EReal.coe_ennreal_toReal {x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x := by
+  lift x to ℝ≥0 using hx
+  rfl
diff --git a/TestingLowerBounds/ForMathlib/RnDeriv.lean b/TestingLowerBounds/ForMathlib/RnDeriv.lean
new file mode 100644
index 00000000..660628bf
--- /dev/null
+++ b/TestingLowerBounds/ForMathlib/RnDeriv.lean
@@ -0,0 +1,213 @@
+/-
+Copyright (c) 2024 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Mathlib.MeasureTheory.Measure.Tilted
+
+/-!
+
+-/
+
+open Real MeasureTheory Filter
+
+open scoped ENNReal
+
+namespace MeasureTheory.Measure
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+  {μ ν : Measure α} {κ η : kernel α β} {f g : ℝ → ℝ}
+
+lemma singularPart_eq_zero_of_ac (h : μ ≪ ν) : μ.singularPart ν = 0 := by
+  rw [← MutuallySingular.self_iff]
+  exact MutuallySingular.mono_ac (mutuallySingular_singularPart _ _)
+    AbsolutelyContinuous.rfl ((absolutelyContinuous_of_le (singularPart_le _ _)).trans h)
+
+lemma singularPart_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
+    μ.singularPart ν = 0 ↔ μ ≪ ν := by
+  have h_dec := haveLebesgueDecomposition_add μ ν
+  refine ⟨fun h ↦ ?_, singularPart_eq_zero_of_ac⟩
+  rw [h, zero_add] at h_dec
+  rw [h_dec]
+  exact withDensity_absolutelyContinuous ν _
+
+lemma singularPart_self (μ : Measure α) : μ.singularPart μ = 0 :=
+  singularPart_eq_zero_of_ac Measure.AbsolutelyContinuous.rfl
+
+lemma singularPart_eq_self (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
+    μ.singularPart ν = μ ↔ μ ⟂ₘ ν := by
+  have h_dec := haveLebesgueDecomposition_add μ ν
+  refine ⟨fun h ↦ ?_, fun  h ↦ ?_⟩
+  · conv_lhs => rw [h_dec]
+    simp only [MutuallySingular.add_left_iff]
+    refine ⟨mutuallySingular_singularPart _ _, ?_⟩
+    rw [← h, withDensity_congr_ae (rnDeriv_singularPart μ ν)]
+    simp
+  · conv_rhs => rw [h_dec]
+    rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]
+
+lemma rnDeriv_add_self_right (ν μ : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    ν.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ (μ.rnDeriv ν x + 1)⁻¹ := by
+  have hν_ac : ν ≪ μ + ν := by rw [add_comm]; exact rfl.absolutelyContinuous.add_right _
+  filter_upwards [Measure.rnDeriv_add' μ ν ν, Measure.rnDeriv_self ν,
+    Measure.inv_rnDeriv hν_ac] with a h1 h2 h3
+  rw [Pi.inv_apply, h1, Pi.add_apply, h2, inv_eq_iff_eq_inv] at h3
+  rw [h3]
+
+lemma rnDeriv_add_self_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1) := by
+  have h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν) :=
+    (ae_add_measure_iff.mp (Measure.rnDeriv_add' μ ν (μ + ν))).2
+  have h_one_add := (ae_add_measure_iff.mp (Measure.rnDeriv_self (μ + ν))).2
+  have : (μ.rnDeriv (μ + ν)) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹ := by
+    filter_upwards [h_add, h_one_add, rnDeriv_add_self_right ν μ] with a h4 h5 h6
+    rw [h5, Pi.add_apply] at h4
+    nth_rewrite 1 [h4]
+    rw [h6]
+    simp only [ne_eq, ENNReal.inv_eq_top, add_eq_zero, one_ne_zero, and_false, not_false_eq_true,
+      ENNReal.add_sub_cancel_right]
+  filter_upwards [this, Measure.rnDeriv_lt_top μ ν] with a ha ha_lt_top
+  rw [ha, div_eq_mul_inv]
+  refine ENNReal.sub_eq_of_eq_add (by simp) ?_
+  nth_rewrite 2 [← one_mul (μ.rnDeriv ν a + 1)⁻¹]
+  have h := add_mul (μ.rnDeriv ν a) 1 (μ.rnDeriv ν a + 1)⁻¹
+  rw [ENNReal.mul_inv_cancel] at h
+  · exact h
+  · simp
+  · simp [ha_lt_top.ne]
+
+lemma rnDeriv_eq_div (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    μ.rnDeriv ν =ᵐ[ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x := by
+  filter_upwards [rnDeriv_add_self_right ν μ, rnDeriv_add_self_left μ ν, Measure.rnDeriv_lt_top μ ν]
+      with a ha1 ha2 ha_lt_top
+  rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc,
+      ENNReal.mul_inv_cancel, one_mul]
+  · simp
+  · simp [ha_lt_top.ne]
+
+lemma rnDeriv_div_rnDeriv {ξ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite ξ]
+    (hμ : μ ≪ ξ) (hν : ν ≪ ξ) :
+    (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x)
+      =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x := by
+  have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ :=
+    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right _)
+  have h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ :=
+    Measure.rnDeriv_mul_rnDeriv ?_
+  swap; · rw [add_comm]; exact rfl.absolutelyContinuous.add_right _
+  have h_ac : μ + ν ≪ ξ := by
+    refine (Measure.AbsolutelyContinuous.add hμ hν).trans ?_
+    have : ξ + ξ = (2 : ℝ≥0∞) • ξ := by
+      ext
+      simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply,
+        Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, smul_eq_mul]
+      rw [two_mul]
+    rw [this]
+    exact Measure.absolutelyContinuous_of_le_smul le_rfl
+  filter_upwards [h_ac h1, h_ac h2, h_ac <| Measure.rnDeriv_lt_top (μ + ν) ξ,
+    Measure.rnDeriv_lt_top ν (μ + ν), Measure.rnDeriv_pos h_ac]
+    with a h1 h2 h_lt_top1 h_lt_top2 h_pos
+  rw [← h1, ← h2, Pi.mul_apply, Pi.mul_apply, div_eq_mul_inv,
+    ENNReal.mul_inv (Or.inr h_lt_top1.ne) (Or.inl h_lt_top2.ne), div_eq_mul_inv, mul_assoc,
+    mul_comm ((μ + ν).rnDeriv ξ a), mul_assoc, ENNReal.inv_mul_cancel h_pos.ne' h_lt_top1.ne,
+    mul_one]
+
+lemma rnDeriv_eq_div' {ξ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite ξ]
+    (hμ : μ ≪ ξ) (hν : ν ≪ ξ) :
+    μ.rnDeriv ν =ᵐ[ν] fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x := by
+  have hν_ac : ν ≪ μ + ν := by rw [add_comm]; exact rfl.absolutelyContinuous.add_right _
+  filter_upwards [rnDeriv_eq_div μ ν, hν_ac (rnDeriv_div_rnDeriv hμ hν)] with a h1 h2
+  exact h1.trans h2.symm
+
+lemma set_lintegral_eq_zero_of_null {s : Set α} {f : α → ℝ≥0∞} (h : μ s = 0) :
+    ∫⁻ x in s, f x ∂μ = 0 := by
+  have : μ.restrict s = 0 := by simp [h]
+  simp [this]
+
+def singularPartSet (μ ν : Measure α) := {x | ν.rnDeriv (μ + ν) x = 0}
+
+lemma measurableSet_singularPartSet : MeasurableSet (singularPartSet μ ν) :=
+  measurable_rnDeriv _ _ (measurableSet_singleton _)
+
+lemma measure_singularPartSet (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    ν (singularPartSet μ ν) = 0 := by
+  let s := singularPartSet μ ν
+  have hs : MeasurableSet s := measurableSet_singularPartSet
+  have hν_ac : ν ≪ μ + ν := by rw [add_comm]; exact rfl.absolutelyContinuous.add_right _
+  have h1 : ∫⁻ x in s, ν.rnDeriv (μ + ν) x ∂(μ + ν) = 0 := by
+    calc ∫⁻ x in s, ν.rnDeriv (μ + ν) x ∂(μ + ν)
+      = ∫⁻ x in s, 0 ∂(μ + ν) := set_lintegral_congr_fun hs (ae_of_all _ (fun _ hx ↦ hx))
+    _ = 0 := lintegral_zero
+  have h2 : ∫⁻ x in s, ν.rnDeriv (μ + ν) x ∂(μ + ν) = ν s :=
+    Measure.set_lintegral_rnDeriv hν_ac _
+  exact h2.symm.trans h1
+
+lemma measure_inter_compl_singularPartSet' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
+    {t : Set α} (ht : MeasurableSet t) :
+    μ (t ∩ (singularPartSet μ ν)ᶜ) = ∫⁻ x in t ∩ (singularPartSet μ ν)ᶜ, μ.rnDeriv ν x ∂ν := by
+  let s := singularPartSet μ ν
+  have hs : MeasurableSet s := measurableSet_singularPartSet
+  have hν_ac : ν ≪ μ + ν := by rw [add_comm]; exact rfl.absolutelyContinuous.add_right _
+  have : μ (t ∩ sᶜ) = ∫⁻ x in t ∩ sᶜ,
+      ν.rnDeriv (μ + ν) x * (μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) ∂(μ + ν) := by
+    have : ∫⁻ x in t ∩ sᶜ,
+          ν.rnDeriv (μ + ν) x * (μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) ∂(μ + ν)
+        = ∫⁻ x in t ∩ sᶜ, μ.rnDeriv (μ + ν) x ∂(μ + ν) := by
+      refine set_lintegral_congr_fun (ht.inter hs.compl) ?_
+      filter_upwards [Measure.rnDeriv_lt_top ν (μ + ν)] with x hx_top hx
+      rw [div_eq_mul_inv, mul_comm, mul_assoc, ENNReal.inv_mul_cancel, mul_one]
+      · simp only [Set.mem_inter_iff, Set.mem_compl_iff, Set.mem_setOf_eq, s] at hx
+        exact hx.2
+      · exact hx_top.ne
+    rw [this, Measure.set_lintegral_rnDeriv (rfl.absolutelyContinuous.add_right _)]
+  rw [this, set_lintegral_rnDeriv_mul hν_ac _ (ht.inter hs.compl)]
+  swap
+  · exact ((Measure.measurable_rnDeriv _ _).div (Measure.measurable_rnDeriv _ _)).aemeasurable
+  refine set_lintegral_congr_fun (ht.inter hs.compl) ?_
+  filter_upwards [Measure.rnDeriv_eq_div μ ν] with x hx
+  rw [hx]
+  exact fun _ ↦ rfl
+
+lemma measure_inter_compl_singularPartSet (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
+    {t : Set α} (ht : MeasurableSet t) :
+    μ (t ∩ (singularPartSet μ ν)ᶜ) = ∫⁻ x in t, μ.rnDeriv ν x ∂ν := by
+  rw [measure_inter_compl_singularPartSet' _ _ ht]
+  symm
+  calc ∫⁻ x in t, rnDeriv μ ν x ∂ν
+    = ∫⁻ x in (singularPartSet μ ν) ∩ t, rnDeriv μ ν x ∂ν
+      + ∫⁻ x in (singularPartSet μ ν)ᶜ ∩ t, rnDeriv μ ν x ∂ν := by
+        rw [← restrict_restrict measurableSet_singularPartSet,
+          ← restrict_restrict measurableSet_singularPartSet.compl,
+          lintegral_add_compl _ measurableSet_singularPartSet]
+  _ = ∫⁻ x in t ∩ (singularPartSet μ ν)ᶜ, rnDeriv μ ν x ∂ν := by
+        rw [set_lintegral_eq_zero_of_null (measure_mono_null (Set.inter_subset_left _ _) ?_),
+          Set.inter_comm, zero_add]
+        exact measure_singularPartSet _ _
+
+lemma restrict_compl_singularPartSet_eq_withDensity
+    (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    μ.restrict (singularPartSet μ ν)ᶜ = ν.withDensity (μ.rnDeriv ν) := by
+  ext t ht
+  rw [restrict_apply ht, measure_inter_compl_singularPartSet μ ν ht, withDensity_apply _ ht]
+
+lemma restrict_singularPartSet_eq_singularPart (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    μ.restrict (singularPartSet μ ν) = μ.singularPart ν := by
+  have h_add := haveLebesgueDecomposition_add μ ν
+  rw [← restrict_compl_singularPartSet_eq_withDensity μ ν] at h_add
+  have : μ = μ.restrict (singularPartSet μ ν) + μ.restrict (singularPartSet μ ν)ᶜ := by
+    rw [restrict_add_restrict_compl measurableSet_singularPartSet]
+  conv_lhs at h_add => rw [this]
+  exact (Measure.add_left_inj _ _ _).mp h_add
+
+lemma absolutelyContinuous_restrict_compl_singularPartSet
+    (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
+    μ.restrict (singularPartSet μ ν)ᶜ ≪ ν := by
+  rw [restrict_compl_singularPartSet_eq_withDensity]
+  exact withDensity_absolutelyContinuous _ _
+
+example [SigmaFinite μ] [SigmaFinite ν] :
+    μ {x | (ν.rnDeriv (μ + ν)) x = 0} = μ.singularPart ν Set.univ := by
+  rw [← restrict_singularPartSet_eq_singularPart]
+  simp only [MeasurableSet.univ, restrict_apply, Set.univ_inter]
+  rfl
+
+end MeasureTheory.Measure
diff --git a/TestingLowerBounds/Hellinger.lean b/TestingLowerBounds/Hellinger.lean
index da931e8b..0c186853 100644
--- a/TestingLowerBounds/Hellinger.lean
+++ b/TestingLowerBounds/Hellinger.lean
@@ -42,6 +42,7 @@ namespace ProbabilityTheory
 variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α}
 
 /-- Squared Hellinger distance between two measures. -/
-noncomputable def sqHellinger (μ ν : Measure α) : ℝ := fDivReal (fun x ↦ 2⁻¹ * (1 - sqrt x)^2) μ ν
+noncomputable def sqHellinger (μ ν : Measure α) : ℝ :=
+  (fDivReal (fun x ↦ 2⁻¹ * (1 - sqrt x)^2) μ ν).toReal
 
 end ProbabilityTheory
diff --git a/TestingLowerBounds/KullbackLeibler.lean b/TestingLowerBounds/KullbackLeibler.lean
index 7bfdc05e..977c554c 100644
--- a/TestingLowerBounds/KullbackLeibler.lean
+++ b/TestingLowerBounds/KullbackLeibler.lean
@@ -51,17 +51,6 @@ lemma integrable_rnDeriv_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace 
     Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν :=
   (integrable_rnDeriv_smul_iff hμν).mpr hf
 
-lemma todo_div [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
-    μ.rnDeriv ν =ᵐ[ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x := by
-  have hν_ac : ν ≪ μ + ν := by
-    rw [add_comm]; exact rfl.absolutelyContinuous.add_right _
-  have h_pos := Measure.rnDeriv_pos hν_ac
-  have h := Measure.rnDeriv_mul_rnDeriv hμν (κ := μ + ν)
-  filter_upwards [hν_ac.ae_le h, h_pos, hν_ac.ae_le (Measure.rnDeriv_ne_top ν (μ + ν))]
-    with x hx hx_pos hx_ne_top
-  rw [Pi.mul_apply] at hx
-  rwa [ENNReal.eq_div_iff hx_pos.ne' hx_ne_top, mul_comm]
-
 end move_this
 
 open Classical in
@@ -98,7 +87,7 @@ lemma integrable_rnDeriv_mul_log [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
 lemma klReal_eq_fDivReal_mul_log [SigmaFinite μ] [Measure.HaveLebesgueDecomposition μ ν]
     (hμν : μ ≪ ν) :
     klReal μ ν = fDivReal (fun x ↦ x * log x) μ ν := by
-  simp_rw [klReal_of_ac hμν, llr, fDivReal]
+  /-simp_rw [klReal_of_ac hμν, llr, fDivReal]
   conv_lhs =>
     rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
     conv in (Measure.rnDeriv (ν.withDensity (μ.rnDeriv ν)) ν) =>
@@ -112,7 +101,8 @@ lemma klReal_eq_fDivReal_mul_log [SigmaFinite μ] [Measure.HaveLebesgueDecomposi
   conv_lhs => rw [h_ν_eq]
   rw [integral_withDensity_eq_integral_smul]
   swap; · exact (Measure.measurable_rnDeriv _ _).ennreal_toNNReal
-  congr
+  congr -/
+  sorry
 
 end llr_and_lrf
 
@@ -121,8 +111,9 @@ section klReal_nonneg
 lemma klReal_ge_mul_log' [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
     (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
     (μ Set.univ).toReal * log (μ Set.univ).toReal ≤ klReal μ ν :=
-  (le_fDivReal Real.convexOn_mul_log Real.continuous_mul_log.continuousOn
-    (integrable_rnDeriv_mul_log hμν h_int) hμν).trans_eq (klReal_eq_fDivReal_mul_log hμν).symm
+  sorry
+  /-(le_fDivReal Real.convexOn_mul_log Real.continuous_mul_log.continuousOn
+    (integrable_rnDeriv_mul_log hμν h_int) hμν).trans_eq (klReal_eq_fDivReal_mul_log hμν).symm-/
 
 lemma klReal_ge_mul_log [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
@@ -165,13 +156,14 @@ lemma klReal_ge_mul_log [IsFiniteMeasure μ] [IsFiniteMeasure ν]
 
 lemma klReal_nonneg (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
     0 ≤ klReal μ ν := by
-  by_cases hμν : μ ≪ ν
+  sorry
+  /- by_cases hμν : μ ≪ ν
   swap; · simp [hμν]
   by_cases h_int : Integrable (llr μ ν) μ
   · rw [klReal_eq_fDivReal_mul_log hμν]
     exact fDivReal_nonneg Real.convexOn_mul_log Real.continuous_mul_log.continuousOn
       (by simp) (integrable_rnDeriv_mul_log hμν h_int) hμν
-  · rw [klReal_of_ac hμν, integral_undef h_int]
+  · rw [klReal_of_ac hμν, integral_undef h_int] -/
 
 end klReal_nonneg
 
diff --git a/TestingLowerBounds/Renyi.lean b/TestingLowerBounds/Renyi.lean
index 8830a734..934c3f5b 100644
--- a/TestingLowerBounds/Renyi.lean
+++ b/TestingLowerBounds/Renyi.lean
@@ -46,7 +46,8 @@ noncomputable def renyiReal (a : ℝ) (μ ν : Measure α) : ℝ :=
   if a = 0 then - log (ν {x | 0 < (∂μ/∂ν) x}).toReal
   else if a = 1 then klReal μ ν
   else if a < 1 ∨ μ ≪ ν
-    then (a - 1)⁻¹ * log (1 + (a - 1) * fDivReal (fun x ↦ (a - 1)⁻¹ * (x ^ a - 1)) μ ν)
+    -- todo: review this def
+    then (a - 1)⁻¹ * log (1 + (a - 1) * (fDivReal (fun x ↦ (a - 1)⁻¹ * (x ^ a - 1)) μ ν).toReal)
     else 0
 
 lemma renyiReal_zero (μ ν : Measure α) :
@@ -57,12 +58,12 @@ lemma renyiReal_one (μ ν : Measure α) : renyiReal 1 μ ν = klReal μ ν := b
 
 lemma renyiReal_of_pos_of_lt_one (μ ν : Measure α) (ha_pos : 0 < a) (ha_lt_one : a < 1) :
     renyiReal a μ ν
-      = (a - 1)⁻¹ * log (1 + (a - 1) * fDivReal (fun x ↦ (a - 1)⁻¹ * (x ^ a - 1)) μ ν) := by
+      = (a - 1)⁻¹ * log (1 + (a - 1) * (fDivReal (fun x ↦ (a - 1)⁻¹ * (x ^ a - 1)) μ ν).toReal) := by
   rw [renyiReal, if_neg ha_pos.ne', if_neg ha_lt_one.ne, if_pos (Or.inl ha_lt_one)]
 
 lemma renyiReal_of_one_lt (ha_one_lt : 1 < a) (hμν : μ ≪ ν) :
     renyiReal a μ ν
-      = (a - 1)⁻¹ * log (1 + (a - 1) * fDivReal (fun x ↦ (a - 1)⁻¹ * (x ^ a - 1)) μ ν) := by
+      = (a - 1)⁻¹ * log (1 + (a - 1) * (fDivReal (fun x ↦ (a - 1)⁻¹ * (x ^ a - 1)) μ ν).toReal) := by
   rw [renyiReal, if_neg (zero_lt_one.trans ha_one_lt).ne', if_neg ha_one_lt.ne',
     if_pos (Or.inr hμν)]
 
diff --git a/TestingLowerBounds/SoonInMathlib/RadonNikodym.lean b/TestingLowerBounds/SoonInMathlib/RadonNikodym.lean
index 75de8142..34063598 100644
--- a/TestingLowerBounds/SoonInMathlib/RadonNikodym.lean
+++ b/TestingLowerBounds/SoonInMathlib/RadonNikodym.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 import TestingLowerBounds.SoonInMathlib.Density
 import Mathlib.Probability.Kernel.WithDensity
 import Mathlib.Probability.Kernel.MeasureCompProd
+import TestingLowerBounds.ForMathlib.RnDeriv
 
 /-!
 # Radon-Nikodym derivative and Lebesgue decomposition for kernels
@@ -451,13 +452,13 @@ lemma Measure.absolutelyContinuous_compProd_right (μ : Measure α) {κ η : ker
     at hs_zero ⊢
   filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero
 
--- ok
+-- PRed a version with `∀ᵐ a ∂ν, κ a ≪ η a`
 lemma Measure.absolutelyContinuous_compProd {μ ν : Measure α} {κ η : kernel α γ}
     [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η]
-    (hμν : μ ≪ ν) (hκη : ∀ᵐ a ∂ν, κ a ≪ η a) :
+    (hμν : μ ≪ ν) (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
     μ ⊗ₘ κ ≪ ν ⊗ₘ η :=
-  (Measure.absolutelyContinuous_compProd_left hμν κ).trans
-    (Measure.absolutelyContinuous_compProd_right ν hκη)
+  (Measure.absolutelyContinuous_compProd_right μ hκη).trans
+    (Measure.absolutelyContinuous_compProd_left hμν _)
 
 lemma Measure.mutuallySingular_compProd_left {μ ν : Measure α} [SFinite μ] [SFinite ν]
     (hμν : μ ⟂ₘ ν) (κ η : kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
@@ -635,7 +636,7 @@ lemma rnDeriv_measure_compProd_aux {μ ν : Measure α} {κ η : kernel α γ}
       = (μ ⊗ₘ κ) s := by
     intro s _
     rw [Measure.set_lintegral_rnDeriv]
-    exact Measure.absolutelyContinuous_compProd hμν hκη
+    exact Measure.absolutelyContinuous_compProd hμν (hμν hκη)
   have : ∀ s t, MeasurableSet s → MeasurableSet t →
       ∫⁻ x in s, ∫⁻ y in t, (∂μ/∂ν) x * rnDeriv κ η x y ∂(η x) ∂ν = (μ ⊗ₘ κ) (s ×ˢ t) :=
     fun _ _ hs ht ↦ set_lintegral_prod_rnDeriv hμν hκη hs ht
@@ -810,6 +811,101 @@ lemma rnDeriv_measure_compProd_right' (μ : Measure α) (κ η : kernel α γ)
   filter_upwards [ha, h a] with b hb1 hb2
   rw [hb1, hb2]
 
+lemma Measure.absolutelyContinuous_compProd_left_iff
+    {μ ν : Measure α} {κ : kernel α γ}
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsMarkovKernel κ]  :
+    μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν := by
+  refine ⟨fun h ↦ ?_, fun h ↦ Measure.absolutelyContinuous_compProd_left h _⟩
+  refine Measure.AbsolutelyContinuous.mk (fun s hs hs0 ↦ ?_)
+  have h1 : (ν ⊗ₘ κ) (s ×ˢ univ) = 0 := by
+    rw [Measure.compProd_apply_prod hs MeasurableSet.univ]
+    exact Measure.set_lintegral_eq_zero_of_null hs0
+  have h2 := h h1
+  rw [Measure.compProd_apply_prod hs MeasurableSet.univ] at h2
+  simpa using h2
+
+lemma Measure.absolutelyContinuous_add_left_iff (μ₁ μ₂ ν : Measure α) :
+    μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν := by
+  refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
+  · constructor
+    · intro s hs0
+      specialize h hs0
+      simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] at h
+      exact h.1
+    · intro s hs0
+      specialize h hs0
+      simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] at h
+      exact h.2
+  · refine Measure.absolutelyContinuous_of_le_smul (c := 2) (le_of_eq ?_)
+    ext
+    simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply,
+      Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, smul_eq_mul]
+    rw [two_mul]
+
+lemma eq_zero_of_absolutelyContinuous_of_mutuallySingular (h_ac : μ ≪ η) (h_ms : μ ⟂ₘ η) :
+    μ = 0 := by
+  let s := h_ms.nullSet
+  suffices μ s = 0 ∧ μ sᶜ = 0 by
+    suffices μ univ = 0 by
+      rwa [Measure.measure_univ_eq_zero] at this
+    rw [← union_compl_self s, measure_union disjoint_compl_right h_ms.measurableSet_nullSet.compl,
+      this.1, this.2, add_zero]
+  exact ⟨h_ms.measure_nullSet, h_ac h_ms.measure_compl_nullSet⟩
+
+lemma Measure.absolutelyContinuous_compProd_right_iff
+    {μ : Measure α} {κ η : kernel α γ}
+    [SFinite μ] [IsFiniteKernel κ] [IsFiniteKernel η] :
+    μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a := by
+  refine ⟨fun h ↦ ?_, fun h ↦ Measure.absolutelyContinuous_compProd_right _ h⟩
+  suffices ∀ᵐ a ∂μ, kernel.singularPart κ η a = 0 by
+    filter_upwards [this] with a ha
+    rwa [singularPart_eq_zero_iff_absolutelyContinuous] at ha
+  rw [← rnDeriv_add_singularPart κ η, Measure.compProd_add_right,
+    Measure.absolutelyContinuous_add_left_iff] at h
+  have : μ ⊗ₘ singularPart κ η ⟂ₘ μ ⊗ₘ η :=
+    Measure.mutuallySingular_compProd_right μ μ (mutuallySingular_singularPart _ _)
+  have h_zero : μ ⊗ₘ singularPart κ η = 0 :=
+    eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
+  simp_rw [← Measure.measure_univ_eq_zero]
+  refine (lintegral_eq_zero_iff (kernel.measurable_coe _ MeasurableSet.univ)).mp ?_
+  rw [← set_lintegral_univ, ← Measure.compProd_apply_prod MeasurableSet.univ MeasurableSet.univ,
+    h_zero]
+  simp
+
+lemma Measure.absolutelyContinuous_of_absolutelyContinuous_compProd
+    {μ ν : Measure α} {κ η : kernel α γ}
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsMarkovKernel κ] [IsFiniteKernel η]
+    (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
+    μ ≪ ν := by
+  refine Measure.AbsolutelyContinuous.mk (fun s hs hs0 ↦ ?_)
+  have h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0 := by
+    rw [Measure.compProd_apply_prod hs MeasurableSet.univ]
+    exact Measure.set_lintegral_eq_zero_of_null hs0
+  have h2 := h h1
+  rw [Measure.compProd_apply_prod hs MeasurableSet.univ] at h2
+  simpa using h2
+
+lemma Measure.absolutelyContinuous_compProd_iff
+    {μ ν : Measure α} {κ η : kernel α γ}
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsMarkovKernel κ] [IsFiniteKernel η] :
+    μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a := by
+  refine ⟨fun h ↦ ⟨Measure.absolutelyContinuous_of_absolutelyContinuous_compProd h, ?_⟩,
+    fun h ↦ Measure.absolutelyContinuous_compProd h.1 h.2⟩
+  suffices ∀ᵐ a ∂μ, kernel.singularPart κ η a = 0 by
+    filter_upwards [this] with a ha
+    rwa [singularPart_eq_zero_iff_absolutelyContinuous] at ha
+  rw [← rnDeriv_add_singularPart κ η, Measure.compProd_add_right,
+    Measure.absolutelyContinuous_add_left_iff] at h
+  have : μ ⊗ₘ singularPart κ η ⟂ₘ ν ⊗ₘ η :=
+    Measure.mutuallySingular_compProd_right μ ν (mutuallySingular_singularPart _ _)
+  have h_zero : μ ⊗ₘ singularPart κ η = 0 :=
+    eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
+  simp_rw [← Measure.measure_univ_eq_zero]
+  refine (lintegral_eq_zero_iff (kernel.measurable_coe _ MeasurableSet.univ)).mp ?_
+  rw [← set_lintegral_univ, ← Measure.compProd_apply_prod MeasurableSet.univ MeasurableSet.univ,
+    h_zero]
+  simp
+
 end MeasureCompProd
 
 end ProbabilityTheory.kernel
diff --git a/TestingLowerBounds/TotalVariation.lean b/TestingLowerBounds/TotalVariation.lean
index e1943b1e..6e90b71c 100644
--- a/TestingLowerBounds/TotalVariation.lean
+++ b/TestingLowerBounds/TotalVariation.lean
@@ -42,6 +42,6 @@ namespace ProbabilityTheory
 variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α}
 
 /-- Total variation distance between two measures. -/
-noncomputable def tv (μ ν : Measure α) : ℝ := fDivReal (fun x ↦ 2⁻¹ * |1 - x|) μ ν
+noncomputable def tv (μ ν : Measure α) : ℝ := (fDivReal (fun x ↦ 2⁻¹ * |1 - x|) μ ν).toReal
 
 end ProbabilityTheory