Besicovitch.exists_goodδ
theorem Besicovitch.exists_goodδ :
∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
∃ δ,
0 < δ ∧
δ < 1 ∧
∀ (s : Finset E),
(∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) → s.card ≤ Besicovitch.multiplicity E
This theorem, named `Besicovitch.exists_goodδ`, states that for any finite-dimensional normed space `E` over the real numbers, there exists a positive number `δ` less than 1, such that for any finite set `s` in `E` where each element `c` has a norm less than or equal to 2, and for any distinct elements `c` and `d` in `s` the norm of the difference between `c` and `d` is at least `1 - δ`, the cardinality of `s` is less than or equal to the Besicovitch multiplicity of `E`. The Besicovitch multiplicity of a space is defined as the supremum of the sizes of `1`-separated sets in the ball of radius `2`.
More concisely: For any finite-dimensional real normed space, there exists a constant `δ` less than 1 such that any finite subset of the space with elements of norm less than or equal to 2 and pairwise distance greater than `1 - δ` has cardinality less than or equal to the Besicovitch multiplicity of the space.
|
Besicovitch.card_le_of_separated
theorem Besicovitch.card_le_of_separated :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
(s : Finset E),
(∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) → s.card ≤ 5 ^ FiniteDimensional.finrank ℝ E
The theorem `Besicovitch.card_le_of_separated` states that for any finite set 's' in a real normed, finite-dimensional space 'E', if all elements in 's' have a norm less than or equal to 2 and any two distinct elements in 's' have a norm difference equal to or more than 1, then the cardinality (or size) of the set 's' is less than or equal to 5 raised to the power of the dimension of the vector space 'E'. This theorem is useful to show that the supremum in the definition of `Besicovitch.multiplicity E` is well-behaved.
More concisely: If a finite set in a real normed, finite-dimensional space satisfies the condition that every element has norm less than or equal to 2 and any distinct elements have norm difference greater than or equal to 1, then its cardinality is bounded by 5 raised to the power of the dimension.
|
Besicovitch.isEmpty_satelliteConfig_multiplicity
theorem Besicovitch.isEmpty_satelliteConfig_multiplicity :
∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
IsEmpty (Besicovitch.SatelliteConfig E (Besicovitch.multiplicity E) (Besicovitch.goodτ E))
The theorem `Besicovitch.isEmpty_satelliteConfig_multiplicity` asserts that in any normed vector space `E`, there cannot exist a satellite configuration with a number of points equal to the multiplicity of `E` plus one and the parameter set to `goodτ E`. This result ensures that during the inductive construction of the Besicovitch covering families, we never encounter more than `multiplicity E` nonempty families. Here, the `multiplicity E` refers to the maximum cardinality of a set in the ball of radius `2` where each point in the set is at least distance `1` apart from each other, and `goodτ E` is a number slightly greater than `1`, specifically chosen to minimize the number of covering families in the Besicovitch covering theorem.
More concisely: In any normed vector space, there can be no configuration of more than the multiplicity + 1 points with pairwise distance greater than 1 and contained in a ball of radius 2.
|