ArithmeticOffDiagonalGraph.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact graph representation of the full off-diagonal energy

def OAI.JointDickman.arithmeticOffDiagonalGraph line 12
theorem OAI.JointDickman.firstFormOffDiagonal_graph line 24
Source documentation
The original off-diagonal energy equals the arithmetic graph, including its actual coefficient/residue weights and exact finite endpoints.
```
theorem firstFormOffDiagonal_graph (B L : ℕ) (τ C : ℝ) (T N : ℕ)
    (hT : T ≤ auxiliaryCutoff B) (F : ℕ → ℂ)
    (hF : ∀ A ∈ (auxiliaryPrimes B).powerset, ∀ n, F ((∏ p ∈ A, p)*n) = F n) :
    firstFormOffDiagonal B L τ C (amplificationOuterWeight B) (amplificationInnerWeight T)
      (fun m => F (m+1)) N = arithmeticOffDiagonalGraph B L τ C T N F := by
…
```
Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.firstFormOffDiagonal, OAI.JointDickman.amplificationOuterWeight, OAI.JointDickman.amplificationInnerWeight, OAI.JointDickman.arithmeticOffDiagonalGraph

theorem OAI.JointDickman.centered_binLabel_offDiagonal_graph line 54

Source documentation

The exact graph identity for the moving centered second bin label.

theorem centered_binLabel_offDiagonal_graph {ι : Type*} [Fintype ι]
    (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
    (z : ι → ℂ) (μ : ℂ) (B L : ℕ) (τ C : ℝ) (T : ℕ) (hT : T ≤ auxiliaryCutoff B) :
    ∀ᶠ N : ℕ in atTop,
      firstFormOffDiagonal B L τ C (amplificationOuterWeight B) (amplificationInnerWeight T)
        (fun m => movingBinLabel J k z N (m+1)-μ) N =
      arithmeticOffDiagonalGraph B L τ C T N (fun n => movingBinLabel J k z N n-μ) := by
…

Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.firstFormOffDiagonal, OAI.JointDickman.amplificationOuterWeight, OAI.JointDickman.amplificationInnerWeight, OAI.JointDickman.movingBinLabel, OAI.JointDickman.arithmeticOffDiagonalGraph