CavitySchurLogDeterminant.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite spectral multiplicity bookkeeping for cav:determinant. The diagonal comparison block has n-s_a copies of eigenvalue a.

lemma OAI.InvariantIsing.cavity_labeledSpectrum_determinant line 13
lemma OAI.InvariantIsing.cavity_missing_multiplicity_product line 28

theorem OAI.InvariantIsing.cavity_schur_tilt_det_multiplicity line 42

Source documentation

The full finite multiplicity cancellation: the determinant ratio is x^n ∏_a (b-λ_a)^s_a, before taking its logarithm.

theorem cavity_schur_tilt_det_multiplicity {d n m : ℕ}
    (A : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
    (C : Matrix (Fin n) (Fin n) ℝ) (g : Fin d → Fin m)
    (lam : Fin m → ℝ) (s : Fin m → ℕ) (hs : ∀ a, s a ≤ n)
    (hcounts : ∀ a, (Finset.univ.filter (fun i => g i = a)).card = n - s a)
    (b x : ℝ) (hx : x ≠ 0) (hb : ∀ a, lam a < b)
    (hA : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det)
    (hM : IsUnit (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C).det)
    (hcompression : ((b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C)⁻¹).toBlocks₂₂ = x • 1)
    (hfull : (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
…

theorem OAI.InvariantIsing.cavity_log_multiplicity_product line 71

Source documentation

Logarithmic multiplicity form used in the final cavity evaluation.

theorem cavity_log_multiplicity_product {m : ℕ}
    (lam rho : Fin m → ℝ) (s : Fin m → ℕ) (n : ℕ)
    (hrho : ∀ a, (s a : ℝ) = (n : ℝ) * rho a)
    (b x : ℝ) (hx : 0 < x) (hb : ∀ a, lam a < b) :
    Real.log (x ^ n * ∏ a, (b - lam a) ^ s a) =
      (n : ℝ) * (Real.log x + ∑ a, rho a * Real.log (b - lam a)) := by
…