OAI/NumberTheory/Ostmann/Characters/CharacterFixedParameters.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One gap choice and one depth threshold for every selected prime band

  1. theorem OAI.Ostmann.exists_character_fixed_parameters line 10

    Source documentation

    All rates here precede the finite choice of the three bands and the rich block depth. The number of cells affects only the later large-L threshold.

    theorem exists_character_fixed_parameters (a β c δ Ctotal C₀ : ℝ)
    (hβ : 0 < β) (hc : 0 < c) (hδ : 0 < δ) (hδ1 : δ ≤ 1)
    (hC₀ : 0 < C₀) (Kmin : ℕ) :
    let Aend := 8 * β + 10
…