OAI/NumberTheory/JointDickman/Counting/OffDiagonalEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.complex_norm_sq_eq_re_star_mul line 11
2. theorem OAI.JointDickman.norm_sum_sq_eq_double line 18
3. theorem OAI.JointDickman.norm_sum_sq_split line 25
4. def OAI.JointDickman.firstFormOffDiagonal line 40
5. theorem OAI.JointDickman.firstFormEnergy_eq_diagonal_add line 49
6. theorem OAI.JointDickman.positive_offDiagonal_of_energy line 65

   Source documentation

   Diagonal removal retains half of any positive lower energy constant.

   theorem positive_offDiagonal_of_energy
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L : ℕ} (hL : 1 ≤ L) {τ : ℝ} (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau)
       (C : ℝ) (J : ℕ → ℕ → ℂ) (hJ : ∀ N n, ‖J N n‖ ≤ 2)
       (s : ℕ → ℕ) (hs : StrictMono s) {e : ℝ} (he : 0 < e)
       (henergy : ∀ᶠ B : ℕ in atTop, ∀ᶠ N : ℕ in atTop,
         e ≤ firstFormEnergy B L τ C (amplificationOuterWeight B)
           (amplificationInnerWeight (amplificationMultiplier B)) (J (s N)) (s N) /
             ((B : ℝ)*amplificationMultiplier B)) :
       ∀ᶠ B : ℕ in atTop, ∀ᶠ N : ℕ in atTop,
         e/2 ≤ firstFormOffDiagonal B L τ C (amplificationOuterWeight B)
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.samplingTau, OAI.JointDickman.firstFormEnergy, OAI.JointDickman.amplificationOuterWeight, OAI.JointDickman.amplificationInnerWeight, OAI.JointDickman.amplificationMultiplier, OAI.JointDickman.firstFormOffDiagonal