Documentation Verification Report

Rademacher

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

Statistics

Metric	Count
Definitions	0
Theorems `ae_differentiableWithinAt`, `ae_differentiableWithinAt_of_mem`, `ae_differentiableWithinAt_of_mem_of_real`, `ae_differentiableWithinAt_of_mem_pi`, `ae_differentiableAt`, `ae_differentiableAt_of_real`, `ae_exists_fderiv_of_countable`, `ae_lineDeriv_sum_eq`, `ae_lineDifferentiableAt`, `hasFDerivAt_of_hasLineDerivAt_of_closure`, `integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul`, `integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'`, `integral_lineDeriv_mul_eq`, `locallyIntegrable_lineDeriv`, `memLp_lineDeriv`, `ae_differentiableAt_norm`, `dense_differentiableAt_norm`	17
Total	17

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_differentiableWithinAt` 📖	mathematical	`LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `MeasurableSet`	`Filter.Eventually` `DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `ae_differentiableWithinAt_of_mem`
`ae_differentiableWithinAt_of_mem` 📖	mathematical	`LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `Finite.of_fintype` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `MeasureTheory.Measure.instOuterMeasureClass` `ae_differentiableWithinAt_of_mem_pi` `RingHomIsometric.ids` `LipschitzWith.comp_lipschitzOnWith` `ContinuousLinearEquiv.lipschitz` `Filter.mp_mem` `Filter.univ_mem'` `ContinuousLinearEquiv.symm_comp_self` `DifferentiableAt.comp_differentiableWithinAt` `ContinuousLinearEquiv.differentiableAt`
`ae_differentiableWithinAt_of_mem_of_real` 📖	mathematical	`LipschitzOnWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `extend_real` `Filter.mp_mem` `LipschitzWith.ae_differentiableAt_of_real` `Filter.univ_mem'` `DifferentiableWithinAt.congr` `DifferentiableAt.differentiableWithinAt`
`ae_differentiableWithinAt_of_mem_pi` 📖	mathematical	`LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `pseudoEMetricSpacePi` `Real` `Real.metricSpace`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`LipschitzWith.eval` `MeasureTheory.Measure.instOuterMeasureClass` `ae_differentiableWithinAt_of_mem_of_real` `LipschitzWith.comp_lipschitzOnWith` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `Finite.to_countable` `Finite.of_fintype` `Filter.univ_mem'` `differentiableWithinAt_pi`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_differentiableAt` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Filter.Eventually` `DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `LipschitzOnWith.ae_differentiableWithinAt_of_mem` `lipschitzOnWith_univ`
`ae_differentiableAt_of_real` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`Filter.Eventually` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `TopologicalSpace.exists_countable_dense` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `Dense.closure_eq` `Set.subset_univ` `Filter.mp_mem` `ae_exists_fderiv_of_countable` `Filter.univ_mem'` `HasFDerivAt.differentiableAt` `hasFDerivAt_of_hasLineDerivAt_of_closure`
`ae_exists_fderiv_of_countable` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`Filter.Eventually` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `RingHomInvPair.ids` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_ball_iff` `ae_lineDeriv_sum_eq` `ae_lineDifferentiableAt` `Filter.mp_mem` `Filter.univ_mem'` `IsTopologicalAddGroup.toContinuousAdd` `instIsTopologicalAddGroupReal` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Algebra.to_smulCommClass` `Finite.of_fintype` `Module.Basis.constr_apply_fintype` `Finset.sum_congr` `Module.Basis.sum_repr` `LineDifferentiableAt.hasLineDerivAt`
`ae_lineDeriv_sum_eq` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`Filter.Eventually` `lineDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`ae_eq_of_integral_contDiff_smul_eq` `Real.instCompleteSpace` `locallyIntegrable_lineDeriv` `MeasureTheory.locallyIntegrable_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.LocallyIntegrable.smul` `Real.isBoundedSMul` `Finset.smul_sum` `MeasureTheory.Integrable.smul_of_top_left` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `ContDiff.continuous` `MeasureTheory.MemLp.const_smul` `memLp_lineDeriv` `MeasureTheory.integral_finset_sum` `MeasureTheory.Integrable.const_mul` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `Continuous.clm_apply` `ContDiff.continuous_fderiv` `continuous_const` `continuous` `HasCompactSupport.mul_right` `HasCompactSupport.comp_left` `HasCompactSupport.fderiv` `Finset.sum_mul` `Finset.sum_congr` `mul_assoc` `MeasureTheory.integral_const_mul` `ContDiff.lipschitzWith_of_hasCompactSupport` `integral_lineDeriv_mul_eq` `DifferentiableAt.lineDeriv_eq_fderiv` `Differentiable.differentiableAt` `ContDiff.differentiable` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_sum` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `neg_mul` `MeasureTheory.integral_neg` `mul_neg` `Finset.sum_neg_distrib` `mul_comm`
`ae_lineDifferentiableAt` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`Filter.Eventually` `LineDifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Measure.instOuterMeasureClass` `ae_differentiableAt_real` `FiniteDimensional.rclike_to_real` `RingHomIsometric.ids` `comp` `add` `const` `ContinuousLinearMap.lipschitz` `Filter.mp_mem` `Filter.univ_mem'` `add_zero` `DifferentiableAt.const_add` `differentiableAt_id` `add_assoc` `add_smul` `DifferentiableAt.comp` `MeasureTheory.ae_mem_of_ae_add_linearMap_mem` `Real.instCompleteSpace` `Real.borelSpace` `instIsAddHaarMeasureVolume` `locallyCompact_of_proper` `instProperSpaceReal` `FiniteDimensional.proper_real` `measurableSet_lineDifferentiableAt` `BorelSpace.opensMeasurable` `continuous`
`hasFDerivAt_of_hasLineDerivAt_of_closure` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set` `Set.instHasSubset` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `HasLineDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.toModule` `Real.normedField` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup`	—	`hasFDerivAt_iff_isLittleO_nhds_zero` `Asymptotics.isLittleO_iff` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_nonneg` `NNReal.coe_nonneg` `norm_nonneg` `RingHomIsometric.ids` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `mul_div_cancel₀` `ne_of_gt` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.mem_closure_iff` `Set.mem_biUnion` `IsCompact.elim_finite_subcover_image` `isCompact_sphere` `FiniteDimensional.proper_real` `Metric.isOpen_ball` `Set.Finite.eventually_all` `Asymptotics.IsLittleO.def` `hasLineDerivAt_iff_isLittleO_nhds_zero` `Metric.mem_nhds_iff` `mem_ball_zero_iff` `eq_or_ne` `add_zero` `sub_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `norm_zero` `MulZeroClass.mul_zero` `sub_zero` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_norm` `inv_mul_cancel₀` `norm_ne_zero_iff` `smul_smul` `mul_inv_cancel₀` `one_smul` `norm_sub_rev` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `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.Tactic.Abel.const_add_termg` `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.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Abel.zero_termg` `norm_add₃_le` `add_le_add` `norm_sub_le` `smul_sub` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `ContinuousLinearMap.lipschitz` `dist_zero_right` `add_sub_add_left_eq_sub` `add_le_add_left` `le_of_lt` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.cast_pos`
`integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Filter.Tendsto` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instInv` `Real.instSub` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `nhdsWithin` `Real.instZero` `Set.Ioi` `Real.instPreorder` `nhds` `lineDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.tendsto_integral_filter_of_dominated_convergence` `TopologicalSpace.isCountablyGenerated_nhdsWithin` `FirstCountableTopology.nhds_generated_countable` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.univ_mem'` `MeasureTheory.AEStronglyMeasurable.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.AEStronglyMeasurable.smul` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `MeasureTheory.aestronglyMeasurable_const` `MeasureTheory.AEStronglyMeasurable.sub` `instIsTopologicalAddGroupReal` `AEMeasurable.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Measurable.comp_aemeasurable'` `Continuous.measurable` `continuous` `AEMeasurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `aemeasurable_id'` `Measurable.aestronglyMeasurable` `MeasureTheory.Integrable.aestronglyMeasurable` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `self_mem_nhdsWithin` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `Real.instIsOrderedAddMonoid` `LT.lt.le` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `norm_sub_le` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `add_sub_cancel_left` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_nonneg` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `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` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `MeasureTheory.Integrable.const_mul` `MeasureTheory.Integrable.norm` `ae_lineDifferentiableAt` `Filter.Tendsto.mul` `HasLineDerivAt.tendsto_slope_zero_right` `LineDifferentiableAt.hasLineDerivAt` `tendsto_const_nhds`
`integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace` `HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `Continuous` `Real.pseudoMetricSpace`	`Filter.Tendsto` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.instMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instInv` `Real.instSub` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `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` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `nhdsWithin` `Set.Ioi` `Real.instPreorder` `nhds` `lineDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup`	—	`IsCompact.cthickening` `FiniteDimensional.proper_real` `MeasureTheory.tendsto_integral_filter_of_dominated_convergence` `TopologicalSpace.isCountablyGenerated_nhdsWithin` `FirstCountableTopology.nhds_generated_countable` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.univ_mem'` `MeasureTheory.AEStronglyMeasurable.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.AEStronglyMeasurable.smul` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `MeasureTheory.aestronglyMeasurable_const` `MeasureTheory.AEStronglyMeasurable.sub` `instIsTopologicalAddGroupReal` `AEMeasurable.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Measurable.comp_aemeasurable'` `Continuous.measurable` `continuous` `AEMeasurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `aemeasurable_id'` `Measurable.aestronglyMeasurable` `Continuous.aestronglyMeasurable` `secondCountableTopologyEither_of_right` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Ioc_mem_nhdsGT` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `LT.lt.le` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `norm_sub_le` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `add_sub_cancel_left` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_nonneg` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `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` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Set.indicator_of_mem` `Function.notMem_support` `Mathlib.Tactic.Contrapose.contrapose₄` `Metric.self_subset_cthickening` `subset_tsupport` `Metric.mem_cthickening_of_dist_le` `dist_eq_norm` `sub_add_cancel_left` `norm_neg` `mul_le_of_le_one_left` `sub_self` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `norm_zero` `Set.indicator_nonneg` `mul_nonneg` `NNReal.coe_nonneg` `MeasureTheory.integrable_indicator_iff` `IsCompact.measurableSet` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousOn.integrableOn_compact` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `ContinuousOn.fun_mul` `continuousOn_const` `ContinuousOn.norm` `Continuous.continuousOn` `ae_lineDifferentiableAt` `Filter.Tendsto.mul` `HasLineDerivAt.tendsto_slope_zero_right` `LineDifferentiableAt.hasLineDerivAt` `tendsto_const_nhds`
`integral_lineDeriv_mul_eq` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace` `HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.instMul` `lineDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `continuous` `integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'` `MeasureTheory.integral_add_right_eq_self` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.IsAddLeftInvariant.isAddRightInvariant` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `smul_neg` `neg_add_cancel_right` `sub_mul` `mul_sub` `MeasureTheory.integral_sub` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.comp` `continuous_add_right` `HasCompactSupport.mul_left` `HasCompactSupport.comp_homeomorph` `mul_assoc` `MeasureTheory.integral_const_mul` `mul_comm` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nhdsGT_neBot` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`locallyIntegrable_lineDeriv` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `lineDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	—	`MeasureTheory.MemLp.locallyIntegrable` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `memLp_lineDeriv` `le_top`
`memLp_lineDeriv` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Real.metricSpace`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `lineDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Top.top` `ENNReal` `instTopENNReal`	—	`MeasureTheory.memLp_top_of_bound` `aestronglyMeasurable_lineDeriv` `locallyCompact_of_proper` `instProperSpaceReal` `BorelSpace.opensMeasurable` `Real.instCompleteSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `continuous` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `norm_lineDeriv_le_of_lipschitz`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_differentiableAt_norm` 📖	mathematical	—	`Filter.Eventually` `DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`LipschitzWith.ae_differentiableAt` `FiniteDimensional.rclike_to_real` `lipschitzWith_one_norm`
`dense_differentiableAt_norm` 📖	mathematical	—	`Dense` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `setOf` `DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`MeasureTheory.Measure.dense_of_ae` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `isAddHaarMeasure_basis_addHaar` `ae_differentiableAt_norm`

---

← Back to Index