OAI/NumberTheory/Ostmann/Characters/CharacterCellCovering.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One fixed covering error for every selected character-cell list

  1. def OAI.Ostmann.characterCellCoveringError line 10
  2. theorem OAI.Ostmann.characterCellCoveringError_gt_one line 13
  3. theorem OAI.Ostmann.character_selected_cell_size_le line 20
  4. theorem OAI.Ostmann.character_selected_product_intervals line 35

    Source documentation

    Neither the selected endpoint nor the number of labels creates another range hypothesis: the explicit uniform covering error bounds every group.

    theorem character_selected_product_intervals {P : Finset ℕ} {F : ℕ → ℂ}
    {c δ U : ℝ} {k : ℕ} {T : Option (Fin k) → ℝ}
    (w : ∀ j, CharacterTargetWord P F c δ U k (T j))
    (a : Fin k → Bool → ℕ) (J : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
    let E := characterCellCoveringError c δ k
…

    Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.characterCellCoveringError