BoundedVariation

📁 Source: Mathlib/Analysis/BoundedVariation.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_differentiableAt_of_mem_uIcc, ae_differentiableWithinAt_of_mem_real, ae_differentiableWithinAt_real, ae_differentiableAt_real, ae_differentiableAt, ae_differentiableWithinAt, ae_differentiableWithinAt_of_mem, ae_differentiableWithinAt_of_mem_pi, ae_differentiableWithinAt_of_mem_real	9
Total	9

BoundedVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_differentiableAt_of_mem_uIcc 📖	mathematical	BoundedVariationOn Real Real.linearOrder EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.uIcc Real.lattice	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.NoAtoms.measure_singleton Real.noAtoms_volume Filter.mp_mem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem locallyBoundedVariationOn Filter.univ_mem' DifferentiableWithinAt.differentiableAt Set.mem_Icc Set.uIcc.eq_1 Icc_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid lt_of_le_of_ne

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_differentiableWithinAt_of_mem_real 📖	mathematical	LipschitzOnWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NormedAddCommGroup.toMetricSpace	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem locallyBoundedVariationOn
ae_differentiableWithinAt_real 📖	mathematical	LipschitzOnWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NormedAddCommGroup.toMetricSpace MeasurableSet Real.measurableSpace	Filter.Eventually DifferentiableWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume	—	LocallyBoundedVariationOn.ae_differentiableWithinAt locallyBoundedVariationOn

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_differentiableAt_real 📖	mathematical	LipschitzWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NormedAddCommGroup.toMetricSpace	Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	LocallyBoundedVariationOn.ae_differentiableAt locallyBoundedVariationOn

LocallyBoundedVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_differentiableAt 📖	mathematical	LocallyBoundedVariationOn Real Real.linearOrder EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ae_differentiableWithinAt_of_mem Filter.univ_mem' differentiableWithinAt_univ Set.mem_univ
ae_differentiableWithinAt 📖	mathematical	LocallyBoundedVariationOn Real Real.linearOrder EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace MeasurableSet Real.measurableSpace	Filter.Eventually DifferentiableWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' ae_differentiableWithinAt_of_mem
ae_differentiableWithinAt_of_mem 📖	mathematical	LocallyBoundedVariationOn Real Real.linearOrder EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Pi.t2Space Finite.of_fintype isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule MeasureTheory.Measure.instOuterMeasureClass ae_differentiableWithinAt_of_mem_pi LipschitzWith.comp_locallyBoundedVariationOn RingHomIsometric.ids ContinuousLinearEquiv.lipschitz Filter.mp_mem Filter.univ_mem' ContinuousLinearEquiv.symm_comp_self DifferentiableAt.comp_differentiableWithinAt ContinuousLinearEquiv.differentiableAt
ae_differentiableWithinAt_of_mem_pi 📖	mathematical	LocallyBoundedVariationOn Real Real.linearOrder pseudoEMetricSpacePi EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	LipschitzWith.eval MeasureTheory.Measure.instOuterMeasureClass ae_differentiableWithinAt_of_mem_real LipschitzWith.comp_locallyBoundedVariationOn Filter.mp_mem MeasureTheory.ae_all_iff Finite.to_countable Finite.of_fintype Filter.univ_mem' differentiableWithinAt_pi
ae_differentiableWithinAt_of_mem_real 📖	mathematical	LocallyBoundedVariationOn Real Real.linearOrder EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.instOuterMeasureClass exists_monotoneOn_sub_monotoneOn Filter.mp_mem MonotoneOn.ae_differentiableWithinAt_of_mem Filter.univ_mem' DifferentiableWithinAt.sub

---

← Back to Index