Documentation Verification Report

Besicovitch

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

Statistics

Metric	Count
Definitions `BallPackage`, `c`, `instInhabited`, `r`, `r_bound`, `SatelliteConfig`, `c`, `instInhabited`, `r`, `TauPackage`, `R`, `color`, `iUnionUpTo`, `index`, `instInhabited`, `lastStep`, `toBallPackage`, `τ`, `unitBallPackage`, `vitaliFamily`, `HasBesicovitchCovering`, `evalBesicovitchSatelliteConfigR`	22
Theorems `r_le`, `rpos`, `h`, `hlast`, `hlast'`, `inter`, `inter'`, `rpos`, `color_lt`, `lastStep_nonempty`, `mem_iUnionUpTo_lastStep`, `monotone_iUnionUpTo`, `one_lt_tau`, `ae_tendsto_measure_inter_div`, `ae_tendsto_measure_inter_div_of_measurableSet`, `ae_tendsto_rnDeriv`, `exist_disjoint_covering_families`, `exist_finset_disjoint_balls_large_measure`, `exists_closedBall_covering_tsum_measure_le`, `exists_disjoint_closedBall_covering_ae`, `exists_disjoint_closedBall_covering_ae_aux`, `exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux`, `tendsto_filterAt`, `no_satelliteConfig`	24
Total	46

Besicovitch

Definitions

Name	Category	Theorems
`BallPackage` 📖	CompData	—
`SatelliteConfig` 📖	CompData	2 math math: `HasBesicovitchCovering.no_satelliteConfig`, `isEmpty_satelliteConfig_multiplicity`
`TauPackage` 📖	CompData	—
`unitBallPackage` 📖	CompOp	—
`vitaliFamily` 📖	CompOp	1 math math: `tendsto_filterAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_tendsto_measure_inter_div` 📖	mathematical	—	`Filter.Eventually` `Filter.Tendsto` `Real` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `BorelSpace.opensMeasurable` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `VitaliFamily.ae_tendsto_measure_inter_div` `Filter.univ_mem'` `Filter.Tendsto.comp` `tendsto_filterAt`
`ae_tendsto_measure_inter_div_of_measurableSet` 📖	mathematical	`MeasurableSet`	`Filter.Eventually` `Filter.Tendsto` `Real` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `BorelSpace.opensMeasurable` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet` `Filter.univ_mem'` `Filter.Tendsto.comp` `tendsto_filterAt`
`ae_tendsto_rnDeriv` 📖	mathematical	—	`Filter.Eventually` `Filter.Tendsto` `Real` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.rnDeriv` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `BorelSpace.opensMeasurable` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `VitaliFamily.ae_tendsto_rnDeriv` `Filter.univ_mem'` `Filter.Tendsto.comp` `tendsto_filterAt`
`exist_disjoint_covering_families` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `BallPackage.c` `BallPackage.r` `Set.instHasSubset` `Set.range` `Set.iUnion` `Set.instMembership` `Metric.ball`	—	`isEmpty_or_nonempty` `Set.pairwiseDisjoint_empty` `Set.image_univ` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype` `Set.image_empty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.instReflSubset` `lt_or_eq_of_le` `TauPackage.color.eq_1` `csInf_mem` `instWellFoundedLTNat` `LT.lt.ne'` `TauPackage.color_lt` `LT.lt.trans` `Mathlib.Tactic.Contrapose.contrapose₁` `Disjoint.symm` `le_of_not_ge` `Set.range_subset_iff` `TauPackage.mem_iUnionUpTo_lastStep` `Set.iUnion_exists` `Set.biUnion_and'`
`exist_finset_disjoint_balls_large_measure` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instZero` `Real.instLE`	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `Finset.instMembership` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Distrib.toAdd` `AddMonoidWithOne.toOne` `Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`le_or_gt` `le_bot_iff` `Finset.coe_empty` `Set.iUnion_congr_Prop` `Set.iUnion_false` `Set.iUnion_empty` `Set.diff_empty` `MulZeroClass.mul_zero` `ENNReal.instCanonicallyOrderedAdd` `isEmpty_or_nonempty` `lt_irrefl` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `not_isEmpty_of_nonempty` `MeasureTheory.exists_measurable_superset` `exist_disjoint_covering_families` `Set.PairwiseDisjoint.countable_of_nonempty_interior` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Metric.nonempty_ball` `BallPackage.rpos` `Set.Nonempty.mono` `Metric.ball_subset_interior_closedBall` `Set.Subset.antisymm` `Subtype.range_coe_subtype` `Set.mem_iUnion` `Subtype.coe_eta` `Metric.ball_subset_closedBall` `Set.iUnion_subset` `Set.inter_subset_left` `Finset.sum_const` `Finset.card_fin` `nsmul_eq_mul` `ENNReal.mul_div_cancel` `ENNReal.instCharZero` `ENNReal.natCast_ne_top` `MeasureTheory.measure_iUnion_fintype_le` `ENNReal.exists_le_of_sum_le` `bot_lt_iff_ne_bot` `Finset.mem_univ` `lt_of_lt_of_le` `ENNReal.mul_lt_mul_iff_right` `LT.lt.ne'` `MeasureTheory.measure_ne_top` `ENNReal.inv_lt_inv` `add_zero` `ENNReal.add_lt_add_left` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `Set.inter_iUnion` `MeasureTheory.measure_biUnion` `Set.PairwiseDisjoint.mono` `Set.inter_subset_right` `MeasurableSet.inter` `measurableSet_closedBall` `Summable.hasSum` `ENNReal.summable` `LT.lt.trans_le` `MeasureTheory.measure_mono` `Set.inter_subset_inter_left` `Filter.Eventually.exists` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `tendsto_order` `ENNReal.instOrderTopology` `Finset.coe_image` `Set.diff_inter_self_eq_diff` `MeasureTheory.measure_diff_le_iff_le_add` `MeasureTheory.NullMeasurableSet.inter` `Finset.nullMeasurableSet_biUnion` `MeasurableSet.nullMeasurableSet` `add_mul` `Distrib.rightDistribClass` `ENNReal.div_add_div_same` `add_comm` `ENNReal.div_self` `Unique.instSubsingleton` `one_mul` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `one_div` `mul_comm` `div_eq_mul_inv` `LE.le.trans` `LT.lt.le` `le_of_eq` `Finset.set_biUnion_coe` `Set.inter_comm` `Set.inter_iUnion₂` `MeasureTheory.measure_biUnion_finset` `Subtype.val_injective` `Finset.set_biUnion_finset_image` `le_trans` `Set.diff_subset_diff` `Set.Subset.refl`
`exists_closedBall_covering_tsum_measure_le` 📖	mathematical	`Set.Nonempty` `Real` `Set` `Set.instInter` `Set.Ioo` `Real.instPreorder` `Real.instZero`	`Set.Countable` `Set.instHasSubset` `Set.instMembership` `Set.iUnion` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `Set.Elem` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `SummationFilter.unconditional` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.exists_isOpen_le_add` `Metric.mem_nhds_iff` `IsOpen.mem_nhds` `exists_disjoint_closedBall_covering_ae` `Set.diff_subset` `HasBesicovitchCovering.no_satelliteConfig` `lt_min` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `LT.lt.trans_le` `min_le_right` `Set.Subset.trans` `Metric.closedBall_subset_ball` `min_le_left` `LT.lt.le` `exist_disjoint_covering_families` `Set.PairwiseDisjoint.countable_of_nonempty_interior` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Metric.nonempty_ball` `BallPackage.rpos` `Set.Nonempty.mono` `Metric.ball_subset_interior_closedBall` `dist_self` `Set.Countable.union` `Set.countable_iUnion` `instCountableFin` `Set.Countable.image` `Subtype.range_coe_subtype` `Set.mem_iUnion₂` `Metric.ball_subset_closedBall` `MeasureTheory.measure_iUnion` `Encodable.countable` `pairwise_subtype_iff_pairwise_set` `measurableSet_closedBall` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.Injective.injOn` `Subtype.val_injective` `Set.InjOn.bijOn_image` `Equiv.tsum_eq` `zero_add` `ENNReal.tsum_union_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_rfl` `ENNReal.tsum_iUnion_le` `Finset.sum_le_sum` `add_le_add_right` `Finset.sum_const` `Finset.card_fin` `nsmul_eq_mul` `add_assoc` `ENNReal.add_halves` `Function.sometimes_spec`
`exists_disjoint_closedBall_covering_ae` 📖	mathematical	`Set.Nonempty` `Real` `Set` `Set.instInter` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instLT`	`Set.Countable` `Set.instHasSubset` `Set.instMembership` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `instZeroENNReal` `Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`lt_min` `LT.lt.trans_le` `min_le_right` `min_le_left` `exists_disjoint_closedBall_covering_ae_aux` `LT.lt.le` `Set.exists_eq_graphOn` `Set.Pairwise.eq` `Set.not_disjoint_iff` `dist_self` `Set.LeftInvOn.injOn` `Set.countable_of_injective_of_countable_image` `Set.biUnion_image` `Set.iUnion_congr_Prop` `Set.InjOn.pairwiseDisjoint_image`
`exists_disjoint_closedBall_covering_ae_aux` 📖	mathematical	`Set.Nonempty` `Real` `Set` `Set.instInter` `Set.Ioo` `Real.instPreorder` `Real.instZero`	`Set.Countable` `Set.instMembership` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `instZeroENNReal` `Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous` `exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux`
`exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux` 📖	mathematical	`Set.Nonempty` `Real` `Set` `Set.instInter` `Set.Ioo` `Real.instPreorder` `Real.instZero`	`Set.Countable` `Set.instMembership` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instSDiff` `Set.iUnion` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `instZeroENNReal` `Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`HasBesicovitchCovering.no_satelliteConfig` `isClosed_biUnion_finset` `Metric.isClosed_closedBall` `Set.mem_diff` `Set.eq_empty_or_nonempty` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_min` `IsClosed.notMem_iff_infDist_pos` `LT.lt.trans_le` `min_le_right` `disjoint_comm` `Metric.disjoint_closedBall_of_lt_infDist` `min_le_left` `exist_finset_disjoint_balls_large_measure` `LT.lt.le` `Finset.subset_union_left` `Finset.coe_union` `Finset.coe_image` `Set.mem_image` `Set.disjoint_of_subset_left` `Finset.set_biUnion_coe` `Set.subset_biUnion_of_mem` `Finset.mem_union` `Finset.mem_image` `Finset.mem_coe` `Finset.set_biUnion_union` `Set.diff_diff` `Finset.set_biUnion_finset_image` `Function.sometimes_spec` `Function.iterate_succ'` `Finset.coe_empty` `instIsEmptyFalse` `Set.countable_iUnion` `instCountableNat` `Finset.countable_toSet` `Set.mem_iUnion` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.diff_subset_diff` `subset_refl` `Set.instReflSubset` `Set.biUnion_subset_biUnion_left` `Set.subset_iUnion` `Set.iUnion_congr_Prop` `Set.iUnion_false` `Set.iUnion_empty` `Set.diff_empty` `pow_zero` `one_mul` `pow_succ'` `mul_assoc` `le_imp_le_of_le_of_le` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_refl` `ENNReal.Tendsto.mul_const` `ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one` `ENNReal.div_lt_iff` `Unique.instSubsingleton` `ENNReal.instCharZero` `ENNReal.Finiteness.add_ne_top` `ENNReal.natCast_ne_top` `ENNReal.one_ne_top` `add_zero` `ENNReal.add_lt_add_left` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `LT.lt.ne` `MeasureTheory.measure_lt_top` `le_bot_iff` `le_of_tendsto_of_tendsto'` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_const_nhds` `MulZeroClass.zero_mul` `LE.le.trans` `Set.pairwiseDisjoint_iUnion` `Monotone.directed_le` `monotone_nat_of_le_succ`
`tendsto_filterAt` 📖	mathematical	—	`Filter.Tendsto` `Real` `Set` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `VitaliFamily.filterAt` `vitaliFamily`	—	`VitaliFamily.mem_filterAt_iff` `Filter.mp_mem` `Ioc_mem_nhdsGT` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.univ_mem'` `Set.mem_image_of_mem` `Metric.closedBall_subset_closedBall`

Besicovitch.BallPackage

Definitions

Name	Category	Theorems
`c` 📖	CompOp	3 math math: `Besicovitch.exist_disjoint_covering_families`, `Besicovitch.TauPackage.mem_iUnionUpTo_lastStep`, `Besicovitch.TauPackage.lastStep_nonempty`
`instInhabited` 📖	CompOp	—
`r` 📖	CompOp	4 math math: `Besicovitch.exist_disjoint_covering_families`, `r_le`, `rpos`, `Besicovitch.TauPackage.lastStep_nonempty`
`r_bound` 📖	CompOp	1 math math: `r_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`r_le` 📖	mathematical	—	`Real` `Real.instLE` `r` `r_bound`	—	—
`rpos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `r`	—	—

Besicovitch.SatelliteConfig

Definitions

Name	Category	Theorems
`c` 📖	CompOp	6 math math: `hlast`, `h`, `inter'`, `centerAndRescale_center`, `exists_normalized_aux1`, `inter`
`instInhabited` 📖	CompOp	—
`r` 📖	CompOp	7 math math: `hlast'`, `centerAndRescale_radius`, `hlast`, `h`, `rpos`, `inter'`, `inter`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`h` 📖	mathematical	—	`Pairwise` `Real` `Real.instLE` `r` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `c` `Real.instMul`	—	—
`hlast` 📖	mathematical	—	`Real` `Real.instLE` `r` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `c` `Real.instMul`	—	—
`hlast'` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`r` `Real.instMul`	—	`lt_or_ge` `hlast` `top_le_iff` `le_mul_of_one_le_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `LT.lt.le` `rpos`
`inter` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `c` `Real.instAdd` `r`	—	—
`inter'` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `c` `Real.instAdd` `r`	—	`lt_or_ge` `inter` `top_le_iff` `LT.lt.le` `rpos` `dist_self` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`rpos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `r`	—	—

Besicovitch.TauPackage

Definitions

Name	Category	Theorems
`R` 📖	CompOp	1 math math: `lastStep_nonempty`
`color` 📖	CompOp	1 math math: `color_lt`
`iUnionUpTo` 📖	CompOp	3 math math: `monotone_iUnionUpTo`, `mem_iUnionUpTo_lastStep`, `lastStep_nonempty`
`index` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`lastStep` 📖	CompOp	1 math math: `mem_iUnionUpTo_lastStep`
`toBallPackage` 📖	CompOp	2 math math: `mem_iUnionUpTo_lastStep`, `lastStep_nonempty`
`τ` 📖	CompOp	2 math math: `one_lt_tau`, `lastStep_nonempty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`color_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `lastStep`	`color`	—	`Ordinal.induction` `color.eq_1` `LT.lt.ne'` `LT.lt.trans` `Nat.notMem_of_lt_sInf` `LE.le.eq_or_lt` `color.congr_simp` `LT.lt.ne` `index.eq_1` `notMem_of_lt_csInf` `OrderBot.bddBelow` `dist_comm` `le_trans` `monotone_iUnionUpTo` `LT.lt.le` `le_ciSup` `Besicovitch.BallPackage.r_le` `Besicovitch.BallPackage.rpos` `LE.le.lt_or_eq` `Fin.val_injective` `le_of_not_ge` `Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall` `IsEmpty.false` `Function.sometimes_spec` `csInf_le`
`lastStep_nonempty` 📖	mathematical	—	`Set.Nonempty` `Ordinal` `setOf` `Set` `Set.instMembership` `iUnionUpTo` `Besicovitch.BallPackage.c` `toBallPackage` `Real` `Real.instLE` `R` `Real.instMul` `τ` `Besicovitch.BallPackage.r`	—	`eq_or_lt_of_le` `index.eq_1` `dist_self` `lt_irrefl` `LT.lt.trans_le` `Besicovitch.BallPackage.rpos` `le_of_not_ge` `not_injective_of_ordinal` `UnivLE.small` `UnivLE.self`
`mem_iUnionUpTo_lastStep` 📖	mathematical	—	`Set` `Set.instMembership` `iUnionUpTo` `lastStep` `Besicovitch.BallPackage.c` `toBallPackage`	—	`csInf_mem` `Ordinal.wellFoundedLT` `lastStep_nonempty` `lt_trans` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_lt_tau` `Besicovitch.BallPackage.rpos` `one_mul` `mul_lt_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `inv_lt_one_of_one_lt₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `le_rfl` `zero_le_one` `exists_lt_of_lt_csSup` `Set.image_univ` `Set.image_nonempty` `Set.mem_univ` `div_le_iff₀'` `LT.lt.le` `div_eq_inv_mul` `lt_irrefl` `LT.lt.trans_le`
`monotone_iUnionUpTo` 📖	mathematical	—	`Monotone` `Ordinal` `Set` `PartialOrder.toPreorder` `Ordinal.partialOrder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `iUnionUpTo`	—	`Set.iUnion_mono'` `LT.lt.trans_le` `Set.Subset.rfl`
`one_lt_tau` 📖	mathematical	—	`Real` `Real.instLT` `Real.instOne` `τ`	—	—

HasBesicovitchCovering

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`no_satelliteConfig` 📖	mathematical	—	`Real` `Real.instLT` `Real.instOne` `IsEmpty` `Besicovitch.SatelliteConfig`	—	—

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalBesicovitchSatelliteConfigR` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`HasBesicovitchCovering` 📖	CompData	1 math math: `Besicovitch.instHasBesicovitchCovering`

---

← Back to Index