IntegerEdgeOperators.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Operator consequences of the concrete integer weighted-row estimate.

theorem OAI.TwoPointCorrelations.integerEdgeMatrix_localized_square line 14

Source documentation

The localized matrix-square estimate for the actual cutoff graph.

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

Mentions: OAI.TwoPointCorrelations.integerEdgeMatrix

theorem OAI.TwoPointCorrelations.centeredIntegerEdge_operator_norm_le line 36

Source documentation

The single-operator bound 2K for the actual centered integer graph.

theorem centeredIntegerEdge_operator_norm_le
    (site : ι → ℤ) (hinj : Function.Injective site)
    (Q P : Finset ℕ) (u : ℕ → ℝ) (eligible : ℕ → Prop)
    (g : ℤ → ℝ) (L K : ℝ) (extra : ℤ → Prop) (h d : ℕ)
    (hL : 0 < L) (hK : 0 ≤ K) (hu : ∀ q ∈ Q, 0 ≤ u q) (hg : ∀ n, 0 < g n)
    (hP : ∀ p ∈ P, p.Prime) (hd : ∀ p ∈ P, p ∣ d)
    (T : EuclideanSpace ℂ ι →L[ℂ] EuclideanSpace ℂ ι)
    (hT : ∀ v i, T v i = ∑ j,
      (integerEdgeMatrix site Q u eligible g (centeredTuple P) L K extra h d i j : ℂ) * v j) :
    ‖T‖ ≤ 2 * K := by
…

Mentions: OAI.TwoPointCorrelations.integerEdgeMatrix, OAI.TwoPointCorrelations.centeredTuple