OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkLogFactors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkLogCutoffWeight line 11
2. theorem OAI.Ostmann.bulkLogCutoffWeight_bounds line 15
3. theorem OAI.Ostmann.movingBulkListLogWeight_eq_cutoff line 25

   Source documentation

   At the original positive prime values this is precisely the initial log-sum cutoff, including its unchanged spectator factor.

   theorem movingBulkListLogWeight_eq_cutoff {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ a, 0 < value a) (outside : List ℕ) (cb cd : ℝ) (slots : List σ) :
       movingBulkListLogWeight value outside cb cd slots =
         bulkLogCutoffWeight (fun a => (value a : ℝ)) cb slots *
           logCellProfile ((outside.map (fun p => Real.log (p : ℝ))).sum - cd) := by
   …

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

4. def OAI.Ostmann.bulkLogCutoffFactors line 47
5. theorem OAI.Ostmann.bulkLogCutoffFactors_weight line 56
6. theorem OAI.Ostmann.bulkLogCutoffFactors_budget line 69
7. theorem OAI.Ostmann.bulkLogCutoffFactors_roots line 80

   Source documentation

   Repeated occurrences in a leaf group are retained. They contribute their actual multiplicity to the elementary degree bound.

   theorem bulkLogCutoffFactors_roots {σ : Type*} {t : ℕ}
       (value : σ → ℝ) (i : σ) (cb D : ℝ) (hD : 0 ≤ D)
       (hlip : ∀ x y, |logCellProfile x - logCellProfile y| ≤ D * |x - y|)
       (slots : Fin t → List σ) (r : ℕ) (hr : ∀ j, (slots j).length ≤ r) :
       ∃ S : Finset ℝ, S.card ≤ t * r ∧
         ∀ j z, z ∈ (bulkLogCutoffFactors value i cb D hD hlip slots j).polynomial.derivative.roots → z ∈ S := by
   …

   Mentions: OAI.Ostmann.logCellProfile, OAI.Ostmann.bulkLogCutoffFactors