ArithmeticGraphPair.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic graph weight obtained from the actual quadratic form

def OAI.JointDickman.arithmeticGraphPairWeight line 10
theorem OAI.JointDickman.divisorEdge_new_quotients line 18
theorem OAI.JointDickman.firstFormPairWeight_graph line 36

theorem OAI.JointDickman.firstFormPairEnergy_graph line 52

Source documentation

This is the exact arithmetic graph expression for a fixed coefficient pair in the original energy. It includes both signs of the additive lag.

theorem firstFormPairEnergy_graph {B L : ℕ} (τ C : ℝ)
    (u : ℕ → ℝ) (v : ℕ → ℕ → ℝ) {D A E : Finset ℕ} {j : ℤ}
    (ha : 0 < ∏ p ∈ A, p) (hb : 0 < ∏ p ∈ E, p) (hc : 0 < ∏ p ∈ D, p)
    (he : ((∏ p ∈ A, p : ℕ) : ℤ)-(∏ p ∈ E, p : ℕ) = j*(∏ p ∈ D, p : ℕ))
    (hcop : (∏ p ∈ A, p).Coprime j.natAbs) (N : ℕ) (F : ℕ → ℂ)
    (hFa : ∀ n, F ((∏ p ∈ A, p)*n) = F n)
    (hFb : ∀ n, F ((∏ p ∈ E, p)*n) = F n)
    (hFc : ∀ n, F ((∏ p ∈ D, p)*n) = F n) :
    firstFormPairEnergy B L τ C u v (fun m => F (m+1)) N D A E =
      ∑ n ∈ divisorEdgeNew (∏ p ∈ A, p) (∏ p ∈ E, p) (∏ p ∈ D, p) N j,
        arithmeticGraphPairWeight B L τ C u v
          (∏ p ∈ A, p) (∏ p ∈ E, p) (∏ p ∈ D, p) j n *
…

Mentions: OAI.JointDickman.firstFormPairEnergy, OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.arithmeticGraphPairWeight