CavityFiniteRoot.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The projected root covariance for the actual finite spectral cavity blocks. All determinant conditions follow from the positive spectral gap.

lemma OAI.InvariantIsing.cavity_finite_base_shift_isUnit line 15
lemma OAI.InvariantIsing.cavity_finite_compressed_shift_isUnit line 33

lemma OAI.InvariantIsing.cavity_finite_tilt_isUnit line 57

Source documentation

The finite cavity tilt is invertible at every positive deficit.

lemma cavity_finite_tilt_isUnit {m d n : ℕ}
    (rho lam : Fin m → ℝ) (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
    (B : Matrix (Fin (m * n)) (Fin d) ℝ) (hB : B.transpose * B = 1)
    (g : Fin d → Fin m) (x : ℝ) (hx : 0 < x) :
    let A := B.transpose * cavityRepeatedSpectrum (n := n) lam * B
…

Mentions: OAI.InvariantIsing.cavityRepeatedSpectrum

lemma OAI.InvariantIsing.cavity_finite_projected_resolvent line 85

Source documentation

The projected resolvent of the finite cavity tilt has the prescribed finite-law scalar field value.

lemma cavity_finite_projected_resolvent {m d n : ℕ}
    (rho lam : Fin m → ℝ) (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
    (B : Matrix (Fin (m * n)) (Fin d) ℝ) (hB : B.transpose * B = 1)
    (hBE : B.transpose * cavityLimitingStack (n := n) rho = 0)
…

Mentions: OAI.InvariantIsing.cavityLimitingStack

theorem OAI.InvariantIsing.cavity_finite_projected_root_covariance line 109
Source documentation
The source root derivative evaluated on the actual repeated-spectrum special/cavity blocks. The base multiplicity map is arbitrary, so this also applies after deleting the cavity eigenvectors from each group.
```
theorem cavity_finite_projected_root_covariance {m d n : ℕ}
    (rho lam : Fin m → ℝ) (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
    (B : Matrix (Fin (m * n)) (Fin d) ℝ) (hB : B.transpose * B = 1)
    (hBE : B.transpose * cavityLimitingStack (n := n) rho = 0)
…
```
Mentions: OAI.InvariantIsing.cavityLimitingStack