OAI/NumberTheory/TwoPoint/Bounds/MaskedIntegerEdges.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extra symmetric edge restrictions preserve the concrete graph estimates.

  1. def OAI.TwoPointCorrelations.maskedIntegerEdgeMatrix line 14
  2. lemma OAI.TwoPointCorrelations.maskedIntegerEdgeMatrix_symmetric line 20
  3. lemma OAI.TwoPointCorrelations.maskedIntegerEdgeMatrix_weighted_row line 33
  4. lemma OAI.TwoPointCorrelations.maskedIntegerEdgeMatrix_level line 48
  5. theorem OAI.TwoPointCorrelations.maskedIntegerEdgeMatrix_localized_square line 61

    Source documentation

    The full localized estimate survives all symmetric entry restrictions.

    theorem maskedIntegerEdgeMatrix_localized_square
    (site : ι → ℤ) (hinj : Function.Injective site)
    (Q : Finset ℕ) (u : ℕ → ℝ) (eligible : ℕ → Prop)
    (g center : ℤ → ℝ) (L K : ℝ) (extra : ℤ → Prop) (h d : ℕ)
    (gate : ι → ι → Prop) (hgate : ∀ i j, gate i j ↔ gate j i)
    (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)
    (v : ι → ℂ) :
    (∑ i, ‖∑ j, maskedIntegerEdgeMatrix site Q u eligible g center L K extra h d gate i j * v j‖ ^ 2) ≤
      4 * K ^ 2 * ∑ i, |center (site i)| ^ 2 * ‖v i‖ ^ 2 := by
…

    Mentions: OAI.TwoPointCorrelations.maskedIntegerEdgeMatrix