OAI/NumberTheory/Ostmann/Arithmetic/FrozenPrimeArithmeticNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frozenBulkFrequencyPrime line 11
2. theorem OAI.Ostmann.frozenBulkFrequencyPrime_mean_le line 42

   Source documentation

   The retained fixed support mask can only decrease the bulk norm.

   theorem frozenBulkFrequencyPrime_mean_le
       (outside : List ℕ) (childBound : ℕ → ℕ) (input : PublishedProgressionInput)
       (Q : ℕ) (X Y : ℝ) (hX : 0 ≤ X) (hY : 0 ≤ Y) :
       let T := fun b => buildMovingSlotData n
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.buildMovingSlotData

3. theorem OAI.Ostmann.frozenArithmetic_same_assignment_prime_norm line 90

   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_prime_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