OAI/NumberTheory/JointDickman/Counting/GraphCoefficientSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Canonical lags and the finite coefficient support of the graph

  1. def OAI.JointDickman.coefficientPairLag line 10
  2. def OAI.JointDickman.GraphCoefficientAdmissible line 13
  3. theorem OAI.JointDickman.nonzero_pairEnergy_admissible line 20

    Source documentation

    Nonzero unequal-pair energy can only occur at an admissible small lag. Thus discarding the other coefficient triples is an exact operation.

    theorem nonzero_pairEnergy_admissible {B L T : ℕ} (τ C : ℝ) (u : ℕ → ℝ)
    (J : ℕ → ℂ) (N : ℕ) {D A E : Finset ℕ}
    (hD : D ⊆ auxiliaryPrimes B) (hA : A ⊆ auxiliaryPrimes B)
    (hE : E ⊆ auxiliaryPrimes B) (hAE : A ≠ E) (hT : T ≤ auxiliaryCutoff B)
    (h : firstFormPairEnergy B L τ C u (amplificationInnerWeight T) J N D A E ≠ 0) :
    GraphCoefficientAdmissible T D A E := by
…

    Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.firstFormPairEnergy, OAI.JointDickman.amplificationInnerWeight, OAI.JointDickman.GraphCoefficientAdmissible