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 📖	mathematical	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	Real Real.instLE 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 instReflLe 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 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 Real.pseudoMetricSpace 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 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 Real.pseudoMetricSpace 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 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 Real.pseudoMetricSpace MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	integral_deriv_mul_eq_sub intervalIntegral.integral_sub IntervalIntegrable.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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	Set Real Real.instLT Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup slope Real.instField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Set.PairwiseDisjoint 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add 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 Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.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