Documentation Verification Report

DensityTheorem

📁 Source: Mathlib/MeasureTheory/Covering/DensityTheorem.lean

Statistics

Metric	Count
Definitions `vitaliFamily`	1
Theorems `ae_tendsto_average`, `ae_tendsto_average_norm_sub`, `ae_tendsto_measure_inter_div`, `closedBall_mem_vitaliFamily_of_dist_le_mul`, `tendsto_closedBall_filterAt`, `vitaliFamily_def`	6
Total	7

IsUnifLocDoublingMeasure

Definitions

Name	Category	Theorems
`vitaliFamily` 📖	CompOp	7 math math: `Real.Icc_mem_vitaliFamily_at_left`, `closedBall_mem_vitaliFamily_of_dist_le_mul`, `Real.tendsto_Icc_vitaliFamily_left`, `tendsto_closedBall_filterAt`, `Real.Icc_mem_vitaliFamily_at_right`, `vitaliFamily_def`, `Real.tendsto_Icc_vitaliFamily_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_tendsto_average` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `VitaliFamily.ae_tendsto_average` `Filter.univ_mem'` `Filter.Tendsto.comp` `tendsto_closedBall_filterAt`
`ae_tendsto_average_norm_sub` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `VitaliFamily.ae_tendsto_average_norm_sub` `Filter.univ_mem'` `Filter.Tendsto.comp` `tendsto_closedBall_filterAt`
`ae_tendsto_measure_inter_div` 📖	mathematical	—	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `VitaliFamily.ae_tendsto_measure_inter_div` `Filter.univ_mem'` `Filter.Tendsto.comp` `tendsto_closedBall_filterAt`
`closedBall_mem_vitaliFamily_of_dist_le_mul` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `VitaliFamily.setsAt` `vitaliFamily` `Metric.closedBall`	—	`Nat.instAtLeastTwoHAddOfNat` `vitaliFamily_def` `Set.Nonempty.mono` `Metric.ball_subset_interior_closedBall` `Metric.nonempty_ball` `BorelSpace.opensMeasurable` `le_or_gt` `Metric.closedBall_subset_closedBall'` `dist_comm` `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.mul_congr` `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.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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `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` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Metric.closedBall_subset_closedBall` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_max_left` `LT.lt.le` `LE.le.trans` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `HasSubset.Subset.trans` `Set.instIsTransSubset` `measure_mul_le_scalingConstantOf_mul` `LT.lt.trans_le` `zero_lt_three` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_max_right` `le_rfl` `Metric.mem_closedBall_self` `Metric.mem_closedBall'` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true` `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` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `CancelDenoms.add_subst` `CancelDenoms.mul_subst` `le_mul_of_one_le_left` `ENNReal.instIsOrderedRing` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.one_le_coe_iff` `exists_eventually_forall_measure_closedBall_le_mul`
`tendsto_closedBall_filterAt` 📖	mathematical	`Filter.Tendsto` `Real` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `Filter.Eventually` `Set` `Set.instMembership` `Metric.closedBall` `Real.instMul`	`VitaliFamily.filterAt` `vitaliFamily`	—	`VitaliFamily.tendsto_filterAt_iff` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `closedBall_mem_vitaliFamily_of_dist_le_mul` `Filter.eq_or_neBot` `Filter.Eventually.exists` `Filter.Eventually.and` `Metric.nonempty_closedBall` `mul_nonneg_iff_left_nonneg_of_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `Set.mem_Ioi` `eventually_mem_of_tendsto_nhdsWithin` `tendsto_nhds_of_tendsto_nhdsWithin` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Filter.Eventually.mono` `Metric.tendsto_nhds` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `dist_zero_right` `abs_eq_self` `LT.lt.le` `lt_div_iff₀'` `le_of_not_gt` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `dist_triangle_right`
`vitaliFamily_def` 📖	mathematical	—	`vitaliFamily`	—	—

---

← Back to Index