PinnedMarginal.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BufferedIsing.contractedPinnedWeight line 12
Source documentation
The actual contracted marginal retains arbitrary fields and all effects of the common pins. It is distinct from the zero-field comparison weight.
```
noncomputable def contractedPinnedWeight {n m : ℕ} (G : FiniteGraph n m)
    (h : Fin n → ℝ) (I J F : Finset (Fin n)) (τ : Spins n)
    (σ : KeptVertex F → Bool) : ℝ :=
…
```
Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins, OAI.BufferedIsing.KeptVertex
lemma OAI.BufferedIsing.respects_terminals_iff line 17
lemma OAI.BufferedIsing.contracted_prescription_iff line 37
lemma OAI.BufferedIsing.pairTable_contractedPinned line 67
Source documentation
Identifying each terminal set separately is exactly restriction to its constant configurations; no new model comparison enters this identity.
```
lemma pairTable_contractedPinned {n m : ℕ} (G : FiniteGraph n m)
    (h : Fin n → ℝ) (I J F : Finset (Fin n))
    (hIF : Disjoint I F) (hJF : Disjoint J F)
    (i j : KeptVertex F) (hi : i.val ∈ I) (hj : j.val ∈ J)
    (τ : Spins n) (s t : Bool) :
    pairTable (contractedPinnedWeight G h I J F τ) i j s t =
      jointWeight G h I J F τ (fun _ => s) (fun _ => t) := by
…
```
Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.Spins, OAI.BufferedIsing.pairTable, OAI.BufferedIsing.contractedPinnedWeight, OAI.BufferedIsing.jointWeight
lemma OAI.BufferedIsing.extremeLogOdds_eq_effective line 98
lemma OAI.BufferedIsing.sum_pin_incidence line 111
def OAI.BufferedIsing.pinField line 144
Source documentation
The finite-field contribution induced by the actual prescribed spins. Neither these induced fields nor the original fields survive in qZero.
```
noncomputable def pinField {n m : ℕ} (G : FiniteGraph n m)
    (h : Fin n → ℝ) (F : Finset (Fin n)) (τ : Spins n) (v : KeptVertex F) : ℝ :=
…
```
Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins, OAI.BufferedIsing.KeptVertex
def OAI.BufferedIsing.pinConstant line 153
Source documentation
Field and bond terms depending only on fixed sites. They cancel from all normalized laws, but recording them makes the elimination exact.
```
noncomputable def pinConstant {n m : ℕ} (G : FiniteGraph n m)
    (h : Fin n → ℝ) (F : Finset (Fin n)) (τ : Spins n) : ℝ :=
…
```
Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins
lemma OAI.BufferedIsing.energy_pin_expansion line 159
lemma OAI.BufferedIsing.sum_kept line 218
lemma OAI.BufferedIsing.energy_pinExtension line 227
Source documentation
Exact deletion of fixed sites: their incident bonds become finite real fields, while only bonds with two free endpoints remain as interactions.
```
lemma energy_pinExtension {n m : ℕ} (G : FiniteGraph n m)
    (h : Fin n → ℝ) (F : Finset (Fin n)) (τ : Spins n) (σ : KeptVertex F → Bool) :
    energy G h (pinExtension F τ σ) = pinConstant G h F τ +
      deletedEnergy G F σ + ∑ v : KeptVertex F, pinField G h F τ v * spin (σ v) := by
…
```
Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.energy, OAI.BufferedIsing.pinExtension, OAI.BufferedIsing.pinConstant, OAI.BufferedIsing.deletedEnergy, OAI.BufferedIsing.pinField, OAI.BufferedIsing.spin
lemma OAI.BufferedIsing.weight_pinExtension line 253