OAI/NumberTheory/Ostmann/Quadratic/QuadraticCorrectionBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quadraticDivisorDyadicBlock_eq_filter line 11
2. theorem OAI.Ostmann.quadratic_correction_divisor_sum line 29
3. theorem OAI.Ostmann.quadratic_correction_divisor_bound line 36
4. theorem OAI.Ostmann.quadraticDyadicDivisors_eq_filter line 46
5. theorem OAI.Ostmann.quadratic_correction_frequency_sum line 70
6. theorem OAI.Ostmann.quadratic_correction_rectangle_bound line 79

   Source documentation

   The original rectangular correction sum is bounded by its actual frequency blocks, with the unit divisor separated before any triangle inequality.

   theorem quadratic_correction_rectangle_bound {Q : ℕ} (hQ : 1 ≤ Q) (K : ℕ)
       (F : ℕ → ℕ → ℂ) (A : ℕ → ℝ) (T : ℕ → ℕ → ℝ)
       (hunit : ∀ i < Nat.log 2 K + 1,
         ‖∑ b ∈ oddSquarefreeRange (2 * 2 ^ i),
           if 2 ^ i ≤ b ∧ b ≤ K ∧ b < 2 * 2 ^ i then F 1 b else 0‖ ≤ A i)
       (hblock : ∀ i < Nat.log 2 K + 1, ∀ j < Nat.log 2 Q + 1,
         ‖∑ d ∈ Finset.Ioc (2 ^ j) (2 * 2 ^ j), ∑ b ∈ oddSquarefreeRange (2 * 2 ^ i),
           if d ≤ Q ∧ 2 ^ i ≤ b ∧ b ≤ K ∧ b < 2 * 2 ^ i then F d b else 0‖ ≤ T i j) :
       ‖∑ d ∈ Finset.Icc 1 Q, ∑ b ∈ oddSquarefreeRange K, F d b‖ ≤
         ∑ i ∈ Finset.range (Nat.log 2 K + 1),
           (A i + ∑ j ∈ Finset.range (Nat.log 2 Q + 1), T i j) := by
   …

   Mentions: OAI.Ostmann.oddSquarefreeRange