progress towards fDiv_trim_le

RemyDegenne · Mar 28, 2024 · bc60d35 · bc60d35
1 parent c613a6a
commit bc60d35
Show file tree

Hide file tree

Showing 3 changed files with 86 additions and 0 deletions.
diff --git a/TestingLowerBounds/DerivAtTop.lean b/TestingLowerBounds/DerivAtTop.lean
@@ -177,6 +177,11 @@ lemma le_add_derivAtTop (h_cvx : ConvexOn ℝ (Set.Ici 0) f)
     f x ≤ f y + (derivAtTop f).toReal * (x - y) := by
   sorry
 
+lemma le_add_derivAtTop'' (h_cvx : ConvexOn ℝ (Set.Ici 0) f)
+    (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
+    f (x + y) ≤ f x + (derivAtTop f).toReal * y := by
+  sorry
+
 lemma le_add_derivAtTop' (h_cvx : ConvexOn ℝ (Set.Ici 0) f)
     (h : derivAtTop f ≠ ⊤) {x u : ℝ} (hx : 0 ≤ x) (hu : 0 ≤ u) :
     f x ≤ f (x * u) + (derivAtTop f).toReal * x * (1 - u) := by

diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean
@@ -351,13 +351,36 @@ lemma fDiv_eq_add_withDensity_singularPart''
     sub_eq_add_neg]
   exact hf_cvx
 
+lemma fDiv_eq_add_withDensity_derivAtTop
+    (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν Set.univ := by
+  rw [fDiv_eq_add_withDensity_singularPart'' μ ν hf_cvx,
+    fDiv_of_mutuallySingular (Measure.mutuallySingular_singularPart _ _),
+    derivAtTop_sub_const hf_cvx]
+  simp
+
 lemma fDiv_lt_top_of_ac [SigmaFinite μ] [SigmaFinite ν] (h : μ ≪ ν)
     (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     fDiv f μ ν < ⊤ := by
   classical
   rw [fDiv_of_absolutelyContinuous h, if_pos h_int]
   simp
 
+lemma fDiv_absolutelyContinuous_add_mutuallySingular {μ₁ μ₂ ν : Measure α}
+    [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] [IsFiniteMeasure ν] (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ⟂ₘ ν)
+    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    fDiv f (μ₁ + μ₂) ν = fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by
+  rw [fDiv_eq_add_withDensity_derivAtTop  _ _ hf_cvx, Measure.singularPart_add,
+    Measure.singularPart_eq_zero_of_ac h₁, Measure.singularPart_eq_self.mpr h₂, zero_add]
+  congr
+  conv_rhs => rw [← Measure.withDensity_rnDeriv_eq μ₁ ν h₁]
+  refine withDensity_congr_ae ?_
+  refine (Measure.rnDeriv_add' _ _ _).trans ?_
+  filter_upwards [Measure.rnDeriv_eq_zero_of_mutuallySingular h₂ Measure.AbsolutelyContinuous.rfl]
+    with x hx
+  simp [hx]
+
 section derivAtTopTop
 
 lemma fDiv_of_not_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivAtTop f = ⊤) (hμν : ¬ μ ≪ ν) :

diff --git a/TestingLowerBounds/FDiv/Trim.lean b/TestingLowerBounds/FDiv/Trim.lean
@@ -114,4 +114,62 @@ lemma fDiv_trim_le_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ m
   refine ae_of_ae_trim hm ?_
   exact f_condexp_rnDeriv_le hm hf hf_cvx hf_cont h_int
 
+lemma fdiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ≪ ν) :
+    fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by
+  classical
+  rw [fDiv_of_absolutelyContinuous (Measure.AbsolutelyContinuous.add_left_iff.mpr ⟨h₁, h₂⟩), if_pos]
+  swap; · sorry
+  rw [fDiv_of_absolutelyContinuous h₁, if_pos]
+  swap; · sorry
+  sorry
+
+lemma Measure.trim_add (μ ν : Measure α) (hm : m ≤ mα) :
+    (μ + ν).trim hm = μ.trim hm + ν.trim hm := by
+  refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)
+  simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply,
+    trim_measurableSet_eq hm hs]
+
+lemma fDiv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα)
+    (hf : StronglyMeasurable f)
+    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) :
+    fDiv f (μ.trim hm) (ν.trim hm) ≤ fDiv f μ ν := by
+  let μ' := μ.singularPart ν
+  have h1 : μ.trim hm = (ν.withDensity (∂μ/∂ν)).trim hm
+      + (ν.trim hm).withDensity (∂(μ'.trim hm)/∂(ν.trim hm))
+      + (μ'.trim hm).singularPart (ν.trim hm) := by
+    conv_lhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, Measure.trim_add,
+      ← Measure.rnDeriv_add_singularPart ((μ.singularPart ν).trim hm) (ν.trim hm), ← add_assoc]
+  rw [h1, fDiv_absolutelyContinuous_add_mutuallySingular _
+    (Measure.mutuallySingular_singularPart _ _) hf_cvx]
+  swap
+  · rw [Measure.AbsolutelyContinuous.add_left_iff]
+    constructor
+    · exact (withDensity_absolutelyContinuous _ _).trim hm
+    · exact withDensity_absolutelyContinuous _ _
+  calc fDiv f ((ν.withDensity (∂μ/∂ν)).trim hm + (ν.trim hm).withDensity (∂μ'.trim hm/∂ν.trim hm))
+        (ν.trim hm)
+      + derivAtTop f * (μ'.trim hm).singularPart (ν.trim hm) Set.univ
+    ≤ fDiv f ((ν.withDensity (∂μ/∂ν)).trim hm) (ν.trim hm)
+      + derivAtTop f * (ν.trim hm).withDensity (∂μ'.trim hm/∂ν.trim hm) Set.univ
+      + derivAtTop f * (μ'.trim hm).singularPart (ν.trim hm) Set.univ := by
+        gcongr
+        refine fdiv_add_measure_le_of_ac ?_ ?_
+        · exact (withDensity_absolutelyContinuous _ _).trim hm
+        · exact withDensity_absolutelyContinuous _ _
+  _ = fDiv f ((ν.withDensity (∂μ/∂ν)).trim hm) (ν.trim hm)
+      + derivAtTop f * ((ν.trim hm).withDensity (∂μ'.trim hm/∂ν.trim hm)
+        + (μ'.trim hm).singularPart (ν.trim hm)) Set.univ := by
+        simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply,
+          EReal.coe_ennreal_add]
+        sorry
+  _ = fDiv f ((ν.withDensity (∂μ/∂ν)).trim hm) (ν.trim hm)
+      + derivAtTop f * μ'.trim hm Set.univ := by
+        conv_rhs => rw [← Measure.rnDeriv_add_singularPart (μ'.trim hm) (ν.trim hm)]
+  _ = fDiv f ((ν.withDensity (∂μ/∂ν)).trim hm) (ν.trim hm) + derivAtTop f * μ' Set.univ := by
+        rw [trim_measurableSet_eq hm MeasurableSet.univ]
+  _ ≤ fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ' Set.univ := by
+        gcongr
+        exact fDiv_trim_le_of_ac hm (withDensity_absolutelyContinuous _ _) hf hf_cvx hf_cont
+  _ = fDiv f μ ν := by conv_rhs => rw [fDiv_eq_add_withDensity_derivAtTop _ _ hf_cvx]
+
 end ProbabilityTheory