diff --git a/TestingLowerBounds/KullbackLeibler.lean b/TestingLowerBounds/KullbackLeibler.lean index d3954af9..5cc744d8 100644 --- a/TestingLowerBounds/KullbackLeibler.lean +++ b/TestingLowerBounds/KullbackLeibler.lean @@ -157,8 +157,6 @@ end kl_nonneg section Conditional variable {β : Type*} {mβ : MeasurableSpace β} --- variable {κ η : kernel α β} - open Classical in