OAI/NumberTheory/JointDickman/Amplification/FirstFormDiagonal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The diagonal is bounded by one weight cap times the linear mass

  1. def OAI.JointDickman.firstFormAtom line 11
  2. def OAI.JointDickman.firstFormDiagonal line 20
  3. def OAI.JointDickman.firstFormMass line 26
  4. theorem OAI.JointDickman.firstFormAtom_diagonal_bound line 30
  5. theorem OAI.JointDickman.firstFormDiagonal_le line 61

    Source documentation

    Bounding one regular coefficient/residue factor pays only one Q.

    theorem firstFormDiagonal_le (B L : ℕ) (τ C : ℝ) (u : ℕ → ℝ)
    (v : ℕ → ℕ → ℝ) (J : ℕ → ℂ) (φ : ℕ → ℝ) (N : ℕ) (Q : ℝ)
    (hu : ∀ c, 0 ≤ u c) (hv : ∀ a c, v a c ∈ Set.Icc (0 : ℝ) 1)
    (hJ : ∀ n, ‖J n‖^2 ≤ 4*φ n)
    (hcap : ∀ a m, regularCoefficientWeight B L τ C a * arithmeticResidueWeight B L τ C m ≤ Q) :
    firstFormDiagonal B L τ C u v J N ≤ 4*Q*firstFormMass B L τ C u v φ N := by
…

    Mentions: OAI.JointDickman.regularCoefficientWeight, OAI.JointDickman.arithmeticResidueWeight, OAI.JointDickman.firstFormDiagonal, OAI.JointDickman.firstFormMass