OAI/NumberTheory/Ostmann/Arithmetic/MovingGuardedRow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingGuardedRow line 11
2. theorem OAI.Ostmann.movingGuardedRow_energy line 19

   Source documentation

   Invalid compensation vectors stay in the original sample space with zero row. No conditioning or renormalization of that sample law is used.

   theorem movingGuardedRow_energy {J : Type*} [Fintype J]
       (q : J → ℕ) [∀ j, Fact (q j).Prime]
       (g : ∀ j, ZMod (q j) → ℂ) (D M : ℕ) (hM : (∏ j, q j) = M)
       (giant : J) (S : ∀ j, Finset (ZMod (q j)))
       (hg : ∀ x, ‖g giant x‖ ≤ 1)
       (hregular : ∀ j, j ≠ giant → g j = normalizedResidueTransform (S j))
       (hS : ∀ j, j ≠ giant → (S j).Nonempty)
       (hSp : ∀ j, j ≠ giant → (S j).card < q j) :
       (∑ t : Fin M, ‖movingGuardedRow q g D t‖ ^ 2) ≤ M := by
   …

   Mentions: OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.movingGuardedRow

3. theorem OAI.Ostmann.movingGuardedRow_grouped line 37

   Source documentation

   On support this is exactly the current transform at the grouped key.

   theorem movingGuardedRow_grouped {J : Type*} [Fintype J]
       (q : J → ℕ) [∀ j, Fact (q j).Prime]
       (g : ∀ j, ZMod (q j) → ℂ) (D H : ℕ) (v : ℤ)
       (hc : Pairwise (fun i j => (q i).Coprime (q j))) (hD : ∀ j, D.Coprime (q j))
       (hH : H.Coprime (∏ j, q j)) :
       movingGuardedRow q g D (positiveIntegerPivotKey (∏ j, q j)
         (Finset.prod_pos (fun j _ => (Fact.out : (q j).Prime).pos)) H v) =
         movingRegularTransform q g (D * H) v := by
   …

   Mentions: OAI.Ostmann.movingGuardedRow, OAI.Ostmann.positiveIntegerPivotKey, OAI.Ostmann.movingRegularTransform