English
In a normed vector space, there is no satellite configuration with multiplicity points (i.e., more than multiplicity(E) points) for the given τ.
Русский
В нормированном векторном пространстве не существует спутниковой конфигурации с более чем multiplicity(E) точками при заданном τ.
LaTeX
$$$$IsEmpty\\; (SatelliteConfig\\; E\\ (multiplicity\\; E)\\ (goodτ\\; E))$$$$
Lean4
/-- In a normed vector space `E`, there can be no satellite configuration with `multiplicity E + 1`
points and the parameter `goodτ E`. This will ensure that in the inductive construction to get
the Besicovitch covering families, there will never be more than `multiplicity E` nonempty
families. -/
theorem isEmpty_satelliteConfig_multiplicity : IsEmpty (SatelliteConfig E (multiplicity E) (goodτ E)) :=
⟨by
intro a
let b := a.centerAndRescale
rcases
b.exists_normalized a.centerAndRescale_center a.centerAndRescale_radius (one_lt_goodτ E).le (goodδ E) le_rfl
(goodδ_lt_one E).le with
⟨c', c'_le_two, hc'⟩
exact lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))⟩
