OAI/NumberTheory/Ostmann/Characters/CharacterRepeatRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Repeated-prime loss for the actual top-first character word

  1. theorem OAI.Ostmann.character_wordRepeatFactor_eq line 12

    Source documentation

    The character word puts the top prime first. Its normalizer is the same as the bulk-first ordering used in the elementary repeat estimate.

    theorem character_wordRepeatFactor_eq {m c : ℕ} (P B T : Finset ℕ)
    (Q : Fin (m + 1) → Finset ℕ) (R : Fin c → Finset ℕ)
    (hzero : Q 0 = T) (hsucc : ∀ i : Fin m, Q i.succ = B)
    (ψ : 𝓢(ℝ, ℂ)) (D : ℝ) :
    wordRepeatFactor P Q R ψ D =
      wordRepeatFactor P (Fin.append (fun _ : Fin m => B) (fun _ : Fin 1 => T)) R ψ D := by
…

    Mentions: OAI.Ostmann.wordRepeatFactor

  2. theorem OAI.Ostmann.eventual_character_repeat_rate line 28