ModFiveVerticalTails.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The two tails of the actual Perron integral. The inverse-square majorant gives explicit inverse-height bounds after integration.

lemma OAI.TwoPointCorrelations.modFive_inverse_square_tail line 13
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveVerticalTails.lean:13 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_vertical_tails line 26
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveVerticalTails.lean:26 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_perron_integrable line 55
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveVerticalTails.lean:55 (same declaration text).

theorem OAI.TwoPointCorrelations.modFive_perron_tail_bound line 91

Source documentation

Uniform tails of the actual nonprincipal Perron integrals.

Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveVerticalTails.lean:91 (same declaration text).

theorem modFive_perron_tail_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : DirichletCharacter ℂ 5), χ ≠ 1 → ∀ δ x T : ℝ,
      0 < δ → 0 < x → 0 < T →
      ‖VerticalIntegral (modFivePerronIntegrand χ x) (1 + δ) -
        VIntegral (modFivePerronIntegrand χ x) (1 + δ) (-T) T‖ ≤
          2 * (1 / δ + C) * x ^ (1 + δ) / T := by
…

Mentions: OAI.TwoPointCorrelations.modFivePerronIntegrand