WeightedRows.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Weighted rows and the localized square estimate

Finite weighted Cauchy--Schwarz proves the localized Schur estimate in q:weighted-rows. Constancy of the site factor on the support replaces a level-set decomposition. Summing the localized estimates only uses a bound at the support of the vector; no commutation with a projection is needed.

lemma OAI.TwoPointCorrelations.weighted_row_square line 21
lemma OAI.TwoPointCorrelations.weighted_column_bound line 38

theorem OAI.TwoPointCorrelations.weighted_kernel_localized_square line 60

Source documentation

The finite localized square bound. The input kernel is nonnegative, so it can in particular be the entrywise norm of a Hermitian matrix.

theorem weighted_kernel_localized_square (B : ι → ι → ℝ)
    (g a : ι → ℝ) (c : ℝ) (hc : 0 ≤ c)
    (hB : ∀ i j, 0 ≤ B i j) (hg : ∀ i, 0 < g i) (ha : ∀ i, 0 ≤ a i)
    (hsymm : ∀ i j, B i j = B j i)
    (hlevel : ∀ i j, B i j ≠ 0 → a i = a j)
    (hrow : ∀ i, ∑ j, B i j * g j / g i ≤ c * a i)
    (v : ι → ℝ) :
    ∑ i, (∑ j, B i j * v j) ^ 2 ≤ c ^ 2 * ∑ i, (a i) ^ 2 * (v i) ^ 2 := by
…

theorem OAI.TwoPointCorrelations.weighted_matrix_localized_square line 92

Source documentation

The manuscript's localized square bound for a complex matrix.

theorem weighted_matrix_localized_square (A : ι → ι → ℂ)
    (g a : ι → ℝ) (c : ℝ) (hc : 0 ≤ c)
    (hg : ∀ i, 0 < g i) (ha : ∀ i, 0 ≤ a i)
    (hsymm : ∀ i j, ‖A i j‖ = ‖A j i‖)
    (hlevel : ∀ i j, A i j ≠ 0 → a i = a j)
    (hrow : ∀ i, ∑ j, ‖A i j‖ * g j / g i ≤ c * a i)
    (v : ι → ℂ) :
    ∑ i, ‖∑ j, A i j * v j‖ ^ 2 ≤ c ^ 2 * ∑ i, (a i) ^ 2 * ‖v i‖ ^ 2 := by
…

theorem OAI.TwoPointCorrelations.localized_square_sum line 111

Source documentation

Summing localized bounds only requires degree control where the vector is nonzero. This is the support condition supplied by v = E v.

theorem localized_square_sum (A : δ → ι → ι → ℂ) (a : δ → ι → ℝ)
    (c M : ℝ) (v : ι → ℂ)
    (hlocal : ∀ d, ∑ i, ‖∑ j, A d i j * v j‖ ^ 2 ≤
      c ^ 2 * ∑ i, (a d i) ^ 2 * ‖v i‖ ^ 2)
    (hdegree : ∀ i, v i ≠ 0 → ∑ d, (a d i) ^ 2 ≤ M) :
    ∑ d, ∑ i, ‖∑ j, A d i j * v j‖ ^ 2 ≤ c ^ 2 * M * ∑ i, ‖v i‖ ^ 2 := by
…

theorem OAI.TwoPointCorrelations.weighted_operator_norm_le line 133

Source documentation

Entrywise application identity lets the matrix estimate feed directly into the finite-dimensional Hilbert-space spectral transfer.

theorem weighted_operator_norm_le
    (T : EuclideanSpace ℂ ι →L[ℂ] EuclideanSpace ℂ ι)
    (A : ι → ι → ℂ) (hT : ∀ v i, T v i = ∑ j, A i j * v j)
    (g a : ι → ℝ) (c : ℝ) (hc : 0 ≤ c)
    (hg : ∀ i, 0 < g i) (ha : ∀ i, 0 ≤ a i) (ha1 : ∀ i, a i ≤ 1)
    (hsymm : ∀ i j, ‖A i j‖ = ‖A j i‖)
    (hlevel : ∀ i j, A i j ≠ 0 → a i = a j)
    (hrow : ∀ i, ∑ j, ‖A i j‖ * g j / g i ≤ c * a i) : ‖T‖ ≤ c := by
…