OAI/NumberTheory/Ostmann/Construction/FixedCharacterTargetCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.fixedTargetCells line 10
2. theorem OAI.Ostmann.fixedTargetCells_subset line 16
3. theorem OAI.Ostmann.fixedTargetCells_mass line 22
4. theorem OAI.Ostmann.fixedTargetCells_unrotated_mean line 32

   Source documentation

   Identical shell/list data preserves the positive norm at every retained endpoint, although its test function and target certificate may differ.

   theorem fixedTargetCells_unrotated_mean {P : Finset ℕ} {F G : ℕ → ℂ}
       {c δ U : ℝ} {k : ℕ} {T S : Option (Fin k) → ℝ}
       (w : ∀ j, CharacterTargetWord P F c δ U k (T j))
       (ζ : ℂ) (hζ : ‖ζ‖ = 1)
       (v : ∀ j, CharacterTargetWord P (fun p => ζ * G p) c δ U k (S j))
       (hdata : ∀ j, (v j).indices = (w j).indices ∧
         ∀ h, (v j).cell h = (w j).cell h)
       (i : Σ j, Fin (w j).indices.length) :
       δ / 2 ≤ ‖∑ p : P, (primeSubsetPrior P (fixedTargetCells w i) p : ℂ) * G p‖ := by
   …

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

5. theorem OAI.Ostmann.fixedTargetCells_product_bounds line 48