OAI/NumberTheory/Ostmann/Characters/CharacterPrimeCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.characterPrimeCells line 10
2. theorem OAI.Ostmann.characterPrimeCells_subset line 19
3. theorem OAI.Ostmann.characterPrimeCells_norm_mean line 28
4. theorem OAI.Ostmann.characterPrimeCells_index line 42
5. theorem OAI.Ostmann.characterPrimeCells_product_bounds line 56

   Source documentation

   The target certificate gives the whole-atom endpoints used by the initial amplitude and all later transfer steps.

   theorem characterPrimeCells_product_bounds {P : Finset ℕ} {F : ℕ → ℂ}
       {c δ U : ℝ} {k : ℕ} {T : Option (Fin k) → ℝ}
       (w : ∀ j, CharacterTargetWord P F c δ U k (T j))
       (a : Fin k → Bool → ℕ) (J E : ℝ) (hc : 0 < c) (hδ : 0 < δ)
       (hE : ∀ v, 64 / (δ * c) +
         (characterCellSize (fun j => (w (some j)).indices.length) (w none).indices.length v : ℝ) ≤ E) :
       ∀ v : CharacterCell k,
         Real.exp (characterLogCenter J (fun j => T (some j)) (fun j b => (a j b : ℝ))
           (T none) (true, some v) - E) ≤
           (∏ i, primeCellLower (characterCellIndex (fun j => (w (some j)).indices) a (w none).indices v i) : ℕ) ∧
         (∏ i, primeCellUpper (characterCellIndex (fun j => (w (some j)).indices) a (w none).indices v i) : ℕ) ≤
           Real.exp (characterLogCenter J (fun j => T (some j)) (fun j b => (a j b : ℝ))
   …

   Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.characterCellSize, OAI.Ostmann.CharacterCell, OAI.Ostmann.characterLogCenter, OAI.Ostmann.primeCellLower, OAI.Ostmann.characterCellIndex, OAI.Ostmann.primeCellUpper