OAI/NumberTheory/TwoPoint/Bounds/IntegerEdgeRows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Derivation of the weighted row estimate for the concrete integer graph.

  1. lemma OAI.TwoPointCorrelations.directedIntegerEdge_forward_bound line 14
  2. lemma OAI.TwoPointCorrelations.directedIntegerEdge_backward_bound line 37
  3. lemma OAI.TwoPointCorrelations.directedIntegerEdge_forward_row line 64
  4. lemma OAI.TwoPointCorrelations.directedIntegerEdge_backward_row line 76
  5. theorem OAI.TwoPointCorrelations.integerEdgeMatrix_weighted_row line 91

    Source documentation

    Both edge orientations are bounded by the same retained padding mass. Incoming divisibility uses the actual integer step h*q*d.

    theorem integerEdgeMatrix_weighted_row
    {ι : Type*} [Fintype ι] (site : ι → ℤ) (hinj : Function.Injective site)
    (hL : 0 < L) (hK : 0 ≤ K) (hu : ∀ q ∈ Q, 0 ≤ u q) (hg : ∀ n, 0 < g n)
    (hperiod : ∀ q ∈ Q, ∀ n, center (n + (h * q * d : ℕ)) = center n)
    (i : ι) :
    ∑ j, |integerEdgeMatrix site Q u eligible g center L K extra h d i j| *
      g (site j) / g (site i) ≤ 2 * K * |center (site i)| := by
…

    Mentions: OAI.TwoPointCorrelations.integerEdgeMatrix

  6. lemma OAI.TwoPointCorrelations.integerEdgeMatrix_center_invariant line 132