Merge branch 'LL/fDiv' into LL/DPIAbsCont

TestingLowerBounds.lean

@@ -29,6 +29,7 @@ import TestingLowerBounds.ForMathlib.Measure
 import TestingLowerBounds.ForMathlib.MonotoneOnTendsto
 import TestingLowerBounds.ForMathlib.RadonNikodym
 import TestingLowerBounds.ForMathlib.RnDeriv
+import TestingLowerBounds.ForMathlib.SetIntegral
 import TestingLowerBounds.Kernel.Basic
 import TestingLowerBounds.Kernel.BayesInv
 import TestingLowerBounds.Kernel.Monoidal

TestingLowerBounds/Divergences/Hellinger.lean

@@ -222,17 +222,16 @@ lemma convexOn_hellingerFun (ha_pos : 0 ≤ a) : ConvexOn ℝ (Set.Ici 0) (helli
     refine ConvexOn.smul (by simp [ha.le]) ?_
     exact h.sub (concaveOn_const _ (convex_Ici 0))
 
-lemma tendsto_hellingerFun_div_atTop_of_one_lt (ha : 1 < a) :
-    Tendsto (fun x ↦ hellingerFun a x / x) atTop atTop := by
+lemma tendsto_rightDeriv_hellingerFun_atTop_of_one_lt (ha : 1 < a) :
+    Tendsto (rightDeriv (hellingerFun a)) atTop atTop := by
   sorry
 
-lemma tendsto_hellingerFun_div_atTop_of_lt_one (ha : a < 1) :
-    Tendsto (fun x ↦ hellingerFun a x / x) atTop (𝓝 0) := by
+lemma tendsto_rightDeriv_hellingerFun_atTop_of_lt_one (ha : a < 1) :
+    Tendsto (rightDeriv (hellingerFun a)) atTop (𝓝 0) := by
   sorry
 
-lemma derivAtTop_hellingerFun_of_one_lt (ha : 1 < a) : derivAtTop (hellingerFun a) = ⊤ := by
-  rw [derivAtTop, if_pos]
-  exact tendsto_hellingerFun_div_atTop_of_one_lt ha
+lemma derivAtTop_hellingerFun_of_one_lt (ha : 1 < a) : derivAtTop (hellingerFun a) = ⊤ :=
+  derivAtTop_of_tendsto_atTop <| tendsto_rightDeriv_hellingerFun_atTop_of_one_lt ha
 
 lemma derivAtTop_hellingerFun_of_one_le (ha : 1 ≤ a) :
     derivAtTop (hellingerFun a) = ⊤ := by
@@ -243,7 +242,7 @@ lemma derivAtTop_hellingerFun_of_one_le (ha : 1 ≤ a) :
 
 lemma derivAtTop_hellingerFun_of_lt_one (ha : a < 1) :
     derivAtTop (hellingerFun a) = 0 :=
-  derivAtTop_of_tendsto (tendsto_hellingerFun_div_atTop_of_lt_one ha)
+  derivAtTop_of_tendsto_nhds <| tendsto_rightDeriv_hellingerFun_atTop_of_lt_one ha
 
 lemma integrable_hellingerFun_iff_integrable_rpow (ha_one : a ≠ 1) [IsFiniteMeasure ν] :
     Integrable (fun x ↦ hellingerFun a ((∂μ/∂ν) x).toReal) ν

TestingLowerBounds/Divergences/KullbackLeibler.lean

@@ -61,12 +61,16 @@ lemma kl_toReal_of_ac (h : μ ≪ ν) : (kl μ ν).toReal = ∫ a, llr μ ν a 
   · rw [kl_of_ac_of_integrable h h_int, EReal.toReal_coe]
   · rw [kl_of_not_integrable h_int, integral_undef h_int, EReal.toReal_top]
 
+lemma rightDeriv_mul_log {x : ℝ} (hx : 0 ≤ x) : rightDeriv (fun x ↦ x * log x) x = log x + 1 := by
+  sorry
+
 lemma derivAtTop_mul_log : derivAtTop (fun x ↦ x * log x) = ⊤ := by
-  rw [derivAtTop_eq_top_iff]
-  refine (tendsto_congr' ?_).mp tendsto_log_atTop
-  simp only [EventuallyEq, eventually_atTop, ge_iff_le]
-  refine ⟨1, fun x hx ↦ ?_⟩
-  rw [mul_div_cancel_left₀ _ (zero_lt_one.trans_le hx).ne']
+  refine derivAtTop_of_tendsto_atTop ?_
+  have h_tendsto : Tendsto (fun x ↦ log x + 1) atTop atTop :=
+    tendsto_log_atTop.atTop_add tendsto_const_nhds
+  refine (tendsto_congr' ?_).mpr h_tendsto
+  rw [EventuallyEq, eventually_atTop]
+  exact ⟨0, fun _ ↦ rightDeriv_mul_log⟩
 
 lemma fDiv_mul_log_eq_top_iff [IsFiniteMeasure μ] [SigmaFinite ν] :
     fDiv (fun x ↦ x * log x) μ ν = ⊤ ↔ μ ≪ ν → ¬ Integrable (llr μ ν) μ := by
@@ -405,7 +409,7 @@ lemma condKL_nonneg (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel 
 lemma condKL_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     condKL (Kernel.const β μ) (Kernel.const β ν) ξ = (kl μ ν) * ξ Set.univ := by
   rw [condKL_eq_condFDiv, kl_eq_fDiv]
-  exact condFDiv_const
+  exact condFDiv_const convexOn_mul_log
 
 lemma kl_fst_le [Nonempty β] [StandardBorelSpace β]
     (μ ν : Measure (α × β)) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :

TestingLowerBounds/FDiv/Trim.lean

@@ -23,7 +23,7 @@ import TestingLowerBounds.FDiv.Basic
 
 -/
 
-open Real MeasureTheory Filter
+open Real MeasureTheory Filter Set
 
 open scoped ENNReal NNReal Topology
 
@@ -34,15 +34,15 @@ variable {α β : Type*} {m mα : MeasurableSpace α} {mβ : MeasurableSpace β}
 
 lemma f_condexp_rnDeriv_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα)
     (hf : StronglyMeasurable f)
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     (fun x ↦ f ((ν[fun x ↦ ((∂μ/∂ν) x).toReal | m]) x))
       ≤ᵐ[ν.trim hm] ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] := by
   sorry -- Jensen for condexp. We don't have it yet.
 
 lemma f_rnDeriv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν)
     (hf : StronglyMeasurable f)
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal)
       ≤ᵐ[ν.trim hm] ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] := by
@@ -54,7 +54,7 @@ lemma f_rnDeriv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ m
 
 lemma integrable_f_rnDeriv_trim [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν)
     (hf : StronglyMeasurable f)
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     Integrable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm) := by
   obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x :=
@@ -74,7 +74,7 @@ lemma integrable_f_rnDeriv_trim [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm :
 lemma integrable_f_condexp_rnDeriv [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hm : m ≤ mα) (hμν : μ ≪ ν)
     (hf : StronglyMeasurable f)
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     Integrable (fun x ↦ f ((ν[fun x ↦ ((∂μ/∂ν) x).toReal | m]) x)) ν := by
   have h := integrable_f_rnDeriv_trim hm hμν hf hf_cvx hf_cont h_int
@@ -84,7 +84,7 @@ lemma integrable_f_condexp_rnDeriv [IsFiniteMeasure μ] [IsFiniteMeasure ν]
 
 lemma fDiv_trim_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν)
     (hf : StronglyMeasurable f)
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0))
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     fDiv f (μ.trim hm) (ν.trim hm) = ∫ x, f ((ν[fun x ↦ ((∂μ/∂ν) x).toReal | m]) x) ∂ν := by
   classical
@@ -99,7 +99,7 @@ lemma fDiv_trim_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα)
 
 lemma fDiv_trim_le_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν)
     (hf : StronglyMeasurable f)
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) :
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) :
     fDiv f (μ.trim hm) (ν.trim hm) ≤ fDiv f μ ν := by
   by_cases h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
   swap; · rw [fDiv_of_not_integrable h_int]; exact le_top
@@ -115,7 +115,7 @@ lemma fDiv_trim_le_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ m
 
 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)) :
+    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) :
     fDiv f (μ.trim hm) (ν.trim hm) ≤ fDiv f μ ν := by
   have h1 : μ.trim hm = (ν.withDensity (∂μ/∂ν)).trim hm + (μ.singularPart ν).trim hm := by
     conv_lhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, trim_add]

TestingLowerBounds/ForMathlib/LeftRightDeriv.lean

@@ -13,7 +13,7 @@ open Set Filter Topology
 
 open scoped ENNReal NNReal
 
-variable {f : ℝ → ℝ}
+variable {f : ℝ → ℝ} {x : ℝ}
 
 /-- The right derivative of a real function. -/
 noncomputable
@@ -70,6 +70,33 @@ lemma leftDeriv_eq_rightDeriv (f : ℝ → ℝ) :
   ext x
   simp [leftDeriv_eq_rightDeriv_apply]
 
+lemma Filter.EventuallyEq.derivWithin_eq_nhds {𝕜 F : Type*} [NontriviallyNormedField 𝕜]
+    [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}
+    (h : f₁ =ᶠ[𝓝 x] f) :
+    derivWithin f₁ s x = derivWithin f s x := by
+  simp_rw [derivWithin]
+  rw [Filter.EventuallyEq.fderivWithin_eq_nhds h]
+
+lemma Filter.EventuallyEq.rightDeriv_eq_nhds {x : ℝ} {g : ℝ → ℝ} (h : f =ᶠ[𝓝 x] g) :
+    rightDeriv f x = rightDeriv g x := h.derivWithin_eq_nhds
+
+lemma rightDeriv_congr_atTop {g : ℝ → ℝ} (h : f =ᶠ[atTop] g) :
+    rightDeriv f =ᶠ[atTop] rightDeriv g := by
+  have h' : ∀ᶠ x in atTop, f =ᶠ[𝓝 x] g := by
+    -- todo: replace by clean filter proof?
+    simp only [Filter.EventuallyEq, eventually_atTop, ge_iff_le] at h ⊢
+    obtain ⟨a, ha⟩ := h
+    refine ⟨a + 1, fun b hab ↦ ?_⟩
+    have h_ge : ∀ᶠ x in 𝓝 b, a ≤ x := eventually_ge_nhds ((lt_add_one _).trans_le hab)
+    filter_upwards [h_ge] using ha
+  filter_upwards [h'] with a ha using ha.rightDeriv_eq_nhds
+
+@[simp]
+lemma rightDeriv_zero : rightDeriv 0 = 0 := by
+  ext x
+  simp only [rightDeriv, Pi.zero_apply]
+  exact derivWithin_const x _ 0 (uniqueDiffWithinAt_Ioi x)
+
 @[simp]
 lemma rightDeriv_const (c : ℝ) : rightDeriv (fun _ ↦ c) = 0 := by
   ext x
@@ -129,6 +156,11 @@ lemma rightDeriv_add_apply {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWit
   simp_rw [rightDeriv_def, ← derivWithin_add (uniqueDiffWithinAt_Ioi x) hf hg]
   rfl
 
+lemma rightDeriv_add_apply' {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Ioi x) x)
+    (hg : DifferentiableWithinAt ℝ g (Ioi x) x) :
+    rightDeriv (fun x ↦ f x + g x) x = rightDeriv f x + rightDeriv g x :=
+  rightDeriv_add_apply hf hg
+
 lemma rightDeriv_add {f g : ℝ → ℝ} (hf : ∀ x, DifferentiableWithinAt ℝ f (Ioi x) x)
     (hg : ∀ x, DifferentiableWithinAt ℝ g (Ioi x) x) :
     rightDeriv (f + g) = fun x ↦ rightDeriv f x + rightDeriv g x := by
@@ -184,6 +216,12 @@ lemma bddBelow_slope_Ioi (hfc : ConvexOn ℝ univ f) (x : ℝ) :
   simp_rw [mem_Ici, ← hz']
   exact slope_mono hfc trivial (by simp) ⟨trivial, hz.ne'⟩ (by linarith)
 
+lemma bddBelow_slope_Ioi' (hfc : ConvexOn ℝ (Ici 0) f) (x : ℝ) (hx : 0 < x) :
+    BddBelow (slope f x '' Ioi x) := by
+  refine bddBelow_iff_subset_Ici.mpr ⟨(slope f x 0), fun y ⟨z, (hz : x < z), hz'⟩ ↦ ?_⟩
+  simp_rw [mem_Ici, ← hz']
+  exact slope_mono hfc hx.le (by simp [hx.ne]) ⟨(hx.trans hz).le, hz.ne'⟩ (by linarith)
+
 lemma bddAbove_slope_Iio (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     BddAbove (slope f x '' Iio x) := by
   refine bddAbove_iff_subset_Iic.mpr ⟨(slope f x (x + 1)), fun y ⟨z, (hz : z < x), hz'⟩ ↦ ?_⟩
@@ -192,7 +230,17 @@ lemma bddAbove_slope_Iio (hfc : ConvexOn ℝ univ f) (x : ℝ) :
 
 end Slope
 
--- TODO: this can be generalized to a set S, where the function is convex, but I still need to figure out what hp to require, since the minimal assumption I think is that there exist a right interval of x that is contained in S (so x itself does not have to be in S), i.e. (x, y) ⊆ S, I don't know if. To generalize we will need MonotoneOn.tendsto_nhdsWithin_Ioo_right. However there are dirrerent kinds of sufficient conditions that could be given, for example S open and x in S or x in the interior of S. Discuss this with Remy. Maybe the minimal hp I described is not sufficient, I also need to assure some kind of boundedness of the slope, this should be assured if x is in the interior of S, because then we can take a point to the left of x but still inside S and use the monotonicity of the solpe in S, but can we do better? For now we can leave it like this
+-- TODO: this can be generalized to a set S, where the function is convex,
+-- but I still need to figure out what hp to require,
+-- since the minimal assumption I think is that there exist a right interval of x
+-- that is contained in S (so x itself does not have to be in S), i.e. (x, y) ⊆ S, I don't know if.
+-- To generalize we will need MonotoneOn.tendsto_nhdsWithin_Ioo_right.
+-- However there are dirrerent kinds of sufficient conditions that could be given,
+-- for example S open and x in S or x in the interior of S. Discuss this with Remy.
+-- Maybe the minimal hp I described is not sufficient, I also need to assure some kind
+-- of boundedness of the slope, this should be assured if x is in the interior of S,
+-- because then we can take a point to the left of x but still inside S and use the monotonicity
+-- of the solpe in S, but can we do better? For now we can leave it like this
 lemma hasRightDerivAt (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     HasDerivWithinAt f (sInf (slope f x '' Ioi x)) (Ioi x) x := by
   simp_rw [hasDerivWithinAt_iff_tendsto_slope]
@@ -203,10 +251,24 @@ lemma hasRightDerivAt (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     exact hfc.secant_mono trivial trivial trivial hy.ne' hz.ne' hz'.le
   exact MonotoneOn.tendsto_nhdsWithin_Ioi h_mono (bddBelow_slope_Ioi hfc x)
 
+lemma hasRightDerivAt' (hfc : ConvexOn ℝ (Ici 0) f) (hx : 0 < x) :
+    HasDerivWithinAt f (sInf (slope f x '' Ioi x)) (Ioi x) x := by
+  simp_rw [hasDerivWithinAt_iff_tendsto_slope]
+  simp only [mem_Ioi, lt_self_iff_false, not_false_eq_true, diff_singleton_eq_self]
+  have h_mono : MonotoneOn (slope f x) (Ioi x) := by
+    refine monotoneOn_iff_forall_lt.mpr fun y (hy : x < y) z (hz : x < z) hz' ↦ ?_
+    simp_rw [slope_def_field]
+    exact hfc.secant_mono hx.le (hx.trans hy).le (hx.trans hz).le hy.ne' hz.ne' hz'.le
+  exact MonotoneOn.tendsto_nhdsWithin_Ioi h_mono (bddBelow_slope_Ioi' hfc x hx)
+
 lemma differentiableWithinAt_Ioi (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     DifferentiableWithinAt ℝ f (Ioi x) x :=
   (hfc.hasRightDerivAt x).differentiableWithinAt
 
+lemma differentiableWithinAt_Ioi' (hfc : ConvexOn ℝ (Ici 0) f) (hx : 0 < x) :
+    DifferentiableWithinAt ℝ f (Ioi x) x :=
+  (hfc.hasRightDerivAt' hx).differentiableWithinAt
+
 lemma hadDerivWithinAt_rightDeriv (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     HasDerivWithinAt f (rightDeriv f x) (Ioi x) x :=
   (hfc.differentiableWithinAt_Ioi x).hasDerivWithinAt
@@ -233,6 +295,10 @@ lemma rightDeriv_eq_sInf_slope (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     rightDeriv f x = sInf (slope f x '' Ioi x) :=
   (hfc.hasRightDerivAt x).derivWithin (uniqueDiffWithinAt_Ioi x)
 
+lemma rightDeriv_eq_sInf_slope' (hfc : ConvexOn ℝ (Ici 0) f) (hx : 0 < x) :
+    rightDeriv f x = sInf (slope f x '' Ioi x) :=
+  (hfc.hasRightDerivAt' hx).derivWithin (uniqueDiffWithinAt_Ioi x)
+
 lemma leftDeriv_eq_sSup_slope (hfc : ConvexOn ℝ univ f) (x : ℝ) :
     leftDeriv f x = sSup (slope f x '' Iio x) :=
   (hfc.hasLeftDerivAt x).derivWithin (uniqueDiffWithinAt_Iio x)
@@ -247,6 +313,16 @@ lemma rightDeriv_mono (hfc : ConvexOn ℝ univ f) : Monotone (rightDeriv f) := b
   rw [slope_comm]
   exact slope_mono hfc trivial ⟨trivial, hxy.ne⟩ ⟨trivial, yz.ne'⟩ (hxy.trans yz).le
 
+lemma rightDeriv_mono' (hfc : ConvexOn ℝ (Ici 0) f) : MonotoneOn (rightDeriv f) (Ioi 0) := by
+  intro x (hx : 0 < x) y (hy : 0 < y) hxy
+  rcases eq_or_lt_of_le hxy with rfl | hxy; · rfl
+  rw [hfc.rightDeriv_eq_sInf_slope' hx, hfc.rightDeriv_eq_sInf_slope' hy]
+  refine csInf_le_of_le (b := slope f x y) (bddBelow_slope_Ioi' hfc x hx)
+    ⟨y, by simp [hxy]⟩ (le_csInf nonempty_of_nonempty_subtype ?_)
+  rintro _ ⟨z, (yz : y < z), rfl⟩
+  rw [slope_comm]
+  exact slope_mono hfc hy.le ⟨hx.le, hxy.ne⟩ ⟨hy.le.trans yz.le, yz.ne'⟩ (hxy.trans yz).le
+
 lemma leftDeriv_mono (hfc : ConvexOn ℝ univ f) : Monotone (leftDeriv f) := by
   rw [leftDeriv_eq_rightDeriv]
   change Monotone (- rightDeriv (f ∘ Neg.neg) ∘ Neg.neg)