OAI/NumberTheory/JointDickman/Analysis/CharacterPrimeCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.finite_distance_lower line 14

   Source documentation

   A finite distance dominates the absolutely convergent damped distance, with the missing mass accounted for explicitly.

   theorem finite_distance_lower {ι : Type*} (S : Finset ι) (a b v : ι → ℝ)
       (hb : Summable b) (hb0 : ∀ i, 0 ≤ b i)
       (hv : ∀ i, |v i| ≤ 1) (hba : ∀ i ∈ S, b i ≤ a i) :
       2*(∑ i ∈ S, b i) - ∑' i, b i - ∑' i, v i*b i ≤
         ∑ i ∈ S, (1-v i)*a i := by
   …

2. def OAI.JointDickman.characterPrimePhase line 37
3. theorem OAI.JointDickman.characterPrimePhase_norm_le line 41
4. theorem OAI.JointDickman.characterPrimePower_eq_phase line 48
5. def OAI.JointDickman.primeCutoff line 64
6. theorem OAI.JointDickman.primeCutoff_sum line 67
7. theorem OAI.JointDickman.characterDistance_primeCutoff line 71
8. theorem OAI.JointDickman.characterDistance_damped_lower line 84

   Source documentation

   The prime cutoff can be replaced by the Euler half-plane without hiding any arithmetic cancellation in an assumption.

   theorem characterDistance_damped_lower {q : ℕ} (χ : DirichletCharacter ℂ q)
       (X t : ℝ) {σ : ℝ} (hσ : 1 < σ) :
       2*(∑ p ∈ primeCutoff X, (p.val:ℝ)^(-σ)) -
         (∑' p : Nat.Primes, (p.val:ℝ)^(-σ)) -
         (primeCharacterLinearSum χ ((σ:ℂ)+(t:ℂ)*I)).re ≤
         PublishedInputs.primeDistanceSquared (characterArithmetic χ) X t := by
   …

   Mentions: OAI.JointDickman.primeCutoff, OAI.JointDickman.primeCharacterLinearSum, OAI.JointDickman.PublishedInputs.primeDistanceSquared, OAI.JointDickman.characterArithmetic