OAI/NumberTheory/Ostmann/Arithmetic/FrozenArithmeticNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.frozenArithmetic_same_assignment_norm line 31

   Source documentation

   The nonnegative original arithmetic model retains the frequency saving, the absolute spectator moments and the exact number of bulk Page factors.

   theorem frozenArithmetic_same_assignment_norm
       (p : I → ℕ) [∀ i, Fact (p i).Prime]
       [NeZero (∏ i, bulkResidueModuli (R ^ (n - 1 + 2)) p i)]
       (hc : Pairwise (fun i j => (bulkResidueModuli (R ^ (n - 1 + 2)) p i).Coprime
         (bulkResidueModuli (R ^ (n - 1 + 2)) p j)))
       (hp : ∀ i, 3 ≤ p i)
       (hfreq : ∀ i b, movingGiantFrequencyUnits (p i) n
         (frequencyTreeMap Subtype.val n (frequencyPairProjection S n b t)))
       (hsmallp : ∀ i b, ((treeLeafProduct n (movingSlotValues base n (small b)) : ℕ) : ZMod (p i)) ≠ 0)
       (hasamples : ∀ i b, ((a b).values base).UnitsAt (p i))
       (g : ∀ i, ZMod (p i) → ℂ) (hg : ∀ i, g i 0 = 0)
       (henergy : ∀ i, ∑ x : ZMod (p i), ‖g i x‖ ^ 2 ≤ (p i : ℝ))
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.frequencyTreeMap, OAI.Ostmann.frequencyPairProjection, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingSlotValues