OAI/NumberTheory/Ostmann/Arithmetic/FrozenBulkFrequencyNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The frequency norm with the original fixed nonbulk masks

  1. theorem OAI.Ostmann.frozenBulkFrequencyFactor_mean_le line 30

    Source documentation

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

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

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