fix bugs

consequencies of the stricter hp of `ConvexOn.nonneg_of_todo`
RemyDegenne · Nov 13, 2024 · 40801ff · 40801ff
1 parent de07d7b
commit 40801ff
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/TestingLowerBounds/Divergences/Hellinger/HellingerFun.lean b/TestingLowerBounds/Divergences/Hellinger/HellingerFun.lean
@@ -359,6 +359,7 @@ lemma rightDeriv_hellingerFun_one :
   simp [rightDeriv_hellingerFun]
 
 lemma hellingerFun_nonneg (ha : 0 ≤ a) {x : ℝ} (hx : 0 ≤ x) : 0 ≤ hellingerFun a x := by
+  rcases hx.eq_or_lt with rfl | hx; · simp
   refine ConvexOn.nonneg_of_todo ?_ hellingerFun_apply_one_eq_zero rightDeriv_hellingerFun_one hx
   exact (convexOn_hellingerFun ha).subset (Set.Ioi_subset_Ici le_rfl) (convex_Ioi _)
 

diff --git a/TestingLowerBounds/Divergences/KullbackLeibler/KLDivFun.lean b/TestingLowerBounds/Divergences/KullbackLeibler/KLDivFun.lean
@@ -91,6 +91,7 @@ lemma rightDeriv_mul_log_add_one_sub_eventually_eq :
   rw [rightDeriv_mul_log_add_one_sub hx]
 
 lemma mul_log_add_one_sub_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ x * log x + 1 - x := by
+  rcases hx.eq_or_lt with rfl | hx; · simp
   refine ConvexOn.nonneg_of_todo (f := fun x ↦ x * log x + 1 - x) ?_ ?_ ?_ hx
   · exact convexOn_mul_log_add_one_sub.subset (Ioi_subset_Ici le_rfl) (convex_Ioi _)
   · simp