DistLEIntegral

📁 Source: Mathlib/MeasureTheory/Integral/IntervalIntegral/DistLEIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems isBigO_norm_rpow_add_one_of_fderiv_of_apply_eq_zero, norm_sub_le_integral_of_norm_deriv_le_of_le, norm_sub_le_mul_volume_of_norm_deriv_le_of_le, norm_sub_le_mul_volume_of_norm_fderiv_le, norm_sub_le_mul_volume_of_norm_lineDeriv_le, sub_isBigO_norm_rpow_add_one_of_fderiv	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_norm_rpow_add_one_of_fderiv_of_apply_eq_zero 📖	mathematical	Real Real.instLE Real.instZero Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds Asymptotics.IsBigO ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.hasOpNorm Real.norm fderiv Real.instPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Real.instAdd Real.instOne	—	sub_zero sub_isBigO_norm_rpow_add_one_of_fderiv
norm_sub_le_integral_of_norm_deriv_le_of_le 📖	mathematical	Real Real.instLE ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder DifferentiableOn 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 NormedAddCommGroup.toAddCommGroup Set.Ioo Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup intervalIntegral	—	MeasureTheory.Measure.instOuterMeasureClass Set.uIoc_of_le MeasureTheory.Measure.restrict_congr_set MeasureTheory.Ioo_ae_eq_Ioc Real.noAtoms_volume Filter.EventuallyLE.eq_1 MeasureTheory.ae_restrict_iff' measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid intervalIntegral.integral_eq_sub_of_hasDeriv_right Set.uIcc_of_le IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul min_eq_left max_eq_right HasDerivAt.hasDerivWithinAt DifferentiableOn.hasDerivAt IsOpen.mem_nhds isOpen_Ioo IntervalIntegrable.mono_fun aestronglyMeasurable_deriv secondCountableTopologyEither_of_left instSecondCountableTopologyReal Filter.EventuallyLE.trans Filter.Eventually.of_forall le_abs_self intervalIntegral.norm_integral_le_of_norm_le measurableSet_Ioc instClosedIicTopology Continuous.comp_continuousOn UniformSpace.Completion.continuous_coe SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul Differentiable.comp_differentiableOn ContinuousLinearMap.differentiable UniformSpace.Completion.coe_toComplL ContinuousLinearMap.hasFDerivAt Ioo_mem_nhds HasDerivAt.deriv HasFDerivAt.comp_hasDerivAt Filter.Eventually.mono UniformSpace.Completion.norm_coe UniformSpace.Completion.dist_eq UniformSpace.Completion.completeSpace
norm_sub_le_mul_volume_of_norm_deriv_le_of_le 📖	mathematical	Real Real.instLE ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Icc Real.instPreorder DifferentiableOn 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 NormedAddCommGroup.toAddCommGroup Set.Ioo Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul MeasureTheory.Measure.real setOf Set Set.instMembership deriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass norm_sub_le_integral_of_norm_deriv_le_of_le Filter.Eventually.mono Set.le_indicator_apply not_imp_comm MeasureTheory.subset_toMeasurable intervalIntegrable_iff_integrableOn_Ioo_of_le PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume enorm_ne_top MeasureTheory.IntegrableOn.indicator MeasureTheory.integrableOn_const Real.volume_Ioo intervalIntegral.integral_of_le MeasureTheory.Measure.restrict_congr_set Filter.EventuallyEq.symm MeasureTheory.Ioo_ae_eq_Ioc MeasureTheory.integral_indicator MeasureTheory.Measure.restrict_restrict MeasureTheory.setIntegral_const Real.instCompleteSpace smul_eq_mul mul_comm MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite measurableSet_Ioo MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal BorelSpace.opensMeasurable HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
norm_sub_le_mul_volume_of_norm_fderiv_le 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Set Set.instHasSubset openSegment Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.hasOpNorm fderiv	NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul MeasureTheory.Measure.real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume setOf Set.instMembership Set.Ioo Real.instPreorder Real.instZero Real.instOne DFunLike.coe AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor AffineMap.instFunLike AffineMap.lineMap ContinuousLinearMap.zero	—	lineMap_mem_openSegment covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LE.le.trans RingHomIsometric.ids Nat.instAtLeastTwoHAddOfNat norm_nonneg Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNNRat_lt_true Real.instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Nat.cast_zero ContinuousOn.mono DiffContOnCl.continuousOn HasSubset.Subset.trans Set.instIsTransSubset segment_subset_closure_openSegment LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instOrderTopologyReal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul closure_mono DifferentiableAt.lineDifferentiableAt DiffContOnCl.differentiableAt DifferentiableAt.lineDeriv_eq_fderiv ContinuousLinearMap.le_of_opNorm_le norm_sub_le_mul_volume_of_norm_lineDeriv_le Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing MeasureTheory.measureReal_mono Set.setOf_subset_setOf_of_imp Mathlib.Tactic.GCongr.and_right_mono ne_top_of_le_ne_top Real.volume_Ioo sub_zero ENNReal.ofReal_one MeasureTheory.measure_mono Set.inter_subset_left mul_nonneg
norm_sub_le_mul_volume_of_norm_lineDeriv_le 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup segment Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField LineDifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup DFunLike.coe AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor AffineMap.instFunLike AffineMap.lineMap SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul MeasureTheory.Measure.real setOf Set Set.instMembership Set.Ioo Real.instPreorder Real.instZero Real.instOne lineDeriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass ContinuousOn.comp Continuous.continuousOn AffineMap.lineMap_continuous instIsTopologicalAddTorsor_1 IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul segment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid HasDerivAt.scomp_of_eq IsScalarTower.left LineDifferentiableAt.hasLineDerivAt HasDerivAt.sub_const hasDerivAt_id HasDerivAt.congr_simp add_comm sub_self sub_smul add_add_sub_cancel one_smul norm_sub_le_mul_volume_of_norm_deriv_le_of_le zero_le_one Real.instZeroLEOneClass DifferentiableAt.differentiableWithinAt HasDerivAt.differentiableAt Filter.Eventually.mono HasDerivAt.deriv AffineMap.lineMap_apply_one AffineMap.lineMap_apply_zero Set.ext
sub_isBigO_norm_rpow_add_one_of_fderiv 📖	mathematical	Real Real.instLE Real.instZero Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds Asymptotics.IsBigO ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.hasOpNorm Real.norm fderiv Real.instPow Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	Real.instAdd Real.instOne	—	Asymptotics.IsBigO.exists_pos Metric.eventually_nhds_iff_ball Filter.Eventually.and Asymptotics.IsBigOWith_def Asymptotics.IsBigO.of_bound Real.norm_of_nonneg Real.rpow_nonneg norm_nonneg Real.rpow_add_one' ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_assoc Metric.closedBall_subset_ball mem_ball_iff_norm Convex.norm_image_sub_le_of_norm_fderiv_le instIsRCLikeNormedField convex_closedBall le_imp_le_of_le_of_le le_refl mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.rpow_le_rpow mem_closedBall_iff_norm le_of_lt dist_self dist_eq_norm_sub

---

← Back to Index