CavityGaussianRank.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Almost-sure nonsingularity of the fixed-width iid Gaussian block.

lemma OAI.InvariantIsing.gaussian_pi_extract_law line 13

lemma OAI.InvariantIsing.gaussian_pi_update_law line 26

Source documentation

Replacing one coordinate by a fresh standard Gaussian preserves the finite iid Gaussian law. The unused old coordinate causes no problem.

private lemma gaussian_pi_update_law {I : Type*} [Fintype I] [DecidableEq I] (i : I) :
    ((Measure.pi (fun _ : I => gaussianReal 0 1)).prod (gaussianReal 0 1)).map
      (fun p : (I → ℝ) × ℝ => Function.update p.1 i p.2) =
        Measure.pi (fun _ : I => gaussianReal 0 1) := by
…

lemma OAI.InvariantIsing.determinant_update_corner_affine line 64
lemma OAI.InvariantIsing.gaussian_affine_ne_zero line 92
theorem OAI.InvariantIsing.cavityGaussianSquare_det_ne_zero line 105
Source documentation
A square matrix with independent standard Gaussian entries is nonsingular almost surely, including the empty-matrix convention.
```
theorem cavityGaussianSquare_det_ne_zero (n : ℕ) :
    ∀ᵐ x ∂Measure.pi (fun _ : Fin n × Fin n => gaussianReal 0 1),
      Matrix.det (fun i j => x (i, j)) ≠ 0 := by
…
```
theorem OAI.InvariantIsing.cavityGaussianRows_square_det_ne_zero line 148
Source documentation
The concrete first q iid Gaussian rows used by the frame construction are full rank almost surely.
```
theorem cavityGaussianRows_square_det_ne_zero (q : ℕ) :
    ∀ᵐ x ∂cavityGaussianRows q,
      Matrix.det (fun i j : Fin q => x i j) ≠ 0 := by
…
```
Mentions: OAI.InvariantIsing.cavityGaussianRows