OAI/NumberTheory/Ostmann/Characters/CharacterTargetCode.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.CharacterTargetWord.code line 10
2. theorem OAI.Ostmann.CharacterTargetWord.index_le line 14
3. theorem OAI.Ostmann.CharacterTargetWord.cell_eq_of_code line 28
4. def OAI.Ostmann.characterTargetCodeGroups line 35
5. theorem OAI.Ostmann.characterTargetCodeGroups_length line 40
6. theorem OAI.Ostmann.characterTargetCodeGroups_size line 46
7. theorem OAI.Ostmann.characterTargetCodeGroups_data line 58
8. theorem OAI.Ostmann.characterTargetCodeGroups_cells line 73
9. theorem OAI.Ostmann.common_character_target_cells line 85

   Source documentation

   Shell identifiers are part of the code, so fixing it fixes the actual prime sets even when targets and Fourier tests vary with the endpoint.

   theorem common_character_target_cells (E : Finset ℕ) (hE : E.Nonempty)
       (P : Finset ℕ) (F : ℕ → ℕ → ℂ) (c δ U : ℝ) (k N B : ℕ)
       (T : ℕ → Option (Fin k) → ℝ)
       (w : ∀ a j, CharacterTargetWord P (F a) c δ U k (T a j))
       (hc : 0 < c) (hδ : 0 < δ) (hk : 5 * k ≤ B)
       (hP : ∀ p ∈ P, primeLogIndex p ≤ B)
       (hN : ∀ a ∈ E, (∑ j : Option (Fin k), (w a j).indices.length) ≤ N) :
       ∃ S : Finset ℕ, S ⊆ E ∧ S.Nonempty ∧
         E.card ≤ ((N + (k + 1) + (k + 1) + 1) *
           (max (N + (k + 1)) B + 1) ^ (N + (k + 1) + (k + 1))) * S.card ∧
         ∀ a ∈ S, ∀ b ∈ S, ∀ j,
           (w a j).indices = (w b j).indices ∧ ∀ h, (w a j).cell h = (w b j).cell h := by
   …

   Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.primeLogIndex