AEEqOfIntegralContDiff

📁 Source: Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_eq_zero_of_integral_contDiff_smul_eq_zero, ae_eq_zero_of_integral_contMDiff_smul_eq_zero, ae_eq_zero_of_integral_contMDiff_smul_eq_zero', ae_eq_zero_of_integral_smooth_smul_eq_zero, ae_eq_zero_of_integral_smooth_smul_eq_zero', ae_eq_of_integral_contDiff_smul_eq, ae_eq_of_integral_contMDiff_smul_eq, ae_eq_of_integral_smooth_smul_eq, ae_eq_zero_of_integral_contDiff_smul_eq_zero, ae_eq_zero_of_integral_contMDiff_smul_eq_zero, ae_eq_zero_of_integral_smooth_smul_eq_zero, instBorelSpaceSubtypeMemOpens	12
Total	12

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_zero_of_integral_contDiff_smul_eq_zero 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.LocallyIntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_zero_of_integral_contMDiff_smul_eq_zero ContMDiffAdd.toIsManifold instContMDiffAddSelf TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper ContMDiff.contDiff
ae_eq_zero_of_integral_contMDiff_smul_eq_zero 📖	mathematical	IsOpen MeasureTheory.LocallyIntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_zero_of_integral_contMDiff_smul_eq_zero' isSigmaCompact_iff_sigmaCompactSpace sigmaCompactSpace_of_locallyCompact_secondCountable locallyCompactSpace ChartedSpace.locallyCompactSpace ModelWithCorners.locallyCompactSpace locallyCompact_of_proper FiniteDimensional.proper_real TopologicalSpace.Subtype.secondCountableTopology ChartedSpace.secondCountable_of_sigmaCompact ModelWithCorners.secondCountableTopology secondCountable_of_proper
ae_eq_zero_of_integral_contMDiff_smul_eq_zero' 📖	mathematical	IsOpen IsSigmaCompact MeasureTheory.LocallyIntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	measurableSet BorelSpace.opensMeasurable MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' ae_restrict_iff_subtype ae_eq_zero_of_integral_contMDiff_smul_eq_zero TopologicalSpace.Opens.instIsManifoldSubtypeMem instBorelSpaceSubtypeMemOpens instT2SpaceSubtype isSigmaCompact_iff_sigmaCompactSpace MeasureTheory.locallyIntegrable_comap Function.Injective.extend_apply Subtype.val_injective MeasureTheory.integral_subtype_comap MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero Function.extend_apply' zero_smul ContMDiff.extend_zero HasCompactSupport.extend_zero continuous_subtype_val HasSubset.Subset.trans Set.instIsTransSubset HasCompactSupport.tsupport_extend_zero_subset Subtype.coe_image_subset
ae_eq_zero_of_integral_smooth_smul_eq_zero 📖	mathematical	IsOpen MeasureTheory.LocallyIntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_zero_of_integral_contMDiff_smul_eq_zero
ae_eq_zero_of_integral_smooth_smul_eq_zero' 📖	mathematical	IsOpen IsSigmaCompact MeasureTheory.LocallyIntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_zero_of_integral_contMDiff_smul_eq_zero'

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_of_integral_contDiff_smul_eq 📖	mathematical	MeasureTheory.LocallyIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_of_integral_contMDiff_smul_eq ContMDiffAdd.toIsManifold instContMDiffAddSelf TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper ContMDiff.contDiff
ae_eq_of_integral_contMDiff_smul_eq 📖	mathematical	MeasureTheory.LocallyIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ae_eq_zero_of_integral_contMDiff_smul_eq_zero MeasureTheory.LocallyIntegrable.sub smul_sub MeasureTheory.integral_sub MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport NormedSpace.toIsBoundedSMul BorelSpace.opensMeasurable ContMDiff.continuous sub_eq_zero Filter.mp_mem Filter.univ_mem'
ae_eq_of_integral_smooth_smul_eq 📖	mathematical	MeasureTheory.LocallyIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_of_integral_contMDiff_smul_eq
ae_eq_zero_of_integral_contDiff_smul_eq_zero 📖	mathematical	MeasureTheory.LocallyIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_zero_of_integral_contMDiff_smul_eq_zero ContMDiffAdd.toIsManifold instContMDiffAddSelf TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper ContMDiff.contDiff
ae_eq_zero_of_integral_contMDiff_smul_eq_zero 📖	mathematical	MeasureTheory.LocallyIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ModelWithCorners.locallyCompactSpace locallyCompact_of_proper FiniteDimensional.proper_real ChartedSpace.locallyCompactSpace ModelWithCorners.secondCountableTopology secondCountable_of_proper ChartedSpace.secondCountable_of_sigmaCompact TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T4Space.of_paracompactSpace_t2Space paracompact_of_locallyCompact_sigmaCompact instWeaklyLocallyCompactSpaceOfLocallyCompactSpace TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology T3Space.toRegularSpace MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace IsCompact.exists_isCompact_cthickening exists_seq_strictAnti_tendsto' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology Metric.thickening_subset_cthickening_of_le LT.lt.le exists_contMDiff_support_eq_eq_one_iff Metric.isOpen_thickening IsCompact.isClosed Metric.self_subset_thickening MeasureTheory.integral_indicator IsCompact.measurableSet BorelSpace.opensMeasurable MeasureTheory.AEStronglyMeasurable.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.aestronglyMeasurable secondCountableTopologyEither_of_right instSecondCountableTopologyReal ContMDiff.continuous MeasureTheory.LocallyIntegrable.aestronglyMeasurable MeasureTheory.integrable_indicator_iff MeasureTheory.Integrable.norm MeasureTheory.LocallyIntegrable.integrableOn_isCompact MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem' norm_smul NormedSpace.toNormSMulClass Set.le_indicator_apply Set.mem_range_self Real.norm_of_nonneg mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg Function.notMem_support Mathlib.Tactic.Contrapose.contrapose₄ norm_zero MulZeroClass.zero_mul one_smul Set.indicator_of_mem T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Set.indicator_of_notMem Filter.Tendsto.congr' tendsto_const_nhds Metric.closure_eq_iInter_thickening IsClosed.closure_eq Filter.mp_mem tendsto_order Metric.thickening_mono zero_smul MeasureTheory.tendsto_integral_of_dominated_convergence HasCompactSupport.of_support_subset_isCompact
ae_eq_zero_of_integral_smooth_smul_eq_zero 📖	mathematical	MeasureTheory.LocallyIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral Real 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ae_eq_zero_of_integral_contMDiff_smul_eq_zero
instBorelSpaceSubtypeMemOpens 📖	mathematical	—	BorelSpace TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype Subtype.instMeasurableSpace	—	Subtype.borelSpace

---

← Back to Index