Commit 2025-02-10 14:34 c38165c0

View on Github →

feat: basic properties of MulExpNegMulSq (#20604) Define MulExpNegMulSq and show basic properties. The function is an important tool in the proof of separation of finite measures by subalgebras of functions

Estimated changes

Modified Mathlib.lean

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

added theorem Real.exp_one_mul_le_exp

added theorem Real.two_mul_le_exp

Created Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean

added theorem Continuous.mulExpNegMulSq

added theorem Real.abs_mulExpNegMulSq_comp_le_norm

added theorem Real.abs_mulExpNegMulSq_le

added theorem Real.abs_mulExpNegMulSq_one_le_one

added theorem Real.continuous_mulExpNegMulSq

added theorem Real.deriv_mulExpNegMulSq

added theorem Real.differentiableAt_mulExpNegMulSq

added theorem Real.differentiable_mulExpNegMulSq

added theorem Real.dist_mulExpNegMulSq_le_dist

added theorem Real.dist_mulExpNegMulSq_le_two_mul_sqrt

added theorem Real.hasDerivAt_mulExpNegMulSq

added theorem Real.lipschitzWith_one_mulExpNegMulSq

added def Real.mulExpNegMulSq

added theorem Real.mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one

added theorem Real.mulExpNegMulSq_one_le_one

added theorem Real.mulExpNegSq_apply

added theorem Real.neg_mulExpNegMulSq_neg

added theorem Real.neg_one_le_mulExpNegMulSq_one

added theorem Real.nnnorm_deriv_mulExpNegMulSq_le_one

added theorem Real.norm_deriv_mulExpNegMulSq_le_one

added theorem Real.tendsto_mulExpNegMulSq