AbsolutelyContinuousFun

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

Statistics

Metric	Count
Definitions	0
Theorems const_of_ae_hasDerivAt_zero, dist_le_of_pairwiseDisjoint_hasSum, integral_deriv_eq_sub, integral_deriv_mul_eq_sub, integral_mul_deriv_eq_deriv_mul, exists_dist_slope_lt_pairwiseDisjoint_hasSum	6
Total	6

AbsolutelyContinuousOnInterval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_of_ae_hasDerivAt_zero 📖	—	AbsolutelyContinuousOnInterval SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul MeasureTheory.Measure.instOuterMeasureClass Set.uIcc_of_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Set.mem_Icc Mathlib.Tactic.Linarith.sub_neg_of_lt LE.le.eq_or_lt dist_self LT.lt.le Filter.mp_mem Filter.univ_mem' div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_not_ge Mathlib.Tactic.Linarith.add_lt_of_neg_of_le exists_dist_slope_lt_pairwiseDisjoint_hasSum le_imp_le_of_le_of_le le_refl mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono le_of_lt dist_eq_norm sub_zero mul_comm Real.norm_of_nonneg norm_smul NormedSpace.toNormSMulClass norm_inv Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt abs_pos_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.one GroupWithZero.toNontrivial norm_sub_rev Finset.sum_le_sum Finset.mul_sum Summable.sum_le_tsum HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional HasSum.summable HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_zero_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.cons_pos Summable.hasSum summable_of_sum_le Real.tsum_le_of_sum_le dist_le_of_pairwiseDisjoint_hasSum mono Mathlib.Tactic.Linarith.add_nonpos Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq exists_between LinearOrderedSemiField.toDenselyOrdered dist_pos symm Set.uIcc_comm Mathlib.Tactic.Linarith.add_neg
dist_le_of_pairwiseDisjoint_hasSum 📖	—	Real Real.instLE AbsolutelyContinuousOnInterval Real.instLT Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.Icc Real.instPreorder HasSum Set.Elem Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub Set.instMembership SummationFilter.unconditional Dist.dist PseudoMetricSpace.toDist	—	—	Set.PairwiseDisjoint.subset Finset.intervalGapsWithin_le_fst Finset.intervalGapsWithin_fst_le_snd Finset.intervalGapsWithin_snd_le Finset.intervalGapsWithin_pairwiseDisjoint_Ioc Finset.sum_nbij Subtype.coe_eta Finset.coe_image Filter.tendsto_inf Finset.sum_congr dist_comm Real.dist_eq abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.sum_intervalGapsWithin_eq_sub_sub_sum Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg Filter.Tendsto.const_sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.Tendsto.mono_left Set.MapsTo.tendsto Filter.principal_univ Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.comp HasSum.eq_1 Finset.sum_eq_sum_range_intervalGapsWithin Finset.sum_range_succ add_right_comm Finset.sum_add_distrib le_imp_le_of_le_of_le le_refl add_le_add_left covariant_swap_add_of_covariant_add Finset.sum_le_sum dist_triangle dist_le_range_sum_dist Finset.intervalGapsWithin.congr_simp Nat.cast_zero Finset.intervalGapsWithin_zero_fst Fin.natCast_eq_last Finset.intervalGapsWithin_last_snd le_of_tendsto_of_tendsto' HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.atTop_neBot Finset.isDirected_le T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace
integral_deriv_eq_sub 📖	mathematical	AbsolutelyContinuousOnInterval Real Real.pseudoMetricSpace	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral intervalIntegrable_deriv sub IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem IntervalIntegrable.ae_hasDerivAt_integral ae_differentiableAt Filter.univ_mem' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg zero_add Mathlib.Tactic.Abel.zero_termg HasDerivAt.sub DifferentiableAt.hasDerivAt const_of_ae_hasDerivAt_zero intervalIntegral.integral_same sub_zero
integral_deriv_mul_eq_sub 📖	mathematical	AbsolutelyContinuousOnInterval Real Real.pseudoMetricSpace	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd Real.instMul deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	integral_deriv_eq_sub fun_mul intervalIntegral.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ae_differentiableAt Filter.univ_mem' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.mul DifferentiableAt.hasDerivAt HasDerivAt.deriv
integral_mul_deriv_eq_deriv_mul 📖	mathematical	AbsolutelyContinuousOnInterval Real Real.pseudoMetricSpace	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	integral_deriv_mul_eq_sub intervalIntegral.integral_sub IntervalIntegrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IntervalIntegrable.mul_continuousOn intervalIntegrable_deriv continuousOn IntervalIntegrable.continuousOn_mul add_sub_cancel_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_dist_slope_lt_pairwiseDisjoint_hasSum 📖	mathematical	Real Real.instLE Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume Real.instLT Real.instZero	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup slope Real.instField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.Icc Real.instPreorder HasSum Set.Elem Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub Set.instMembership SummationFilter.unconditional	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul MeasureTheory.Measure.instOuterMeasureClass LE.le.eq_or_lt instIsEmptyFalse sub_self Set.instIsEmptyElemEmptyCollection Vitali.exists_disjoint_covering_ae' BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal Real.locallyFinite_volume Nat.instAtLeastTwoHAddOfNat Real.volume_closedBall Real.volume_Icc ENNReal.ofReal_ofNat ENNReal.ofReal_mul Mathlib.Meta.NormNum.isNat_le_true Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.instAtLeastTwo ENNReal.ofReal_le_ofReal_iff le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.sub_neg_of_lt interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instNontrivial instNoMaxOrderOfNontrivial HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Eventually.frequently nhdsGT_neBot hasDerivAt_iff_tendsto_slope Metric.tendsto_nhdsWithin_nhds eventually_nhdsWithin_iff eventually_nhds_iff isOpen_Ioo eventually_mem_of_tendsto_nhdsWithin Filter.mp_mem IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Filter.univ_mem' lt_of_not_ge Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_neg CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true dist_self_add_left abs_eq_self LT.lt.le add_sub_cancel_left Subtype.prop Subtype.coe_ne_coe MeasureTheory.measure_eq_zero_iff_ae_notMem Set.iUnion_coe_set Set.iUnion_congr_Prop MeasureTheory.measure_eq_measure_of_null_diff Real.volume_Ioo Summable.hasSum_iff TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional ENNReal.toReal_ofReal ENNReal.tsum_toReal_eq MeasureTheory.measure_iUnion

---

← Back to Index