OAI/NumberTheory/Ostmann/Characters/CharacterBandGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The three selected prime bands give all character separation parameters

  1. def OAI.Ostmann.characterBandPoint line 8
  2. theorem OAI.Ostmann.characterBandPoint_strictMono line 11
  3. theorem OAI.Ostmann.characterBandPoint_bounds line 18
  4. theorem OAI.Ostmann.character_three_band_margins line 33

    Source documentation

    Midpoints of the unused partition gaps satisfy the strict margins required by both the anchor and nonanchor energy comparisons.

    theorem character_three_band_margins (α β : ℝ) (q : ℕ) (hα : 0 < α) (hαβ : α < β)
    (hq : 0 < q) (i j k : Fin q) (hij : i.val + 1 < j.val) (hjk : j.val + 1 < k.val) :
    let γs := characterBandPoint α β q (i.val + 1)
…

    Mentions: OAI.Ostmann.characterBandPoint