OAI/NumberTheory/Ostmann/Characters/CharacterIntervalGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constructed character targets satisfy the two integer transfer inequalities

  1. def OAI.Ostmann.characterRangeError line 10
  2. theorem OAI.Ostmann.eventual_character_interval_geometry line 15

    Source documentation

    The threshold is uniform in the selected word bin, anchors and target centers. Only the fixed depth and bounded cell errors enter it.

    theorem eventual_character_interval_geometry (k : ℕ) (B z c : ℝ)
    (hB : 0 ≤ B) (hz : 1 ≤ z) (hc : 0 ≤ c) :
    ∀ᶠ m : ℝ in atTop, ∀ J : ℝ, ∀ a : Fin k → Bool → ℝ, ∀ F : ℝ,
    let Δ := fun j : Fin k => characterPivotGap B z m j.val
…

    Mentions: OAI.Ostmann.characterPivotGap