cleanup

LorenzoLuccioli · Sep 18, 2024 · 541c58d · 541c58d
1 parent 761e076
commit 541c58d
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/TestingLowerBounds/Divergences/fDivStatInfo.lean b/TestingLowerBounds/Divergences/fDivStatInfo.lean
@@ -340,7 +340,6 @@ lemma fDiv_ne_top_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous
     rw [rightDeriv_add_const_apply, rightDeriv_add_linear_apply, rightDeriv_add_const_apply hf_diff,
       add_neg_cancel] <;> fun_prop
 
-
 lemma integrable_f_rnDeriv_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous
     [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf_cvx : ConvexOn ℝ univ f) (hf_cont : Continuous f) (h_ac : μ ≪ ν) :