MRTSparseGram.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite duality for sparse Dirichlet-polynomial samples. The analytic input is an explicit Gram-row sum, with no density-to-energy substitution.

lemma OAI.TwoPointCorrelations.mrt_gram_synthesis line 14

theorem OAI.TwoPointCorrelations.mrt_gram_analysis line 43

Source documentation

Finite Bessel inequality with an absolute Gram-row bound.

theorem mrt_gram_analysis {ι E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℂ E] (S : Finset ι) (v : ι → E) (u : E)
    {B : ℝ} (hB : 0 ≤ B) (hrow : ∀ i ∈ S, ∑ j ∈ S, ‖inner ℂ (v i) (v j)‖ ≤ B) :
    (∑ i ∈ S, ‖inner ℂ (v i) u‖^2) ≤ B * ‖u‖^2 := by
…

theorem OAI.TwoPointCorrelations.mrt_finite_matrix_gram line 80

Source documentation

The Gram kernel is evaluated on the actual coefficient matrix.

theorem mrt_finite_matrix_gram {ι κ : Type*} (S : Finset ι) (K : Finset κ)
    (A : ι → κ → ℂ) (a : κ → ℂ) {B : ℝ} (hB : 0 ≤ B)
    (hrow : ∀ i ∈ S, ∑ j ∈ S, ‖∑ n ∈ K, A i n * conj (A j n)‖ ≤ B) :
    (∑ i ∈ S, ‖∑ n ∈ K, A i n * a n‖^2) ≤ B * ∑ n ∈ K, ‖a n‖^2 := by
…