PeakFunction

📁 Source: Mathlib/MeasureTheory/Integral/PeakFunction.lean

Statistics

Metric	Count
Definitions	0
Theorems integrableOn_peak_smul_of_integrableOn_of_tendsto, tendsto_integral_comp_smul_smul_of_integrable, tendsto_integral_comp_smul_smul_of_integrable', tendsto_integral_peak_smul_of_integrable_of_tendsto, tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto, tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrableOn_peak_smul_of_integrableOn_of_tendsto 📖	mathematical	MeasurableSet Set Filter Filter.instMembership nhdsWithin TendstoUniformlyOn Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.instZero Real.instZero Set.instSDiff Filter.Tendsto MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict nhds UniformSpace.toTopologicalSpace Real.instOne Filter.Eventually MeasureTheory.AEStronglyMeasurable MeasureTheory.IntegrableOn SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	mem_nhdsWithin Filter.inter_mem Metric.ball_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.inter_comm HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.inter_subset_right Filter.mp_mem tendsto_order instOrderTopologyReal tendsto_iff_norm_sub_tendsto_zero Metric.tendstoUniformlyOn_iff Filter.univ_mem' MeasureTheory.Integrable.of_integral_ne_zero zero_sub norm_neg CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass MeasureTheory.Integrable.smul_of_top_right NormedSpace.toIsBoundedSMul MeasureTheory.IntegrableOn.mono Set.diff_subset le_rfl MeasureTheory.memLp_top_of_bound MeasureTheory.AEStronglyMeasurable.mono_set MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.self_mem_ae_restrict MeasurableSet.diff IsOpen.measurableSet BorelSpace.opensMeasurable dist_zero_left LT.lt.le MeasureTheory.Integrable.smul_of_top_left MeasureTheory.IntegrableOn.mono_set MeasureTheory.Integrable.aestronglyMeasurable MeasurableSet.inter norm_lt_of_mem_ball Set.diff_union_inter MeasureTheory.IntegrableOn.union PseudoEMetricSpace.pseudoMetrizableSpace
tendsto_integral_comp_smul_smul_of_integrable 📖	mathematical	Real Real.instLE Real.instZero MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instOne Filter.Tendsto Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Bornology.cobounded PseudoMetricSpace.toBornology nhds Real.pseudoMetricSpace MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Filter.atTop Real.instPreorder	—	MeasureTheory.integrable_of_integral_eq_one tendsto_integral_peak_smul_of_integrable_of_tendsto IsClosed.measurableSet BorelSpace.opensMeasurable Metric.isClosed_closedBall Metric.closedBall_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsCompact.measure_ne_top MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts ProperSpace.isCompact_closedBall FiniteDimensional.proper_real Filter.mp_mem Filter.Ici_mem_atTop Filter.univ_mem' mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass Metric.tendstoUniformlyOn_iff Metric.isOpen_iff Filter.HasBasis.eventually_iff Metric.hasBasis_cobounded_compl_closedBall tendsto_order instOrderTopologyReal mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toZeroLEOneClass LT.lt.trans_le le_max_right dist_zero_right Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial lt_trans div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono pow_le_pow_left₀ le_of_lt norm_smul NormedSpace.toNormSMulClass abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul abs_of_nonneg LT.lt.le div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_le_mul_of_nonneg_left mul_lt_mul_iff_of_pos_left dist_zero norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass MeasureTheory.AECover.integral_tendsto_of_countably_generated instIsCountablyGenerated_atTop TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal MeasureTheory.aecover_closedBall Filter.tendsto_id Filter.Tendsto.congr' MeasureTheory.integral_const_mul MeasureTheory.Measure.setIntegral_comp_smul_of_pos smul_eq_mul mul_assoc mul_inv_cancel₀ ne_of_gt smul_closedBall zero_le_one smul_zero mul_one one_mul MeasureTheory.AEStronglyMeasurable.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Integrable.aestronglyMeasurable MeasureTheory.Integrable.comp_smul LT.lt.ne'
tendsto_integral_comp_smul_smul_of_integrable' 📖	mathematical	Real Real.instLE Real.instZero MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instOne Filter.Tendsto Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Bornology.cobounded PseudoMetricSpace.toBornology nhds Real.pseudoMetricSpace MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAt	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Filter.atTop Real.instPreorder	—	sub_eq_add_neg MeasureTheory.Integrable.comp_neg ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular locallyCompact_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite PseudoEMetricSpace.pseudoMetrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instWeaklyLocallyCompactSpaceOfLocallyCompactSpace MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite MeasureTheory.Integrable.comp_add_left ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant tendsto_integral_comp_smul_smul_of_integrable sub_zero ContinuousAt.comp ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub continuousAt_const continuousAt_id' MeasureTheory.integral_add_left_eq_self MeasureTheory.integral_neg_eq_self smul_add smul_neg neg_add_rev neg_neg add_neg_cancel_comm_assoc
tendsto_integral_peak_smul_of_integrable_of_tendsto 📖	mathematical	MeasurableSet Set Filter Filter.instMembership nhds Filter.Eventually TendstoUniformlyOn Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.instZero Real.instZero Compl.compl Set.instCompl Filter.Tendsto MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict UniformSpace.toTopologicalSpace Real.instOne MeasureTheory.AEStronglyMeasurable MeasureTheory.Integrable SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto MeasurableSet.univ Set.subset_univ nhdsWithin_univ MeasureTheory.Measure.restrict_univ
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto 📖	mathematical	MeasurableSet Set Set.instHasSubset Filter Filter.instMembership nhdsWithin Filter.Eventually TendstoUniformlyOn Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.instZero Real.instZero Set.instSDiff Filter.Tendsto MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict nhds UniformSpace.toTopologicalSpace Real.instOne MeasureTheory.AEStronglyMeasurable MeasureTheory.IntegrableOn SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux MeasureTheory.Integrable.sub MeasureTheory.integrable_indicator_iff MeasureTheory.integrableOn_const_iff enorm_ne_top MeasureTheory.Measure.restrict_apply lt_of_le_of_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_left Ne.lt_top sub_self Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub Filter.Tendsto.congr' tendsto_const_nhds Filter.mp_mem Filter.univ_mem' Set.indicator_of_mem Filter.Tendsto.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul tendsto_order instOrderTopologyReal tendsto_iff_norm_sub_tendsto_zero zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike integrableOn_peak_smul_of_integrableOn_of_tendsto smul_sub MeasureTheory.integral_sub MeasureTheory.Integrable.smul_const MeasureTheory.Measure.restrict_restrict Set.inter_eq_left MeasureTheory.Integrable.of_integral_ne_zero zero_sub norm_neg CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass MeasureTheory.setIntegral_indicator Set.inter_eq_right integral_smul_const sub_add_cancel one_smul zero_add
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux 📖	mathematical	MeasurableSet Set Set.instHasSubset Filter Filter.instMembership nhdsWithin Filter.Eventually TendstoUniformlyOn Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.instZero Real.instZero Set.instSDiff Filter.Tendsto MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict nhds UniformSpace.toTopologicalSpace Real.instOne MeasureTheory.AEStronglyMeasurable MeasureTheory.IntegrableOn SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	Metric.tendsto_nhds Nat.instAtLeastTwoHAddOfNat Filter.Tendsto.mono_left Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul Filter.tendsto_id tendsto_const_nhds Filter.Tendsto.const_mul nhdsWithin_le_nhds Ioo_mem_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.Eventually.exists nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and tendsto_order MulZeroClass.mul_zero zero_add MulZeroClass.zero_mul mem_nhdsWithin Filter.inter_mem Metric.ball_mem_nhds Set.inter_comm HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.inter_subset_right Filter.mp_mem integrableOn_peak_smul_of_integrableOn_of_tendsto tendsto_iff_norm_sub_tendsto_zero Metric.tendstoUniformlyOn_iff Filter.univ_mem' MeasureTheory.Integrable.of_integral_ne_zero 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf 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_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt zero_sub norm_neg CStarRing.norm_of_mem_unitary instCStarRingReal SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass MeasureTheory.norm_integral_le_integral_norm MeasureTheory.setIntegral_mono_on IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule MeasureTheory.IntegrableOn.mono_set MeasureTheory.Integrable.norm MeasureTheory.Integrable.mul_const MeasurableSet.inter IsOpen.measurableSet BorelSpace.opensMeasurable norm_smul NormedSpace.toNormSMulClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono LT.lt.le mem_ball_zero_iff norm_nonneg MeasureTheory.setIntegral_mono_set Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass mul_nonneg MeasureTheory.setIntegral_congr_fun Real.norm_of_nonneg MeasureTheory.integral_mul_const mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono le_of_not_gt Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_nonpos_of_le LE.le.trans le_abs_self le_of_lt Set.diff_subset MeasureTheory.Integrable.const_mul MeasurableSet.diff dist_zero_left MeasureTheory.integral_const_mul Set.diff_union_inter MeasureTheory.setIntegral_union Set.disjoint_sdiff_inter norm_add_le add_le_add IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add dist_zero_right LE.le.trans_lt
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn 📖	mathematical	IsCompact ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT Real.instLE Real.instZero Set Set.instMembership closure interior SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.Tendsto SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Monoid.toNatPow Filter.atTop Nat.instPreorder nhds	—	tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn ContinuousOn.integrableOn_compact BorelSpace.opensMeasurable isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure TopologicalSpace.t2Space_of_metrizableSpace IsClosed.closure_eq IsCompact.isClosed closure_mono interior_subset
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn 📖	mathematical	IsCompact ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT Real.instLE Real.instZero Set Set.instMembership closure interior MeasureTheory.IntegrableOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousWithinAt	Filter.Tendsto SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Monoid.toNatPow Filter.atTop Nat.instPreorder nhds	—	IsClosed.closure_eq IsCompact.isClosed TopologicalSpace.t2Space_of_metrizableSpace closure_mono interior_subset tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos IsOpen.measure_pos IsOpen.inter isOpen_interior mem_closure_iff MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_inter subset_refl Set.instReflSubset
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos 📖	mathematical	IsCompact ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.instInter ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLT Real.instLE Real.instZero Set.instMembership MeasureTheory.IntegrableOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousWithinAt	Filter.Tendsto SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Monoid.toNatPow Filter.atTop Nat.instPreorder nhds	—	mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MeasureTheory.setIntegral_nonneg IsCompact.measurableSet BorelSpace.opensMeasurable TopologicalSpace.t2Space_of_metrizableSpace pow_nonneg Real.instZeroLEOneClass ContinuousOn.integrableOn_compact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure ContinuousOn.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.ae_restrict_mem Filter.univ_mem' MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae continuousOn_iff isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid LT.lt.trans_le MeasureTheory.measure_mono ne_of_gt pow_pos MeasureTheory.integral_const_mul inv_mul_cancel₀ LT.lt.ne' Set.eq_empty_or_nonempty le_rfl instIsEmptyFalse IsCompact.exists_isMaxOn instClosedIciTopology IsCompact.diff ContinuousOn.mono Set.diff_subset exists_between LinearOrderedSemiField.toDenselyOrdered LE.le.trans_lt MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.measureReal_restrict_apply Set.univ_inter mul_comm MeasureTheory.setIntegral_mono_on IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule MeasureTheory.integrableOn_const LT.lt.ne lt_of_le_of_lt Set.inter_subset_right IsCompact.measure_lt_top enorm_ne_top MeasureTheory.IntegrableOn.mono MeasurableSet.inter IsOpen.measurableSet pow_le_pow_left₀ IsOrderedRing.toMulPosMono LT.lt.le MeasureTheory.setIntegral_mono_set Filter.Eventually.of_forall div_pow div_div ENNReal.toReal_pos div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono IsOrderedRing.toZeroLEOneClass mul_pos IsStrictOrderedRing.toZeroLEOneClass Filter.Tendsto.mul tendsto_const_nhds tendsto_pow_atTop_nhds_zero_of_lt_one AddGroup.existsAddOfLE Real.instArchimedean instOrderTopologyReal div_nonneg div_lt_one Metric.tendstoUniformlyOn_iff tendsto_order MulZeroClass.mul_zero dist_zero_left Real.norm_of_nonneg Filter.Tendsto.congr MeasureTheory.Integrable.aestronglyMeasurable MeasureTheory.Integrable.const_mul tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto Set.Subset.rfl self_mem_nhdsWithin MeasureTheory.integral_smul NormedSpace.toNormSMulClass smulCommClass_self

---

← Back to Index