Main.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BufferedIsing.dssMatrix line 14
Source documentation
The oriented pair matrix is precisely the original edge-list interaction; parallel edges are summed, with no ghost and no change to the field.
```
def dssMatrix {n m : ℕ} (G : FiniteGraph n m) (u v : Fin n) : ℝ :=
…
```
Mentions: OAI.BufferedIsing.FiniteGraph
lemma OAI.BufferedIsing.dssMatrix_nonneg line 17
lemma OAI.BufferedIsing.dss_hamiltonian_eq line 23
lemma OAI.BufferedIsing.dss_mass_eq line 40
lemma OAI.BufferedIsing.dss_average_eq line 44
theorem OAI.BufferedIsing.arbitraryFieldCovarianceBound line 50
Source documentation
The arbitrary-field covariance bound for the finite edge-list Gibbs law, including equal sites.
```
theorem arbitraryFieldCovarianceBound : ArbitraryFieldCovarianceBound := by
…
```
Mentions: OAI.BufferedIsing.ArbitraryFieldCovarianceBound
theorem OAI.BufferedIsing.effectiveCouplingBound line 56
lemma OAI.BufferedIsing.extremeLogOdds_le_zero line 59

theorem OAI.BufferedIsing.finite_graph_comparison line 72

Source documentation

Finite-graph comparison for arbitrary probability mixtures on both sides. Dirac mixtures recover the conditional laws.

Distinct definitions of this name: ComparatorChallenges/BufferedIsing.lean:98 (same statement text; different proof or body). Qualify references as OAI.BufferedIsing.finite_graph_comparison@path.

theorem finite_graph_comparison {n m : ℕ} (G : FiniteGraph n m)
    (h : Fin n → ℝ) (I J F : Finset (Fin n))
    (hIJ : Disjoint I J) (hIF : Disjoint I F) (hJF : Disjoint J F)
    (i j : KeptVertex F) (hi : i.val ∈ I) (hj : j.val ∈ J)
    (a τ : Spins n) (mix mix' : Spins n → ℝ)
    (hmix : ∀ b, 0 ≤ mix b) (hmix' : ∀ b, 0 ≤ mix' b)
    (hmixsum : ∑ b, mix b = 1) (hmix'sum : ∑ b, mix' b = 1) :
    Real.exp (-4 * Real.artanh (qZero G I J F i j)) ≤
        mixtureProb G h I J F a τ mix / mixtureProb G h I J F a τ mix' ∧
      mixtureProb G h I J F a τ mix / mixtureProb G h I J F a τ mix' ≤
        Real.exp (4 * Real.artanh (qZero G I J F i j)) := by
…

Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.Spins, OAI.BufferedIsing.qZero, OAI.BufferedIsing.mixtureProb