OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkLogVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingBulkListLogWeight_variation line 12

   Source documentation

   Freezing each prime in a log cell of diameter η changes the retained bulk cutoff by at most its number of slots times one fixed Lipschitz constant.

   theorem movingBulkListLogWeight_variation {σ : Type*}
       (value value' : σ → ℕ) (outside : List ℕ) (cb cd D η : ℝ)
       (hD : 0 ≤ D)
       (hprofile : ∀ x y, |logCellProfile x - logCellProfile y| ≤ D * |x - y|)
       (bulk : List σ)
       (hclose : ∀ a ∈ bulk, |Real.log (value a : ℝ) - Real.log (value' a : ℝ)| ≤ η) :
       |movingBulkListLogWeight value outside cb cd bulk -
           movingBulkListLogWeight value' outside cb cd bulk| ≤ D * bulk.length * η := by
   …

   Mentions: OAI.Ostmann.logCellProfile, OAI.Ostmann.movingBulkListLogWeight