FundThmCalculus

📁 Source: Mathlib/MeasureTheory/Integral/Bochner/FundThmCalculus.lean

Statistics

Metric	Count
Definitions	0
Theorems integral_sub_linear_isLittleO_ae, integral_sub_linear_isLittleO_ae, integral_sub_linear_isLittleO_ae, integral_sub_linear_isLittleO_ae	4
Total	4

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_sub_linear_isLittleO_ae 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup StronglyMeasurableAtFilter nhds Filter.Tendsto Set Filter.smallSets Filter.EventuallyEq Real MeasureTheory.Measure.real	Asymptotics.IsLittleO NormedAddCommGroup.toNorm Real.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.integral MeasureTheory.Measure.restrict 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.integral_sub_linear_isLittleO_ae nhds_isMeasurablyGenerated Filter.Tendsto.mono_left MeasureTheory.Measure.instOuterMeasureClass inf_le_left MeasureTheory.Measure.finiteAt_nhds

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_sub_linear_isLittleO_ae 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership MeasurableSet Filter.Tendsto Filter.smallSets nhdsWithin Filter.EventuallyEq Real MeasureTheory.Measure.real	Asymptotics.IsLittleO NormedAddCommGroup.toNorm Real.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.integral MeasureTheory.Measure.restrict 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	—	ContinuousWithinAt.integral_sub_linear_isLittleO_ae self_mem_nhdsWithin aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_sub_linear_isLittleO_ae 📖	mathematical	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasurableSet StronglyMeasurableAtFilter nhdsWithin Filter.Tendsto Set Filter.smallSets Filter.EventuallyEq Real MeasureTheory.Measure.real	Asymptotics.IsLittleO NormedAddCommGroup.toNorm Real.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.integral MeasureTheory.Measure.restrict 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.integral_sub_linear_isLittleO_ae MeasurableSet.nhdsWithin_isMeasurablyGenerated Filter.Tendsto.mono_left MeasureTheory.Measure.instOuterMeasureClass inf_le_left MeasureTheory.Measure.finiteAt_nhdsWithin

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_sub_linear_isLittleO_ae 📖	mathematical	Filter.Tendsto Filter Filter.instInf MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup StronglyMeasurableAtFilter MeasureTheory.Measure.FiniteAtFilter Set Filter.smallSets Filter.EventuallyEq Real MeasureTheory.Measure.real	Asymptotics.IsLittleO NormedAddCommGroup.toNorm Real.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.integral MeasureTheory.Measure.restrict 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	—	MeasureTheory.Measure.instOuterMeasureClass Asymptotics.isLittleO_iff Filter.eventually_smallSets_eventually eventually Metric.closedBall_mem_nhds Filter.mp_mem StronglyMeasurableAtFilter.eventually MeasureTheory.IntegrableAtFilter.eventually MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae MeasureTheory.Measure.FiniteAtFilter.eventually Filter.univ_mem' dist_eq_norm MeasureTheory.setIntegral_const MeasureTheory.integral_sub MeasureTheory.integrableOn_const LT.lt.ne enorm_ne_top Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid MeasureTheory.measureReal_nonneg MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae' Asymptotics.IsLittleO.congr' Asymptotics.IsLittleO.comp_tendsto Filter.Eventually.mono

---

← Back to Index