MulExpNegMulSqIntegral

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

Statistics

Metric	Count
Definitions	0
Theorems abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure, dist_integral_mulExpNegMulSq_comp_le, integrable_mulExpNegMulSq_comp, integrable_mulExpNegMulSq_comp_restrict_of_isCompact, integral_mulExpNegMulSq_comp_eq, tendsto_integral_mulExpNegMulSq_comp, tendsto_integral_mul_one_add_inv_smul_sq_pow	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt 📖	mathematical	MeasurableSet Real Real.instLT Real.instZero ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Compl.compl Set.instCompl ENNReal.ofNNReal Real.toNNReal	abs Real.lattice Real.instAddGroup Real.instSub MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.mulExpNegMulSq ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike MeasureTheory.Measure.restrict Real.sqrt	—	lt_of_le_of_lt MeasureTheory.norm_integral_sub_setIntegral_le Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass Real.abs_mulExpNegMulSq_le integrable_mulExpNegMulSq_comp mul_inv_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Real.sqrt_pos_of_pos Real.mul_self_sqrt le_of_lt ENNReal.toReal_lt_of_lt_ofReal
abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure 📖	mathematical	IsCompact MeasurableSet Real Real.instLT Real.instZero abs Real.lattice Real.instAddGroup Real.instSub DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike	Real.instLE MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Real.mulExpNegMulSq Real.instMul ENNReal.toReal MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike	—	MeasureTheory.integral_sub integrable_mulExpNegMulSq_comp_restrict_of_isCompact Real.norm_eq_abs MeasureTheory.norm_setIntegral_le_of_norm_le_const IsCompact.measure_lt_top isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure le_trans Real.dist_mulExpNegMulSq_le_dist LT.lt.le
dist_integral_mulExpNegMulSq_comp_le 📖	mathematical	Subalgebra.SeparatesPoints UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Real Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedCommRing.toNormedRing Real.normedCommRing Ring.toSemiring NormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.instRCLike IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Subalgebra.map BoundedContinuousFunction ContinuousMap BoundedContinuousFunction.instSemiring instBoundedMul IsTopologicalSemiring.toContinuousMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instBoundedAddOfLipschitzAdd ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedAddCommGroup.to_lipschitzAdd NonUnitalSeminormedRing.toSeminormedAddCommGroup IsTopologicalSemiring.toContinuousAdd BoundedContinuousFunction.instAlgebra ContinuousMap.instSemiringOfIsTopologicalSemiring ContinuousMap.algebra BoundedContinuousFunction.toContinuousMapₐ MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace RCLike.toInnerProductSpaceReal DFunLike.coe Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike Real.instLT Real.instZero	Real.instLE abs Real.lattice Real.instAddGroup Real.instSub Real.mulExpNegMulSq Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.sqrt	—	instBoundedMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instBoundedAddOfLipschitzAdd Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd NonUnitalSeminormedRing.toIsTopologicalRing SeminormedAddCommGroup.to_lipschitzAdd Nat.instAtLeastTwoHAddOfNat MeasureTheory.integral_zero_measure sub_self abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial le_of_lt Real.sqrt_pos_of_pos not_and_or lt_max_of_lt_left ENNReal.toReal_pos MeasureTheory.Measure.measure_univ_ne_zero MeasureTheory.measure_ne_top lt_max_of_lt_right MeasurableSet.exists_isCompact_isClosed_diff_lt instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace TopologicalSpace.IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable EMetric.instIsCountablyGeneratedUniformity MeasurableSet.univ LT.lt.ne' ENNReal.ofReal_pos IsCompact.union IsClosed.union lt_of_le_of_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.compl_subset_compl_of_subset Set.subset_union_left Set.subset_union_right BoundedContinuousMapClass.toContinuousMapClass BoundedContinuousFunction.instBoundedContinuousMapClass ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints Left.mul_pos inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE BoundedContinuousFunction.coe_toContinuousMapₐ abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt IsClosed.measurableSet BorelSpace.opensMeasurable abs_sub_comm le_trans abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure mul_assoc mul_le_of_le_one_right IsOrderedRing.toPosMulMono inv_mul_le_one_of_le₀ Real.instZeroLEOneClass le_max_of_le_left ENNReal.toReal_le_toReal Set.subset_univ le_max_of_le_right abs_eq_zero covariant_swap_add_of_covariant_add sub_eq_zero integral_mulExpNegMulSq_comp_eq dist_triangle8 le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo 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.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le sub_eq_zero_of_eq
integrable_mulExpNegMulSq_comp 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.mulExpNegMulSq DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	BoundedContinuousFunction.integrable BorelSpace.opensMeasurable instSecondCountableTopologyReal Real.borelSpace Continuous.mulExpNegMulSq ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass Nat.instAtLeastTwoHAddOfNat Real.dist_mulExpNegMulSq_le_two_mul_sqrt
integrable_mulExpNegMulSq_comp_restrict_of_isCompact 📖	mathematical	IsCompact MeasurableSet	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.mulExpNegMulSq DFunLike.coe ContinuousMap ContinuousMap.instFunLike MeasureTheory.Measure.restrict	—	ContinuousOn.integrableOn_compact' BorelSpace.opensMeasurable isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure Continuous.continuousOn Continuous.mulExpNegMulSq ContinuousMap.continuous
integral_mulExpNegMulSq_comp_eq 📖	mathematical	Real Real.instLT Real.instZero MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike Subalgebra Real.instCommSemiring BoundedContinuousFunction.instSemiring Real.semiring instBoundedMul NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing IsTopologicalSemiring.toContinuousMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal instBoundedAddOfLipschitzAdd Real.instAddMonoid Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd BoundedContinuousFunction.instAlgebra Real.normedField NormedCommRing.toNormedRing RCLike.toNormedAlgebra SetLike.instMembership Subalgebra.instSetLike	Real.mulExpNegMulSq	—	instBoundedMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instBoundedAddOfLipschitzAdd Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd Real.isBoundedSMul Subalgebra.mul_mem Subalgebra.pow_mem Subalgebra.add_mem Subalgebra.one_mem Subalgebra.smul_mem Subalgebra.neg_mem tendsto_integral_mul_one_add_inv_smul_sq_pow tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
tendsto_integral_mulExpNegMulSq_comp 📖	mathematical	—	Filter.Tendsto Real MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.mulExpNegMulSq DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.instZero Set.Ioi Real.instPreorder nhds	—	Filter.tendsto_of_seq_tendsto TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_nhdsWithin_iff MeasureTheory.tendsto_integral_filter_of_norm_le_const instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat Filter.Eventually.of_forall Continuous.aestronglyMeasurable BorelSpace.opensMeasurable secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.mulExpNegMulSq BoundedContinuousFunction.continuous MeasureTheory.Measure.instOuterMeasureClass Real.abs_mulExpNegMulSq_comp_le_norm le_of_lt Set.mem_Ioi Filter.Tendsto.comp tendsto_nhdsWithin_of_tendsto_nhds Real.tendsto_mulExpNegMulSq
tendsto_integral_mul_one_add_inv_smul_sq_pow 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike BoundedContinuousFunction.instMul Real.instMul instBoundedMul NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing IsTopologicalSemiring.toContinuousMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal BoundedContinuousFunction.hasNatPow SeminormedCommRing.toSeminormedRing BoundedContinuousFunction.instAdd Real.instAdd instBoundedAddOfLipschitzAdd Real.instAddMonoid Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd BoundedContinuousFunction.instOne Real.instOne BoundedContinuousFunction.instSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.isBoundedSMul Real.instInv Real.instNatCast BoundedContinuousFunction.instNeg NonUnitalSeminormedRing.toSeminormedAddCommGroup Filter.atTop Nat.instPreorder nhds Real.mulExpNegMulSq	—	MeasureTheory.tendsto_integral_filter_of_norm_le_const instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace instBoundedMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instBoundedAddOfLipschitzAdd Real.hasLipschitzAdd IsTopologicalSemiring.toContinuousAdd Real.isBoundedSMul Filter.Eventually.of_forall MeasureTheory.StronglyMeasurable.aestronglyMeasurable Continuous.stronglyMeasurable BorelSpace.opensMeasurable secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.mul BoundedContinuousFunction.continuous MeasureTheory.Measure.instOuterMeasureClass exists_nat_gt Real.instIsStrictOrderedRing Real.instArchimedean Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat lt_of_lt_of_le lt_of_le_of_lt mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt mul_self_nonneg AddGroup.existsAddOfLE IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_le Real.instZeroLEOneClass RCLike.charZero_rclike smul_neg norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass LE.le.trans mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono BoundedContinuousFunction.norm_coe_le_norm pow_nonneg abs_nonneg covariant_swap_add_of_covariant_add mul_le_of_le_one_right norm_nonneg pow_le_one₀ mul_assoc inv_mul_eq_div abs_le le_trans le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt sub_nonneg_of_le div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_le_mul le_refl abs_le_iff_mul_self_le abs_norm add_le_iff_nonpos_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Left.neg_nonpos_iff div_nonneg Filter.Tendsto.const_mul NonUnitalSeminormedRing.toIsTopologicalRing SeminormedAddCommGroup.to_lipschitzAdd Algebra.smul_mul_assoc Real.tendsto_one_add_div_pow_exp

---

← Back to Index