OAI/NumberTheory/Ostmann/Characters/CharacterSelectionScales.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rates for the actual tail count and top-word bin count

  1. theorem OAI.Ostmann.eventual_character_tail_count_rate line 11
  2. theorem OAI.Ostmann.eventual_character_bin_count line 43
  3. def OAI.Ostmann.characterEndpointExtension line 54

    Source documentation

    The endpoint tests can be extended outside their selected finite set without strengthening any premise about actual endpoints.

    noncomputable def characterEndpointExtension (E : Finset ℕ) (x₀ : ℕ)
    (G : ℕ → ℕ → ℂ) (x p : ℕ) : ℂ := if x ∈ E then G x p else G x₀ p
  4. theorem OAI.Ostmann.characterEndpointExtension_of_mem line 57
  5. theorem OAI.Ostmann.characterEndpointExtension_property line 61