OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeAverages.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingInternalPrimeAverage line 11
2. def OAI.Ostmann.movingSpectatorPrimeAverage line 17
3. def OAI.Ostmann.frozenBulkSpectatorPrime line 23
4. theorem OAI.Ostmann.movingArithmeticPrimePageFactor_averages line 31
5. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_prime_page_factorization line 56

   Source documentation

   Both exceptional-character multipliers remain in the frequency factor. All internal and spectator factors have the literal two-unit law.

   theorem movingSeparatedPairResidueCoefficient_prime_page_factorization {σ I : Type*}
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (g : ∀ i, ZMod (q i) → ℂ) (D : Bool → ∀ i, (ZMod (q i))ˣ)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (nodes : Bool → List MovingFormulaNode)
       (R : ℤ) (r : ℕ) [NeZero r] (P : Finset ℕ) (S : Finset I)
       [∀ p : P, Fact p.val.Prime] [∀ b, NeZero (movingArithmeticModuli r q P S b)]
       [NeZero (∏ b, movingArithmeticModuli r q P S b)]
       (hf : ∀ side, (T side).Frequencies (· ≠ 0))
       (hR : ∀ side, (T side).frequencyProduct ∣ R)
       (hfrequency : R ^ (n + 1) ∣ (r : ℤ))
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingArithmeticModuli

6. theorem OAI.Ostmann.frozenBulkSpectatorPrime_actual line 85
7. theorem OAI.Ostmann.frozenBulkSpectatorPrime_absolute_mean_le line 107

   Source documentation

   The original two-prime spectator average has the same absolute third moment bound, without a density correction.

   theorem frozenBulkSpectatorPrime_absolute_mean_le {σ : Type*} {q : ℕ} [Fact q.Prime]
       (hq : 3 ≤ q) (base : σ → ℕ) (n m : ℕ) (hm : 0 < m)
       (t : Bool → FrequencyTree ℤ n)
       (small : Bool → TreeLeafTuple (List σ) n) (samples : Bool → MovingSampleSlots σ n)
       (hfreq : ∀ b, movingGiantFrequencyUnits q n (t b))
       (hsmall : ∀ b, ((treeLeafProduct n (movingSlotValues base n (small b)) : ℕ) : ZMod q) ≠ 0)
       (hsamples : ∀ b, ((samples b).values base).UnitsAt q)
       (D : Bool → (ZMod q)ˣ) (e : Equiv.Perm (TreeLeafIndex n × Fin m))
       (g : ZMod q → ℂ) (hg : g 0 = 0) (henergy : ∑ x : ZMod q, ‖g x‖ ^ 2 ≤ (q : ℝ)) :
       (Fintype.card (TreeLeafIndex n × Fin m → (ZMod q)ˣ) : ℝ)⁻¹ *
         (∑ z : TreeLeafIndex n × Fin m → (ZMod q)ˣ,
           ‖frozenBulkSpectatorPrime base n m t small samples D e g z‖) ≤ (3 : ℝ) ^ (2 ^ n) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingSlotValues, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.frozenBulkSpectatorPrime