Documentation Verification Report

Doubling

📁 Source: Mathlib/MeasureTheory/Measure/Doubling.lean

Statistics

Metric	Count
Definitions `IsUnifLocDoublingMeasure`, `doublingConstant`, `scalingConstantOf`, `scalingScaleOf`	4
Theorems `eventually_measure_le_doublingConstant_mul`, `eventually_measure_le_scaling_constant_mul`, `eventually_measure_le_scaling_constant_mul'`, `eventually_measure_mul_le_scalingConstantOf_mul`, `exists_eventually_forall_measure_closedBall_le_mul`, `exists_measure_closedBall_le_mul`, `exists_measure_closedBall_le_mul'`, `exists_measure_closedBall_le_mul''`, `measure_mul_le_scalingConstantOf_mul`, `one_le_scalingConstantOf`, `scalingScaleOf_pos`	11
Total	15

IsUnifLocDoublingMeasure

Definitions

Name	Category	Theorems
`doublingConstant` 📖	CompOp	—
`scalingConstantOf` 📖	CompOp	3 math math: `eventually_measure_mul_le_scalingConstantOf_mul`, `measure_mul_le_scalingConstantOf_mul`, `one_le_scalingConstantOf`
`scalingScaleOf` 📖	CompOp	1 math math: `scalingScaleOf_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_measure_le_doublingConstant_mul` 📖	mathematical	—	`Filter.Eventually` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_measure_closedBall_le_mul`
`eventually_measure_le_scaling_constant_mul` 📖	mathematical	—	`Filter.Eventually` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder`	—	`Filter.mp_mem` `exists_eventually_forall_measure_closedBall_le_mul` `Filter.univ_mem'` `le_imp_le_of_le_of_le` `le_rfl` `le_refl` `scalingConstantOf.eq_1` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.coe_le_coe_of_le` `le_max_left`
`eventually_measure_le_scaling_constant_mul'` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Eventually` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.Ioi` `Real.instPreorder`	—	`inv_mul_cancel_left₀` `LT.lt.ne'` `eventually_nhdsGT_zero_mul_left` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `eventually_measure_le_scaling_constant_mul`
`eventually_measure_mul_le_scalingConstantOf_mul` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.closedBall` `Real.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `scalingConstantOf`	—	`exists_eventually_forall_measure_closedBall_le_mul` `mem_nhdsGT_iff_exists_Ioc_subset` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_trichotomy` `mul_neg_of_pos_of_neg` `Metric.closedBall_eq_empty` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.instCanonicallyOrderedAdd` `MulZeroClass.mul_zero` `le_mul_of_one_le_of_le` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.one_le_coe_iff` `le_max_right` `le_rfl` `LE.le.trans` `mul_le_mul_left` `ENNReal.coe_le_coe_of_le` `le_max_left`
`exists_eventually_forall_measure_closedBall_le_mul` 📖	mathematical	—	`Filter.Eventually` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_zero` `one_mul` `eventually_nhdsGT_zero_mul_left` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `two_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Filter.mp_mem` `eventually_measure_le_doublingConstant_mul` `Filter.univ_mem'` `pow_succ` `mul_assoc` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `pow_unbounded_of_one_lt` `Real.instArchimedean` `AddGroup.existsAddOfLE` `one_lt_two` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `eventually_mem_nhdsWithin` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Metric.closedBall_subset_closedBall` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_of_lt` `Set.mem_Ioi` `ENNReal.coe_pow`
`exists_measure_closedBall_le_mul` 📖	mathematical	—	`Filter.Eventually` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder`	—	`exists_measure_closedBall_le_mul''`
`exists_measure_closedBall_le_mul'` 📖	mathematical	—	`Filter.Eventually` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder`	—	`eventually_measure_le_doublingConstant_mul`
`exists_measure_closedBall_le_mul''` 📖	mathematical	—	`Filter.Eventually` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder`	—	—
`measure_mul_le_scalingConstantOf_mul` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder` `Real.instZero` `Real.instLE` `scalingScaleOf`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Metric.closedBall` `Real.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `scalingConstantOf`	—	`eventually_measure_mul_le_scalingConstantOf_mul`
`one_le_scalingConstantOf` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `scalingConstantOf`	—	`le_max_of_le_right` `exists_eventually_forall_measure_closedBall_le_mul` `le_refl`
`scalingScaleOf_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `scalingScaleOf`	—	`eventually_measure_mul_le_scalingConstantOf_mul`

(root)

Definitions

Name	Category	Theorems
`IsUnifLocDoublingMeasure` 📖	CompData	4 math math: `MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure`, `MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod`, `AddCircle.instIsUnifLocDoublingMeasureRealVolume`, `IsUnifLocDoublingMeasure.prod`

---

← Back to Index