OAI/NumberTheory/Ostmann/Characters/CharacterMeanRotation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quarterTurn line 10
2. theorem OAI.Ostmann.quarterTurn_norm line 13
3. theorem OAI.Ostmann.exists_positive_quarterTurn line 17
4. theorem OAI.Ostmann.common_positive_character_rotation line 35

   Source documentation

   A single quarter turn retains at least a quarter of the prime mass. Thereafter the word and cell estimates can use the original characters.

   theorem common_positive_character_rotation (P : Finset ℕ) (m : ℕ → ℂ) (δ : ℝ)
       (hm : ∀ p ∈ P, δ ≤ ‖m p‖) :
       ∃ ζ : ℂ, ∃ E : Finset ℕ, ‖ζ‖ = 1 ∧ E ⊆ P ∧
         (∑ p ∈ P, (p : ℝ)⁻¹) / 4 ≤ (∑ p ∈ E, (p : ℝ)⁻¹) ∧
         ∀ p ∈ E, δ / 2 ≤ (ζ * m p).re := by
   …

5. theorem OAI.Ostmann.norm_weighted_common_rotation line 62
6. theorem OAI.Ostmann.CharacterTargetWord.cell_unrotated_mean line 74

   Source documentation

   The positive rotated cell mean supplies the norm bound used by the unrotated initial character statistic, without modifying the harmonic law.

   theorem CharacterTargetWord.cell_unrotated_mean {P : Finset ℕ} {G : ℕ → ℂ}
       {c δ U : ℝ} {k : ℕ} {T : ℝ} (ζ : ℂ) (hζ : ‖ζ‖ = 1)
       (w : CharacterTargetWord P (fun p => ζ * G p) c δ U k T)
       (h : ℕ) (hh : h ∈ w.indices) :
       δ / 2 ≤ ‖∑ p : P, (primeSubsetPrior P (w.cell h) p : ℂ) * G p‖ := by
   …

   Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.primeSubsetPrior