CavityBlockFactor.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-volume algebra for the coupled cavity comparison. The spectral coupling and its Gaussian limit are separate source obligations.

def OAI.InvariantIsing.cavityQuadratic line 15
def OAI.InvariantIsing.cavityLogFactor line 18
lemma OAI.InvariantIsing.cavityQuadratic_sub line 24

theorem OAI.InvariantIsing.cavity_block_factor line 30

Source documentation

The exact exponent difference in cav:factor, with no commutativity assumption on the two symmetric special-coordinate blocks.

theorem cavity_block_factor {d n : ℕ} (A A0 : Matrix (Fin d) (Fin d) ℝ)
    (L : Matrix (Fin d) (Fin n) ℝ) (C : Matrix (Fin n) (Fin n) ℝ)
    (y : Fin d → ℝ) (ε : Spin n) :
    (1 / 2 : ℝ) * (∑ i : Fin d ⊕ Fin n, ∑ j : Fin d ⊕ Fin n,
      Sum.elim y (fun a => spinValue (ε a)) i *
        (Matrix.fromBlocks A L L.transpose C) i j *
        Sum.elim y (fun a => spinValue (ε a)) j) - cavityQuadratic A0 y =
      cavityLogFactor (A - A0) L C y ε := by
…

Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinValue, OAI.InvariantIsing.cavityQuadratic, OAI.InvariantIsing.cavityLogFactor

def OAI.InvariantIsing.cavityFactorMean line 57
Source documentation
The base Gibbs law times the independent uniform probability on the cavity cube, evaluated on the positive cavity factor.
```
def cavityFactorMean {N n : ℕ} (H : Spin N → ℝ) (V : Spin N → Spin n → ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.Spin
lemma OAI.InvariantIsing.cavityFactorMean_eq_gibbsAverage line 61
lemma OAI.InvariantIsing.cavityFactorMean_eq_ratio line 71
lemma OAI.InvariantIsing.cavityFactorMean_pos line 82
theorem OAI.InvariantIsing.logPartition_cavity_increment line 90
Source documentation
Exact finite log-partition increment for probability-normalized partition functions, at the base endpoint of the cavity interpolation.
```
theorem logPartition_cavity_increment {N n : ℕ} (H : Spin N → ℝ)
    (V : Spin N → Spin n → ℝ) :
    logPartition (fun x : Spin N × Spin n => H x.1 + V x.1 x.2) - logPartition H =
      Real.log (cavityFactorMean H V) := by
…
```
Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.logPartition, OAI.InvariantIsing.cavityFactorMean
theorem OAI.InvariantIsing.logPartition_cavityBlock_increment line 105