OAI/NumberTheory/Ostmann/Construction/InitialMovingTests.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.initialGiantFlag line 11
2. theorem OAI.Ostmann.initialGiantFlag_reindex line 16
3. theorem OAI.Ostmann.initial_full_physical_test line 43
4. theorem OAI.Ostmann.initial_full_transform line 62

   Source documentation

   The complete transform uses exactly the manuscript's phase at the two original giant positions and its normalized residue transform elsewhere.

   theorem initial_full_transform (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
       (b d r : ℕ) (S : ∀ q : ℕ, Finset (ZMod q)) (fav : ℕ → Bool)
       (x : Fin ((b + (d + r) + 1) + (b + (d + r) + 1)) → P) (s : ℤ) :
       movingRegularTransform (fun i => (x i : ℕ))
         (fun i => densityFourier (Fin.append
           (primeHalfTests (n := b + (d + r)) P (fun p => S p) (fun p => fav p))
   …

   Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.densityFourier, OAI.Ostmann.primeHalfTests

5. theorem OAI.Ostmann.initial_moving_transform line 79

   Source documentation

   Exact factorization of the original transform after fixing spectators.

   theorem initial_moving_transform (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
       (b d r : ℕ) (S : ∀ q : ℕ, Finset (ZMod q)) (fav : ℕ → Bool)
       (sl sr : Fin d → P) (XL XR : P)
       (y : MovingRegularSlot 0 (r + r) (b + b) → P) (s : ℤ) :
       let x := initialMovingTuple b d r sl sr XL XR y
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.initialMovingTuple

6. theorem OAI.Ostmann.initial_moving_tagged_zero line 122