CavityGaussianRankGram.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Positive definiteness of finite Gaussian and normalized-frame windows.

theorem OAI.InvariantIsing.cavityGaussianRows_window_det_ne_zero line 16
Source documentation
Any consecutive square block of the iid Gaussian row sequence is nonsingular almost surely.
```
theorem cavityGaussianRows_window_det_ne_zero (q l : ℕ) :
    ∀ᵐ x ∂cavityGaussianRows q,
      Matrix.det (fun i j : Fin q => x (l + i) j) ≠ 0 := by
…
```
Mentions: OAI.InvariantIsing.cavityGaussianRows
lemma OAI.InvariantIsing.cavity_gram_posDef_of_minor line 46
lemma OAI.InvariantIsing.cavityWindowGram_mul line 61
def OAI.InvariantIsing.cavityMaskedRows line 67
lemma OAI.InvariantIsing.cavityWindowGram_eq_mask_gram line 71
lemma OAI.InvariantIsing.cavityWindowGram_posDef_of_minor line 87
theorem OAI.InvariantIsing.cavityGaussianRows_gram_posDef line 100
Source documentation
Positive definiteness holds at every admissible finite row count.
```
theorem cavityGaussianRows_gram_posDef (N q : ℕ) (hqN : q ≤ N) :
    ∀ᵐ x ∂cavityGaussianRows q, (cavityEmpiricalGram x N).PosDef := by
…
```
Mentions: OAI.InvariantIsing.cavityGaussianRows, OAI.InvariantIsing.cavityEmpiricalGram
lemma OAI.InvariantIsing.cavityGoodGram_probability_one line 127
theorem OAI.InvariantIsing.cavityGaussianRows_normalized_window_posDef line 137
Source documentation
Every window containing at least q rows is positive definite at finite volume, before and after the common Gram normalization.
```
theorem cavityGaussianRows_normalized_window_posDef (N q l u : ℕ)
    (hlq : l + q ≤ u) (huN : u ≤ N) :
    ∀ᵐ x ∂cavityGaussianRows q,
      (cavityWindowGram (cavityNormalizeFrame (cavityGaussianMatrix x N)) l u).PosDef := by
…
```
Mentions: OAI.InvariantIsing.cavityGaussianRows, OAI.InvariantIsing.cavityWindowGram, OAI.InvariantIsing.cavityNormalizeFrame, OAI.InvariantIsing.cavityGaussianMatrix