OAI/NumberTheory/JointDickman/Probability/ArithmeticGraphKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.JointDickman.GraphCoefficientTriple line 10
2. def OAI.JointDickman.arithmeticGraphTriples line 13
3. def OAI.JointDickman.arithmeticGraphVertexCap line 18
4. def OAI.JointDickman.graphTripleLag line 21
5. def OAI.JointDickman.graphTripleEdges line 24
6. def OAI.JointDickman.graphTripleWeight line 27
7. def OAI.JointDickman.rawArithmeticGraphKernel line 33
8. theorem OAI.JointDickman.graphTriple_lag_mem line 38
9. theorem OAI.JointDickman.graphTriple_edges_subset line 48
10. theorem OAI.JointDickman.arithmeticOffDiagonalGraph_triples line 62
11. theorem OAI.JointDickman.arithmeticOffDiagonalGraph_kernel line 82

    Source documentation

    The graph form as a sum of one kernel per small additive lag. This identity precedes all kernel estimates and contains no analytic premise.

    theorem arithmeticOffDiagonalGraph_kernel (B L : ℕ) (τ C : ℝ)
        (T N : ℕ) (F : ℕ → ℂ) :
        arithmeticOffDiagonalGraph B L τ C T N F =
          (∑ n ∈ Icc 1 (arithmeticGraphVertexCap B N), ∑ j ∈ Icc (-(T : ℤ)) T,
            rawArithmeticGraphKernel B L τ C T N j n * (star (F n)*F ((n : ℤ)+j).toNat).re)/(N : ℝ) := by
    …

    Mentions: OAI.JointDickman.arithmeticOffDiagonalGraph, OAI.JointDickman.arithmeticGraphVertexCap, OAI.JointDickman.rawArithmeticGraphKernel