OAI/NumberTheory/JointDickman/Analysis/MellinFloorEndpoints.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The bounded floor discrepancy between real and integer dyadic cutoffs

  1. lemma OAI.JointDickman.mellinPolynomial_consecutive line 9
  2. lemma OAI.JointDickman.norm_mellinPolynomial_interval_le line 16
  3. lemma OAI.JointDickman.nat_floor_four_bounds line 33
  4. theorem OAI.JointDickman.mellinPolynomial_real_cutoff_energy line 49

    Source documentation

    The three possible extra floor-endpoint terms contribute only O(T/N²) to the spectral energy.

    theorem mellinPolynomial_real_cutoff_energy (a : ℕ → ℂ) (ha : ∀ n, ‖a n‖ ≤ 1)
    {X A B : ℝ} (hX : 1 ≤ X)
    (hbound : ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖mellinPolynomial (Ioc ⌊X⌋₊ (4 * ⌊X⌋₊)) a t‖ ^ 2) ≤ A + B * T) :
    ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖mellinPolynomial (Ioc ⌊X⌋₊ ⌊4 * X⌋₊) a t‖ ^ 2) ≤
        2 * A + (2 * B + 3 / (⌊X⌋₊ : ℝ) ^ 2) * T := by
…

    Mentions: OAI.JointDickman.mellinPolynomial