OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeRowNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_crt_row_energy line 14

   Source documentation

   Both the giant's bounded row and the exact compensation-prime energies enter multiplicatively, at their actual modulus sizes.

   theorem moving_crt_row_energy {J : Type*} [Fintype J]
       (p : J → ℕ) [∀ j, NeZero (p j)] [NeZero (∏ j, p j)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (g : ∀ j, ZMod (p j) → ℂ)
       (henergy : ∀ j, (∑ x, ‖g j x‖ ^ 2) ≤ (p j : ℝ)) :
       (∑ x : ZMod (∏ j, p j), ‖tupleCRTFunction p hc g x‖ ^ 2) ≤ (∏ j, p j : ℕ) := by
   …

   Mentions: OAI.Ostmann.tupleCRTFunction

2. theorem OAI.Ostmann.moving_crt_scaled_row_energy line 33

   Source documentation

   The cofactor and outside-denominator units merely permute each local row.

   theorem moving_crt_scaled_row_energy {J : Type*} [Fintype J]
       (p : J → ℕ) [∀ j, Fact (p j).Prime] [NeZero (∏ j, p j)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (g : ∀ j, ZMod (p j) → ℂ) (u : ∀ j, (ZMod (p j))ˣ)
       (henergy : ∀ j, (∑ x, ‖g j x‖ ^ 2) ≤ (p j : ℝ)) :
       (∑ x : ZMod (∏ j, p j),
         ‖tupleCRTFunction p hc (fun j x => g j ((u j : ZMod (p j)) * x)) x‖ ^ 2) ≤
           (∏ j, p j : ℕ) := by
   …

   Mentions: OAI.Ostmann.tupleCRTFunction

3. theorem OAI.Ostmann.moving_crt_fin_row_energy line 48

   Source documentation

   This is the counting row indexed by Fin modulus in the finite transfer.

   theorem moving_crt_fin_row_energy {J : Type*} [Fintype J]
       (p : J → ℕ) [∀ j, Fact (p j).Prime] [NeZero (∏ j, p j)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (g : ∀ j, ZMod (p j) → ℂ) (u : ∀ j, (ZMod (p j))ˣ)
       (henergy : ∀ j, (∑ x, ‖g j x‖ ^ 2) ≤ (p j : ℝ)) :
       (∑ x : Fin (∏ j, p j),
         ‖tupleCRTFunction p hc (fun j x => g j ((u j : ZMod (p j)) * x))
           (ZMod.finEquiv (∏ j, p j) x)‖ ^ 2) ≤ (∏ j, p j : ℕ) := by
   …

   Mentions: OAI.Ostmann.tupleCRTFunction

4. theorem OAI.Ostmann.moving_crt_compensation_row_energy line 66

   Source documentation

   The giant factor is bounded by one; all other factors are the paper's normalized compensation transforms. No bound on an individual compensation transform is required.

   theorem moving_crt_compensation_row_energy {J : Type*} [Fintype J]
       (p : J → ℕ) [∀ j, Fact (p j).Prime] [NeZero (∏ j, p j)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j))) (giant : J)
       (g : ∀ j, ZMod (p j) → ℂ) (u : ∀ j, (ZMod (p j))ˣ)
       (S : ∀ j, Finset (ZMod (p 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 < p j) :
       (∑ x : Fin (∏ j, p j),
         ‖tupleCRTFunction p hc (fun j x => g j ((u j : ZMod (p j)) * x))
           (ZMod.finEquiv (∏ j, p j) x)‖ ^ 2) ≤ (∏ j, p j : ℕ) := by
   …

   Mentions: OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.tupleCRTFunction

5. theorem OAI.Ostmann.finEquiv_eq_natCast line 90
6. theorem OAI.Ostmann.moving_compensation_fourier_row_energy line 101

   Source documentation

   The actual extracted row G_P(t/d): each local argument includes the outside denominator and the cofactor of that prime. Their inverses are units, so the exact counting energy remains at most the modulus.

   theorem moving_compensation_fourier_row_energy {J : Type*} [Fintype J]
       (p : J → ℕ) [∀ j, Fact (p j).Prime] [NeZero (∏ j, p j)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j))) (giant : J)
       (g : ∀ j, ZMod (p j) → ℂ) (S : ∀ j, Finset (ZMod (p 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 < p j)
       (D : ℕ) (hD : ∀ j, D.Coprime (p j)) :
       (∑ x : Fin (∏ j, p j), ‖∏ j,
         g j ((x.val : ZMod (p j)) / ((D * tupleCofactor p j : ℕ) : ZMod (p j)))‖ ^ 2) ≤
         (∏ j, p j : ℕ) := by
   …

   Mentions: OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.tupleCofactor