OAI/NumberTheory/JointDickman/Counting/TypicalShortEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.restrictArithmetic line 10
2. theorem OAI.JointDickman.restrictArithmetic_norm_le line 14
3. lemma OAI.JointDickman.complexShortAverage_sub line 22
4. theorem OAI.JointDickman.shortAverage_restrict_energy line 30

   Source documentation

   Removing an arbitrary exceptional set costs its ordinary counting density, uniformly in the short-window length.

   theorem shortAverage_restrict_energy (S : ℕ → Prop) [DecidablePred S]
       (f : ArithmeticFunction ℂ) (hf : ∀ n, ‖f n‖ ≤ 1)
       {X H : ℝ} (hX : 0 < X) (hH : 1 ≤ H) (hHX : H ≤ X) :
       (1 / X) * (∫ x in X..2 * X, ‖complexShortAverage f H x‖ ^ 2) ≤
         2 * ((1 / X) * (∫ x in X..2 * X, ‖complexShortAverage (restrictArithmetic S f) H x‖ ^ 2)) +
           4 * (((range (⌊3 * X⌋₊ + 1)).filter fun n => ¬S n).card : ℝ) / X := by
   …

   Mentions: OAI.JointDickman.restrictArithmetic

5. theorem OAI.JointDickman.shortAverage_typical_dyadic_energy line 77

   Source documentation

   This is the analytic transfer used after the multiscale estimate for the literal typical coefficient. No multiplicativity is assumed of the cutoff.

   theorem shortAverage_typical_dyadic_energy (η : ℝ) (hη : 0 < η) (hηhalf : η < 1/2)
       (m : ℕ) (hm : 0 < m) :
       ∃ C : ℝ, 0 < C ∧ ∀ (S : ℕ → Prop) [DecidablePred S]
         (f : ArithmeticFunction ℂ), (∀ n, ‖f n‖ ≤ 1) →
         ∀ X H : ℝ, 0 < X → 1 ≤ H → H ≤ X → ∀ A B : ℝ, 0 ≤ A → 0 ≤ B →
         (∀ T : ℝ, 1 ≤ T →
           (∫ t in -T..T, ‖mellinPolynomial (Ioc ⌊X⌋₊ ⌊4 * X⌋₊)
             (restrictArithmetic S f) t‖ ^ 2) ≤ A + B * T) →
         (1 / X) * (∫ x in X..2 * X, ‖complexShortAverage f H x‖ ^ 2) ≤
           C * (A + B * X / H) +
             4 * (3 / (m : ℝ) + 11 / H + H / X + 1 / X + 16 * η) ^ 2 +
             4 * (((range (⌊3 * X⌋₊ + 1)).filter fun n => ¬S n).card : ℝ) / X := by
   …

   Mentions: OAI.JointDickman.mellinPolynomial, OAI.JointDickman.restrictArithmetic