SmoothApprox

📁 Source: Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

Statistics

Metric	Count
Definitions	0
Theorems exist_eLpNorm_sub_le_of_continuous, dense_hasCompactSupport_contDiff, exist_eLpNorm_sub_le	3
Total	3

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exist_eLpNorm_sub_le_of_continuous 📖	mathematical	Real Real.instLT Real.instZero HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Continuous	ContDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ENNReal.ofReal	—	MeasureTheory.Measure.instOuterMeasureClass sub_zero MeasureTheory.eLpNorm_congr_ae MeasureTheory.eLpNorm_zero ENNReal.instCanonicallyOrderedAdd contDiff_const LT.lt.ne IsCompact.measure_lt_top ENNReal.toReal_pos LT.lt.ne' MeasureTheory.pos_mono subset_tsupport pos_of_ne_zero MeasureTheory.Measure.measure_support_eq_zero_iff mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.rpow_pos_of_pos ENNReal.ofReal_toReal ENNReal.ofReal_rpow_of_pos ENNReal.ofReal_mul LT.lt.le ENNReal.ofReal_le_ofReal_iff mul_assoc Real.rpow_add neg_add_cancel Real.rpow_zero mul_one le_refl Continuous.exists_contDiff_approx continuous_const mono LE.le.trans MeasureTheory.eLpNorm_sub_le_of_dist_bdd IsCompact.measurableSet BorelSpace.opensMeasurable TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace dist_comm HasSubset.Subset.trans Set.instIsTransSubset

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_hasCompactSupport_contDiff 📖	mathematical	—	Dense MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNormedAddCommGroup setOf Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall MeasureTheory.MemLp.exist_eLpNorm_sub_le Fact.out memLp Continuous.memLp_of_hasCompactSupport BorelSpace.opensMeasurable ContDiff.continuous MeasureTheory.MemLp.coeFn_toLp Metric.mem_closedBall dist_comm dist_def ENNReal.le_ofReal_iff_toReal_le MeasureTheory.MemLp.eLpNorm_ne_top MeasureTheory.MemLp.sub LT.lt.le MeasureTheory.eLpNorm_congr_ae Filter.EventuallyEq.sub Filter.EventuallyEq.refl

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exist_eLpNorm_sub_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Real Real.instLT Real.instZero	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat MeasureTheory.eLpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ENNReal.ofReal	—	Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo ENNReal.ofReal_pos exists_hasCompactSupport_eLpNorm_sub_le PerfectlyNormalSpace.toNormalSpace T6Space.toPerfectlyNormalSpace instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts LT.lt.ne' HasCompactSupport.exist_eLpNorm_sub_le_of_continuous sub_sub_sub_cancel_right le_imp_le_of_le_of_le MeasureTheory.eLpNorm_sub_le MeasureTheory.AEStronglyMeasurable.sub aestronglyMeasurable Continuous.aestronglyMeasurable BorelSpace.opensMeasurable secondCountableTopologyEither_of_left ContDiff.continuous le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid MeasureTheory.eLpNorm_sub_comm add_le_add_right ENNReal.ofReal_add LT.lt.le add_halves CharZero.NeZero.two RCLike.charZero_rclike

---

← Back to Index