Merge remote-tracking branch 'upstream/master' into TestLeanCopilot

TestingLowerBounds.lean

@@ -10,23 +10,29 @@ import TestingLowerBounds.Divergences.KullbackLeibler
 import TestingLowerBounds.Divergences.Renyi
 import TestingLowerBounds.Divergences.StatInfo
 import TestingLowerBounds.Divergences.TotalVariation
+import TestingLowerBounds.Divergences.fDivStatInfo
 import TestingLowerBounds.ErealLLR
 import TestingLowerBounds.FDiv.Basic
 import TestingLowerBounds.FDiv.CompProd
 import TestingLowerBounds.FDiv.CondFDiv
+import TestingLowerBounds.FDiv.CondFDivCompProdMeasure
 import TestingLowerBounds.FDiv.IntegralRnDerivSingularPart
+import TestingLowerBounds.FDiv.Measurable
 import TestingLowerBounds.FDiv.Trim
+import TestingLowerBounds.FindAxioms
 import TestingLowerBounds.ForMathlib.ByParts
 import TestingLowerBounds.ForMathlib.CountableOrCountablyGenerated
 import TestingLowerBounds.ForMathlib.EReal
 import TestingLowerBounds.ForMathlib.GiryMonad
+import TestingLowerBounds.ForMathlib.Integrable
 import TestingLowerBounds.ForMathlib.Integrable_of_empty
 import TestingLowerBounds.ForMathlib.KernelFstSnd
 import TestingLowerBounds.ForMathlib.LeftRightDeriv
 import TestingLowerBounds.ForMathlib.LogLikelihoodRatioCompProd
 import TestingLowerBounds.ForMathlib.MaxMinEqAbs
 import TestingLowerBounds.ForMathlib.RadonNikodym
 import TestingLowerBounds.ForMathlib.RnDeriv
+import TestingLowerBounds.IntegrableFRNDeriv
 import TestingLowerBounds.Kernel.Basic
 import TestingLowerBounds.Kernel.BayesInv
 import TestingLowerBounds.Kernel.Deterministic

TestingLowerBounds/CompProd.lean

@@ -3,6 +3,8 @@ 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, Lorenzo Luccioli
 -/
+import TestingLowerBounds.Convex
+import TestingLowerBounds.ForMathlib.Integrable
 import TestingLowerBounds.ForMathlib.RadonNikodym
 
 /-!
@@ -11,7 +13,7 @@ import TestingLowerBounds.ForMathlib.RadonNikodym
 
 -/
 
-open Real MeasureTheory Filter
+open Real MeasureTheory Filter MeasurableSpace
 
 open scoped ENNReal NNReal Topology
 
@@ -22,7 +24,7 @@ variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β
 
 section SingularPart
 
-lemma singularPart_compProd'' [MeasurableSpace.CountableOrCountablyGenerated α β]
+lemma singularPart_compProd'' [CountableOrCountablyGenerated α β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
     (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η)
@@ -47,7 +49,7 @@ lemma singularPart_compProd'' [MeasurableSpace.CountableOrCountablyGenerated α
     exact Kernel.Measure.mutuallySingular_compProd_right (ν.withDensity (∂μ/∂ν)) ν
       (.of_forall <| κ.mutuallySingular_singularPart _)
 
-lemma singularPart_compProd [MeasurableSpace.CountableOrCountablyGenerated α β]
+lemma singularPart_compProd [CountableOrCountablyGenerated α β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
     (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η)
@@ -59,7 +61,7 @@ lemma singularPart_compProd [MeasurableSpace.CountableOrCountablyGenerated α β
   rw [this]
   abel
 
-lemma singularPart_compProd' [MeasurableSpace.CountableOrCountablyGenerated α β]
+lemma singularPart_compProd' [CountableOrCountablyGenerated α β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
     (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η)
@@ -70,13 +72,13 @@ lemma singularPart_compProd' [MeasurableSpace.CountableOrCountablyGenerated α 
     rw [← Measure.compProd_add_right, (κ.rnDeriv_add_singularPart η)]
   rw [this]
 
-lemma singularPart_compProd_left [MeasurableSpace.CountableOrCountablyGenerated α β]
+lemma singularPart_compProd_left [CountableOrCountablyGenerated α β]
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ : Kernel α β) [IsFiniteKernel κ] :
     (μ ⊗ₘ κ).singularPart (ν ⊗ₘ κ) = μ.singularPart ν ⊗ₘ κ := by
   rw [singularPart_compProd', κ.singularPart_self, Measure.compProd_zero_right, add_zero]
 
-lemma singularPart_compProd_right [MeasurableSpace.CountableOrCountablyGenerated α β]
+lemma singularPart_compProd_right [CountableOrCountablyGenerated α β]
     (μ : Measure α) [IsFiniteMeasure μ]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
     (μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) = μ ⊗ₘ κ.singularPart η := by
@@ -107,7 +109,109 @@ theorem _root_.MeasureTheory.Integrable.integral_compProd' [NormedAddCommGroup E
     Integrable (fun x ↦ ∫ y, f (x, y) ∂(κ x)) μ :=
   hf.integral_compProd
 
-variable [MeasurableSpace.CountableOrCountablyGenerated α β]
+lemma integrable_f_rnDeriv_compProd_iff_of_nonneg' [IsFiniteMeasure ν]
+    [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_nonneg : ∀ x, 0 ≤ x → 0 ≤ f x) :
+    Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
+      ↔ (∀ᵐ a ∂ν, Integrable (fun x ↦ f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, x)).toReal) (η a))
+        ∧ Integrable (fun a ↦ ∫ b, f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, b)).toReal ∂(η a)) ν := by
+  have h_ae : AEStronglyMeasurable (fun x ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η) :=
+    (hf.comp_measurable (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable
+  refine ⟨fun h ↦ ?_, fun ⟨h1, h2⟩ ↦ ?_⟩
+  · have h_int := h.integral_compProd'
+    rw [Measure.integrable_compProd_iff h_ae] at h
+    exact ⟨h.1, h_int⟩
+  · rw [Measure.integrable_compProd_iff h_ae]
+    refine ⟨h1, ?_⟩
+    convert h2 using 4 with a b
+    rw [norm_of_nonneg]
+    exact h_nonneg _ ENNReal.toReal_nonneg
+
+lemma integrable_add_affine_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (f : ℝ → ℝ) (a b : ℝ) :
+    Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal + a * (μ.rnDeriv ν x).toReal + b) ν
+      ↔ Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν := by
+  have h_int : Integrable (fun x ↦ a * (μ.rnDeriv ν x).toReal + b) ν :=
+    (Measure.integrable_toReal_rnDeriv.const_mul _).add (integrable_const _)
+  simp_rw [add_assoc]
+  change Integrable ((fun x ↦ f ((∂μ/∂ν) x).toReal) + (fun x ↦ (a * ((∂μ/∂ν) x).toReal + b))) ν ↔ _
+  rwa [integrable_add_iff_integrable_left]
+
+lemma integrable_sub_affine_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (f : ℝ → ℝ) (a b : ℝ) :
+    Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal - (a * (μ.rnDeriv ν x).toReal + b)) ν
+      ↔ Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν := by
+  simp_rw [sub_eq_add_neg, neg_add, ← neg_mul, ← add_assoc]
+  rw [integrable_add_affine_iff f]
+
+lemma integrable_f_rnDeriv_compProd_iff' [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
+    (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
+    Integrable (fun x ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
+      ↔ (∀ᵐ a ∂ν, Integrable (fun x ↦ f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, x)).toReal) (η a))
+        ∧ Integrable (fun a ↦ ∫ b, f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, b)).toReal ∂(η a)) ν := by
+  obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, _ → c * x + c' ≤ f x := h_cvx.exists_affine_le (convex_Ici 0)
+  simp only [Set.mem_Ici] at h
+  rw [← integrable_sub_affine_iff f c c']
+  change Integrable (fun x ↦
+    (fun y ↦ f y - (c * y + c')) ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η) ↔ _
+  rw [integrable_f_rnDeriv_compProd_iff_of_nonneg' (f := fun y ↦ f y - (c * y + c'))]
+  rotate_left
+  · exact hf.sub ((stronglyMeasurable_id.const_mul c).add_const c')
+  · simpa using h
+  have h_int' : Integrable (fun p ↦ ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) p).toReal) (ν ⊗ₘ η) :=
+    Measure.integrable_toReal_rnDeriv
+  rw [Measure.integrable_compProd_iff] at h_int'
+  swap; · exact (Measure.measurable_rnDeriv _ _).ennreal_toReal.aestronglyMeasurable
+  have h_int''' : ∀ᵐ a ∂ν,
+      Integrable (fun x ↦ c * ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, x)).toReal + c') (η a) := by
+    filter_upwards [h_int'.1] with a h_int''
+    exact ((h_int''.const_mul _).add (integrable_const _))
+  -- The goal has shape `(P₁ ∧ Q₁) ↔ (P₂ ↔ Q₂)`. We prove first `P₁ ↔ P₂`.
+  have h_left : (∀ᵐ a ∂ν, Integrable (fun x ↦ f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, x)).toReal
+        - (c * (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, x)).toReal + c')) (η a))
+      ↔ ∀ᵐ a ∂ν, Integrable (fun x ↦ f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, x)).toReal) (η a) := by
+    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+    · filter_upwards [h, h_int'''] with a h h_int'''
+      change Integrable ((fun x ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, x)).toReal)
+        + (fun x ↦ -(c * ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, x)).toReal + c'))) (η a) at h
+      rwa [integrable_add_iff_integrable_left h_int'''.neg'] at h
+    · filter_upwards [h, h_int'''] with a h h_int'''
+      simp_rw [sub_eq_add_neg]
+      rwa [integrable_add_iff_integrable_left' h_int'''.neg']
+  rw [h_left, and_congr_right_iff]
+  -- Now we have proved `P₁ ↔ P₂` and it remains to prove `P₂ → (Q₁ ↔ Q₂)`.
+  intro h_int
+  have : ∀ᵐ a ∂ν, ∫ b, f (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, b)).toReal
+        - (c * (((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) (a, b)).toReal + c') ∂η a
+      = ∫ b, f ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (a, b)).toReal ∂η a
+        - ∫ b, c * ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (a, b)).toReal + c' ∂η a := by
+    filter_upwards [h_int, h_int'''] with a h_int h_int'''
+    rw [← integral_sub h_int h_int''']
+  rw [integrable_congr this]
+  simp_rw [sub_eq_add_neg]
+  rw [integrable_add_iff_integrable_left']
+  -- `⊢ Integrable (fun x ↦ -∫ (b : β), c * ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (x, b)).toReal + c' ∂η x) ν`
+  have h_int_compProd :
+      Integrable (fun x ↦ ∫ b, ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (x, b)).toReal ∂η x) ν := by
+    convert h_int'.2 with a b
+    rw [norm_of_nonneg ENNReal.toReal_nonneg]
+  have : ∀ᵐ x ∂ν, -∫ b, c * ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (x, b)).toReal + c' ∂η x
+      = -c * ∫ b, ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (x, b)).toReal ∂η x
+        - c' * (η x .univ).toReal := by
+    filter_upwards [h_int'.1] with x h_int'
+    rw [integral_add _ (integrable_const _)]
+    swap; · exact h_int'.const_mul _
+    simp only [integral_const, smul_eq_mul, neg_add_rev, neg_mul]
+    rw [add_comm, mul_comm]
+    congr 1
+    rw [mul_comm c, ← smul_eq_mul, ← integral_smul_const]
+    simp_rw [smul_eq_mul, mul_comm _ c]
+  rw [integrable_congr this]
+  refine Integrable.sub (h_int_compProd.const_mul _) (Integrable.const_mul ?_ _)
+  simp_rw [← integral_indicator_one MeasurableSet.univ]
+  simp only [Set.mem_univ, Set.indicator_of_mem, Pi.one_apply]
+  exact Integrable.integral_compProd' (f := fun _ ↦ 1) (integrable_const _)
+
+variable [CountableOrCountablyGenerated α β]
 
 lemma f_compProd_congr (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
@@ -164,31 +268,16 @@ lemma integrable_f_rnDeriv_compProd_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν
         ∧ Integrable (fun a ↦ ∫ b, f ((∂μ/∂ν) a * (∂κ a/∂η a) b).toReal ∂(η a)) ν := by
   have h_ae_eq : ∀ᵐ a ∂ν, (fun y ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, y)).toReal)
       =ᵐ[η a] fun x ↦ f ((∂μ/∂ν) a * (∂κ a/∂η a) x).toReal := f_compProd_congr μ ν κ η
-  refine ⟨fun h ↦ ?_, fun ⟨h1, h2⟩ ↦ ?_⟩
-  · have h_int := h.integral_compProd'
-    rw [Measure.integrable_compProd_iff] at h
-    swap
-    · exact (hf.comp_measurable
-        (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable
-    constructor
-    · filter_upwards [h.1, h_ae_eq] with a ha1 ha2
-      exact (integrable_congr ha2).mp ha1
-    · refine (integrable_congr ?_).mp h_int
-      filter_upwards [h_ae_eq] with a ha
-      exact integral_congr_ae ha
-  · rw [Measure.integrable_compProd_iff]
-    swap
-    · exact (hf.comp_measurable
-        (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable
-    constructor
-    · filter_upwards [h1, h_ae_eq] with a ha1 ha2
-      exact (integrable_congr ha2).mpr ha1
-    · rw [← integrable_congr (integral_f_compProd_congr μ ν κ η)] at h2
-      -- todo: cut into two parts, depending on sign of f.
-      -- on the positive part, use h2.
-      -- on the negative part, use `f x ≥ a * x + b` by convexity, then since both measures are
-      -- finite the integral is finite.
-      sorry
+  rw [integrable_f_rnDeriv_compProd_iff' hf h_cvx]
+  congr! 1
+  · refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+    · filter_upwards [h_ae_eq, h] with a ha h
+      rwa [integrable_congr ha.symm]
+    · filter_upwards [h_ae_eq, h] with a ha h
+      rwa [integrable_congr ha]
+  · refine integrable_congr ?_
+    filter_upwards [h_ae_eq] with a ha
+    exact integral_congr_ae ha
 
 lemma integrable_f_rnDeriv_compProd_right_iff [IsFiniteMeasure μ]
     [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)

TestingLowerBounds/Convex.lean

@@ -3,9 +3,8 @@ 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, Lorenzo Luccioli
 -/
-import TestingLowerBounds.ForMathlib.EReal
-import Mathlib.Analysis.Convex.Integral
-import Mathlib.Analysis.Calculus.MeanValue
+import Mathlib.Analysis.InnerProductSpace.Basic
+import TestingLowerBounds.ForMathlib.LeftRightDeriv
 
 /-!
 
@@ -33,29 +32,52 @@ variable {f g : ℝ → ℝ} {s : Set ℝ} {x : ℝ}
 
 namespace ConvexOn
 
+lemma affine_le_of_mem_interior (hf : ConvexOn ℝ s f) {x y : ℝ} (hx : x ∈ interior s) (hy : y ∈ s) :
+    rightDeriv f x * y + (f x - rightDeriv f x * x) ≤ f y := by
+  rw [add_comm]
+  rcases lt_trichotomy x y with hxy | h_eq | hyx
+  · have : rightDeriv f x ≤ slope f x y := rightDeriv_le_slope hf hx hy hxy
+    rw [slope_def_field] at this
+    rwa [le_div_iff₀ (by simp [hxy]), le_sub_iff_add_le, add_comm, mul_sub, add_sub,
+      add_sub_right_comm] at this
+  · simp [h_eq]
+  · have : slope f x y ≤ rightDeriv f x :=
+      (slope_le_leftDeriv hf hx hy hyx).trans (leftDeriv_le_rightDeriv_of_mem_interior hf hx)
+    rw [slope_def_field] at this
+    rw [← neg_div_neg_eq, neg_sub, neg_sub] at this
+    rwa [div_le_iff₀ (by simp [hyx]), sub_le_iff_le_add, mul_sub, ← sub_le_iff_le_add',
+      sub_sub_eq_add_sub, add_sub_right_comm] at this
+
+lemma _root_.Convex.subsingleton_of_interior_eq_empty (hs : Convex ℝ s) (h : interior s = ∅) :
+    s.Subsingleton := by
+  intro x hx y hy
+  by_contra h_ne
+  wlog h_lt : x < y
+  · refine this hs h hy hx (Ne.symm h_ne) ?_
+    exact lt_of_le_of_ne (not_lt.mp h_lt) (Ne.symm h_ne)
+  · have h_subset : Set.Icc x y ⊆ s := by
+      rw [← segment_eq_Icc h_lt.le]
+      exact hs.segment_subset hx hy
+    have : Set.Ioo x y ⊆ interior s := by
+      rw [← interior_Icc]
+      exact interior_mono h_subset
+    simp only [h, Set.subset_empty_iff, Set.Ioo_eq_empty_iff] at this
+    exact this h_lt
+
 lemma exists_affine_le (hf : ConvexOn ℝ s f) (hs : Convex ℝ s) :
     ∃ c c', ∀ x ∈ s, c * x + c' ≤ f x := by
-  sorry
-
-lemma comp_neg {𝕜 F β : Type*} [LinearOrderedField 𝕜] [AddCommGroup F]
-    [OrderedAddCommMonoid β] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} {s : Set F}
-    (hf : ConvexOn 𝕜 s f) :
-    ConvexOn 𝕜 (-s) (fun x ↦ f (-x)) := by
-  refine ⟨hf.1.neg, fun x hx y hy a b ha hb hab ↦ ?_⟩
-  simp_rw [neg_add_rev, ← smul_neg, add_comm]
-  exact hf.2 hx hy ha hb hab
-
-lemma comp_neg_iff {𝕜 F β : Type*} [LinearOrderedField 𝕜] [AddCommGroup F]
-    [OrderedAddCommMonoid β] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} {s : Set F}  :
-    ConvexOn 𝕜 (-s) (fun x ↦ f (-x)) ↔ ConvexOn 𝕜 s f := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ConvexOn.comp_neg h⟩
-  rw [← neg_neg s, ← Function.comp_id f, ← neg_comp_neg, ← Function.comp.assoc]
-  exact h.comp_neg
-
---this can be stated in much greater generality
-lemma const_mul_id (c : ℝ) : ConvexOn ℝ .univ (fun (x : ℝ) ↦ c * x) := by
-  refine ⟨convex_univ, fun _ _ _ _ _ _ _ _ _ ↦ Eq.le ?_⟩
-  simp only [smul_eq_mul]
-  ring
+  cases Set.eq_empty_or_nonempty (interior s) with
+  | inl h => -- there is at most one point in `s`
+    have hs_sub : s.Subsingleton := hs.subsingleton_of_interior_eq_empty h
+    cases Set.eq_empty_or_nonempty s with
+    | inl h' => simp [h']
+    | inr h' => -- there is exactly one point in `s`
+      obtain ⟨x, hxs⟩ := h'
+      refine ⟨0, f x, fun y hys ↦ ?_⟩
+      simp [hs_sub hxs hys]
+  | inr h => -- there is a point in the interior of `s`
+    obtain ⟨x, hx⟩ := h
+    refine ⟨rightDeriv f x, f x - rightDeriv f x * x, fun y hy ↦ ?_⟩
+    exact affine_le_of_mem_interior hf hx hy
 
 end ConvexOn

TestingLowerBounds/DerivAtTop.lean

@@ -3,6 +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 TestingLowerBounds.ForMathlib.EReal
 import TestingLowerBounds.ForMathlib.LeftRightDeriv
 
 /-!