MulExpNegMulSq

📁 Source: Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean

Statistics

Metric	Count
Definitions mulExpNegMulSq	1
Theorems mulExpNegMulSq, abs_mulExpNegMulSq_comp_le_norm, abs_mulExpNegMulSq_le, abs_mulExpNegMulSq_one_le_one, continuous_mulExpNegMulSq, deriv_mulExpNegMulSq, differentiableAt_mulExpNegMulSq, differentiable_mulExpNegMulSq, dist_mulExpNegMulSq_le_dist, dist_mulExpNegMulSq_le_two_mul_sqrt, hasDerivAt_mulExpNegMulSq, lipschitzWith_one_mulExpNegMulSq, mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one, mulExpNegMulSq_one_le_one, mulExpNegSq_apply, neg_mulExpNegMulSq_neg, neg_one_le_mulExpNegMulSq_one, nnnorm_deriv_mulExpNegMulSq_le_one, norm_deriv_mulExpNegMulSq_le_one, tendsto_mulExpNegMulSq	20
Total	21

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulExpNegMulSq 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.mulExpNegMulSq	—	comp Real.continuous_mulExpNegMulSq

Real

Definitions

Name	Category	Theorems
mulExpNegMulSq 📖	CompOp	28 math math: differentiableAt_mulExpNegMulSq, nnnorm_deriv_mulExpNegMulSq_le_one, dist_mulExpNegMulSq_le_two_mul_sqrt, mulExpNegSq_apply, abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure, norm_deriv_mulExpNegMulSq_le_one, abs_mulExpNegMulSq_comp_le_norm, dist_integral_mulExpNegMulSq_comp_le, deriv_mulExpNegMulSq, tendsto_integral_mul_one_add_inv_smul_sq_pow, tendsto_integral_mulExpNegMulSq_comp, Continuous.mulExpNegMulSq, lipschitzWith_one_mulExpNegMulSq, mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one, abs_mulExpNegMulSq_one_le_one, hasDerivAt_mulExpNegMulSq, differentiable_mulExpNegMulSq, neg_mulExpNegMulSq_neg, integral_mulExpNegMulSq_comp_eq, neg_one_le_mulExpNegMulSq_one, abs_mulExpNegMulSq_le, mulExpNegMulSq_one_le_one, integrable_mulExpNegMulSq_comp_restrict_of_isCompact, integrable_mulExpNegMulSq_comp, abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, dist_mulExpNegMulSq_le_dist, continuous_mulExpNegMulSq, tendsto_mulExpNegMulSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_mulExpNegMulSq_comp_le_norm 📖	mathematical	Real instLE instZero	Real instLE abs lattice instAddGroup mulExpNegMulSq DFunLike.coe BoundedContinuousFunction pseudoMetricSpace BoundedContinuousFunction.instFunLike Norm.norm BoundedContinuousFunction.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing	—	abs_mul instIsOrderedRing abs_exp le_trans mul_le_of_le_one_right IsOrderedRing.toPosMulMono abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add exp_le_one_iff Left.neg_nonpos_iff mul_assoc mul_nonneg mul_self_nonneg AddGroup.existsAddOfLE BoundedContinuousFunction.norm_coe_le_norm
abs_mulExpNegMulSq_le 📖	mathematical	Real instLT instZero	Real instLE abs lattice instAddGroup mulExpNegMulSq instInv sqrt	—	mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one abs_mul instIsOrderedRing abs_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing sqrt_pos_of_pos mul_le_of_le_one_right IsOrderedRing.toPosMulMono le_of_lt abs_mulExpNegMulSq_one_le_one
abs_mulExpNegMulSq_one_le_one 📖	mathematical	—	Real instLE abs lattice instAddGroup mulExpNegMulSq instOne	—	abs_le instIsOrderedAddMonoid neg_one_le_mulExpNegMulSq_one mulExpNegMulSq_one_le_one
continuous_mulExpNegMulSq 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace mulExpNegMulSq	—	Continuous.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id Continuous.rexp Continuous.neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing Continuous.comp' continuous_mul Continuous.prodMk continuous_const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring continuous_id'
deriv_mulExpNegMulSq 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace mulExpNegMulSq instAdd exp instNeg instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	HasDerivAt.deriv Nat.instAtLeastTwoHAddOfNat hasDerivAt_mulExpNegMulSq
differentiableAt_mulExpNegMulSq 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace mulExpNegMulSq	—	DifferentiableAt.mul differentiableAt_fun_id DifferentiableAt.exp DifferentiableAt.fun_neg DifferentiableAt.fun_mul DifferentiableAt.const_mul differentiableAt_id
differentiable_mulExpNegMulSq 📖	mathematical	—	Differentiable Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace mulExpNegMulSq	—	differentiableAt_mulExpNegMulSq
dist_mulExpNegMulSq_le_dist 📖	mathematical	Real instLT instZero	Real instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace mulExpNegMulSq	—	lipschitzWith_one_mulExpNegMulSq ENNReal.toReal_le_toReal edist_ne_top one_mul ENNReal.coe_one
dist_mulExpNegMulSq_le_two_mul_sqrt 📖	mathematical	Real instLT instZero	Real instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace mulExpNegMulSq instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instInv sqrt	—	le_trans Nat.instAtLeastTwoHAddOfNat dist_triangle dist_zero_right dist_zero_left two_mul add_le_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add abs_mulExpNegMulSq_le
hasDerivAt_mulExpNegMulSq 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal mulExpNegMulSq instAdd exp instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat one_mul HasDerivAt.mul hasDerivAt_id' HasDerivAt.exp HasDerivAt.congr_deriv HasDerivAt.neg HasDerivAt.const_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one
lipschitzWith_one_mulExpNegMulSq 📖	mathematical	Real instLT instZero	LipschitzWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace metricSpace NNReal NNReal.instOne mulExpNegMulSq	—	lipschitzWith_of_nnnorm_deriv_le differentiable_mulExpNegMulSq nnnorm_deriv_mulExpNegMulSq_le_one
mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one 📖	mathematical	Real instLT instZero	mulExpNegMulSq Real instMul instInv sqrt instOne	—	—
mulExpNegMulSq_one_le_one 📖	mathematical	—	Real instLE mulExpNegMulSq instOne	—	one_mul le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing exp_pos exp_neg div_inv_eq_mul le_trans le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing mul_self_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike mul_nonneg_of_nonpos_of_nonpos IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Mathlib.Tactic.Linarith.mul_nonpos le_of_lt mul_pos_of_neg_of_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono add_one_le_exp
mulExpNegSq_apply 📖	mathematical	—	mulExpNegMulSq Real instMul exp instNeg	—	—
neg_mulExpNegMulSq_neg 📖	mathematical	—	Real instNeg mulExpNegMulSq	—	mul_neg neg_mul neg_neg
neg_one_le_mulExpNegMulSq_one 📖	mathematical	—	Real instLE instNeg instOne mulExpNegMulSq	—	neg_mulExpNegMulSq_neg neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mulExpNegMulSq_one_le_one
nnnorm_deriv_mulExpNegMulSq_le_one 📖	mathematical	Real instLT instZero	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm Real SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace mulExpNegMulSq NNReal.instOne	—	NNReal.coe_le_coe coe_nnnorm norm_deriv_mulExpNegMulSq_le_one
norm_deriv_mulExpNegMulSq_le_one 📖	mathematical	Real instLT instZero	Real instLE Norm.norm norm deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace mulExpNegMulSq instOne	—	norm_eq_abs Nat.instAtLeastTwoHAddOfNat deriv_mulExpNegMulSq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul abs_mul instIsOrderedRing abs_exp mul_assoc mul_nonneg IsOrderedRing.toPosMulMono LT.lt.le mul_self_nonneg AddGroup.existsAddOfLE IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_le_of_le_inv_mul₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing zero_le_one' instZeroLEOneClass exp_nonneg exp_neg neg_neg mul_one AddGroup.toOrderedSub covariant_swap_add_of_covariant_add le_trans two_mul_le_exp le_add_iff_nonneg_left IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le zero_le_one one_le_exp le_add_of_nonneg_right instNontrivial
tendsto_mulExpNegMulSq 📖	mathematical	—	Filter.Tendsto Real mulExpNegMulSq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero	—	MulZeroClass.zero_mul neg_zero exp_zero mul_one Continuous.tendsto Continuous.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_const Continuous.rexp Continuous.neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing Continuous.comp' continuous_mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring

---

← Back to Index