OAI/NumberTheory/Ostmann/Arithmetic/FrequencyBulkNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.arithmeticLeafSupport_mean_le line 11
2. theorem OAI.Ostmann.uniform_average_norm_average_mul_le line 36
3. theorem OAI.Ostmann.frequencyModelBulkCore_mean_le line 91

   Source documentation

   The original bulk unit law gives the product of the simultaneous quadratic-root bounds. The coefficient contains the literal data weights.

   theorem frequencyModelBulkCore_mean_le (x y : ℤ) :
       let T := fun b => buildMovingSlotData n
   …

   Mentions: OAI.Ostmann.buildMovingSlotData

4. theorem OAI.Ostmann.frequencyModelBulkPage_mean_le line 129

   Source documentation

   Discarding the Page multiplier costs only two and preserves every frequency split saving under the original bulk law.

   theorem frequencyModelBulkPage_mean_le (input : PublishedProgressionInput)
       (Q : ℕ) (Y : ℝ) (hY : 0 ≤ Y) :
       let T := fun b => buildMovingSlotData n
   …

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