Commit 2023-07-18 03:34 2db59610

View on Github →

feat: positivity extension for Real.log of natural/integer casts and numeric literals (#5839) This PR adds a positivity extension for expressions of the form Real.log n where n is a cast from a natural number or an integer. (Since positivity can't handle conditions like 1 ≤ x, this is pretty much the best we can do for the log.) Also, the namespace of the positivity extension for exp is corrected.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

added def Mathlib.Meta.Positivity.evalLogIntCast

added def Mathlib.Meta.Positivity.evalLogNatCast

added def Mathlib.Meta.Positivity.evalLogNatLit

added theorem Mathlib.Meta.Positivity.log_nonneg_of_isNat

added theorem Mathlib.Meta.Positivity.log_nonneg_of_isNegNat

added theorem Mathlib.Meta.Positivity.log_nz_of_isRat

added theorem Mathlib.Meta.Positivity.log_nz_of_isRat_neg

added theorem Mathlib.Meta.Positivity.log_pos_of_isNat

added theorem Mathlib.Meta.Positivity.log_pos_of_isNegNat

added theorem Mathlib.Meta.Positivity.log_pos_of_isRat

added theorem Mathlib.Meta.Positivity.log_pos_of_isRat_neg

added theorem Real.log_int_cast_nonneg

added theorem Real.log_nat_cast_nonneg

added theorem Real.log_neg_nat_cast_nonneg

added theorem Real.log_neg_of_lt_zero

added theorem Real.log_pos_of_lt_neg_one

Modified Mathlib/Data/Complex/Exponential.lean

added def Mathlib.Meta.Positivity.evalExp

deleted def Tactic.evalExp

Modified test/positivity.lean