Theorems · Theorem · measure theory

Besicovitch.SatelliteConfig.exists_normalized

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ),
  a.c (Fin.last N) = 0 →
    a.r (Fin.last N) = 1 →
      1 ≤ τ →
        ∀ (δ : ℝ),
          τ ≤ 1 + δ / 4 → δ ≤ 1 → ∃ c', (∀ (n : Fin N.succ), ‖c' n‖ ≤ 2) ∧ Pairwise fun i j => 1 - δ ≤ ‖c' i - c' j‖

Defined in

Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Cited by

1 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace