OAI/NumberTheory/Ostmann/Arithmetic/MovingGiantPhase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.giantPairPhase line 12

   Source documentation

   The two cofactor phases before inserting the logarithmic coordinates.

   noncomputable def giantPairPhase (g : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (D H XL XR : ℕ) (s : ℤ) : ℂ :=
   …

2. def OAI.Ostmann.movingGiantPhase line 21

   Source documentation

   The two giant factors of Section 7.4, evaluated at their exact cofactors. The definition also applies to the integer giant in a transfer diagonal.

   noncomputable def movingGiantPhase {σ B : Type*} {n : ℕ}
       (value : σ → ℕ) (outside : List ℕ) (small bulk : TreeLeafTuple (List B) n)
       (g : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (s : ℤ) (y : B → σ) (x z : ℝ) : ℂ :=
   …

   Mentions: OAI.Ostmann.TreeLeafTuple

3. theorem OAI.Ostmann.movingGiantPhase_norm_le line 30
4. theorem OAI.Ostmann.movingGiantPhase_selectedBulkSample line 40