Theorems · Inductive type · measure theory

Besicovitch.SatelliteConfig

(α : Type u_1) → [MetricSpace α] → ℕ → ℝ → Type u_1

A satellite configuration is a configuration of N+1 points that shows up in the inductive construction for the Besicovitch covering theorem. It depends on some parameter τ ≥ 1. This is a family of balls (indexed by i : Fin N.succ, with center c i and radius r i) such that the last ball intersects all the other balls (condition inter), and given any two balls there is an order between them, ensuring that the first ball does not contain the center of the other one, and the radius of the second ball cannot be larger than the radius of the first ball (up to a factor τ). This order corresponds to the order of choice in the inductive construction: otherwise, the second ball would have been chosen before. This is the condition h. Finally, the last ball is chosen after all the other ones, meaning that h can be strengthened by keeping only one side of the alternative in hlast.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

23 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

MetricSpace