ParametricIntervalIntegral

📁 Source: Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems hasDerivAt_integral_of_dominated_loc_of_deriv_le, hasDerivAt_integral_of_dominated_loc_of_lip, hasFDerivAt_integral_of_dominated_loc_of_lip, hasFDerivAt_integral_of_dominated_of_fderiv_le	4
Total	4

intervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasDerivAt_integral_of_dominated_loc_of_deriv_le 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Filter.Eventually MeasureTheory.AEStronglyMeasurable Real SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.measurableSpace MeasureTheory.Measure.restrict Set.uIoc Real.linearOrder IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Real.pseudoMetricSpace Real.normedAddCommGroup	HasDerivAt DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul intervalIntegral	—	MeasureTheory.Measure.instOuterMeasureClass IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul PseudoEMetricSpace.pseudoMetrizableSpace HasDerivAt.congr_simp intervalIntegral_eq_integral_uIoc hasDerivAt_integral_of_dominated_loc_of_deriv_le MeasureTheory.ae_restrict_iff' measurableSet_uIoc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid HasDerivAt.const_smul IsScalarTower.to_smulCommClass' Real.isScalarTower TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
hasDerivAt_integral_of_dominated_loc_of_lip 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Filter.Eventually MeasureTheory.AEStronglyMeasurable Real SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.measurableSpace MeasureTheory.Measure.restrict Set.uIoc Real.linearOrder IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Real.pseudoMetricSpace Real.normedAddCommGroup	HasDerivAt DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul intervalIntegral	—	MeasureTheory.Measure.instOuterMeasureClass IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul PseudoEMetricSpace.pseudoMetrizableSpace HasDerivAt.congr_simp intervalIntegral_eq_integral_uIoc hasDerivAt_integral_of_dominated_loc_of_lip MeasureTheory.ae_restrict_iff' measurableSet_uIoc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid HasDerivAt.const_smul IsScalarTower.to_smulCommClass' Real.isScalarTower TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
hasFDerivAt_integral_of_dominated_loc_of_lip 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually MeasureTheory.AEStronglyMeasurable Real Real.measurableSpace MeasureTheory.Measure.restrict Set.uIoc Real.linearOrder IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Real.pseudoMetricSpace Real.normedAddCommGroup	ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing HasFDerivAt intervalIntegral NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedSpace Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PseudoEMetricSpace.pseudoMetrizableSpace intervalIntegral_eq_integral_uIoc hasFDerivAt_integral_of_dominated_loc_of_lip MeasureTheory.ae_restrict_iff' measurableSet_uIoc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid HasFDerivAt.const_smul
hasFDerivAt_integral_of_dominated_of_fderiv_le 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually MeasureTheory.AEStronglyMeasurable Real Real.measurableSpace MeasureTheory.Measure.restrict Set.uIoc Real.linearOrder IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Real.pseudoMetricSpace Real.normedAddCommGroup	HasFDerivAt DenselyNormedField.toNontriviallyNormedField intervalIntegral NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace intervalIntegral_eq_integral_uIoc HasFDerivAt.const_smul hasFDerivAt_integral_of_dominated_of_fderiv_le PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.ae_restrict_iff' measurableSet_uIoc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid

---

← Back to Index