OAI/Analysis/Unitarizability/SphereNet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quarter-nets and their cardinality bounds. Volume comparison with radii 1/8 and 9/8 gives the constant 9^m.

  1. theorem OAI.Dixmier.SphereNet.quarter_separated_card line 18
  2. theorem OAI.Dixmier.SphereNet.exists_quarter_net line 56

    Source documentation

    A quarter-net with all centers on the unit sphere and at most 9^dim centers.

    theorem exists_quarter_net : ∃ s : Finset E,
    (∀ x ∈ s, ‖x‖ = 1) ∧ s.card ≤ 9 ^ finrank ℝ E ∧
      ∀ x : E, ‖x‖ = 1 → ∃ y ∈ s, ‖x-y‖ ≤ (1/4 : ℝ) := by
…