LebesgueDifferentiationThm

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

Statistics

Metric	Count
Definitions	0
Theorems ae_hasDerivAt_integral, ae_hasDerivAt_integral	2
Total	2

IntervalIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_hasDerivAt_integral 📖	mathematical	IntervalIntegrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.instOuterMeasureClass Set.uIcc_of_le MeasureTheory.NoAtoms.measure_singleton Real.noAtoms_volume MeasureTheory.Integrable.locallyIntegrable MeasureTheory.IntegrableOn.integrable_of_forall_notMem_eq_zero PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.integrableOn_congr_fun BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.mp_mem LocallyIntegrable.ae_hasDerivAt_integral Filter.univ_mem' HasDerivWithinAt.hasDerivAt IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivWithinAt.congr HasDerivAt.hasDerivWithinAt intervalIntegral.integral_congr_ae' Ioo_mem_nhds symm 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_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing lt_of_not_ge Set.uIcc_comm

LocallyIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_hasDerivAt_integral 📖	mathematical	MeasureTheory.LocallyIntegrable Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.volume	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	intervalIntegrable_iff PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.IntegrableOn.mono_set MeasureTheory.LocallyIntegrable.integrableOn_isCompact isCompact_uIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Set.uIoc_subset_uIcc MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure Real.borelSpace FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume instSecondCountableTopologyReal Real.locallyFinite_volume MeasureTheory.Measure.instOuterMeasureClass VitaliFamily.ae_tendsto_average Real.instCompleteSpace MeasureTheory.integral_Icc_eq_integral_Ioc Real.noAtoms_volume Filter.mp_mem IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.univ_mem' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_iff_tendsto_slope_left_right Filter.tendsto_congr' self_mem_nhdsWithin intervalIntegral.integral_interval_sub_left intervalIntegral.integral_of_ge mul_neg MeasureTheory.Measure.restrict_apply Set.univ_inter MeasureTheory.integral_smul_measure ENNReal.toReal_inv Real.volume_Icc ENNReal.toReal_ofReal covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.Tendsto.comp Real.tendsto_Icc_vitaliFamily_left intervalIntegral.integral_of_le Real.tendsto_Icc_vitaliFamily_right

---

← Back to Index