coupling_quadratic

formal source

  83def coupling_cost (ε₁ ε₂ : ℝ) : ℝ := Jcost (Real.exp (ε₁ - ε₂))
  84
  85/-- The quadratic approximation of the coupling cost. -/
  86def coupling_quadratic (ε₁ ε₂ : ℝ) : ℝ := (ε₁ - ε₂) ^ 2 / 2
  87
  88/-! ## Discrete Laplacian Structure
  89
  90The quadratic J-cost coupling is a discrete Laplacian action.
  91On a simplicial complex with N simplices and adjacency weights w_ij:
  92
  93  S_quadratic = (1/2) Σ_{i~j} w_ij · (ε_i − ε_j)²
  94
  95This is the standard graph Laplacian energy. -/
  96
  97/-- A weighted simplicial graph representing the ledger. -/
  98structure WeightedLedgerGraph (n : ℕ) where
  99  weight : Fin n → Fin n → ℝ
 100  weight_nonneg : ∀ i j, 0 ≤ weight i j
 101  weight_symm : ∀ i j, weight i j = weight j i
 102
 103/-- The discrete Laplacian action (= quadratic J-cost) on the graph. -/
 104def laplacian_action {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) : ℝ :=
 105  (1 / 2) * ∑ i : Fin n, ∑ j : Fin n, G.weight i j * (ε i - ε j) ^ 2
 106
 107/-- The discrete Laplacian of ε at vertex i:
 108    (Δε)_i = Σ_j w_ij · (ε_i − ε_j) -/
 109def discrete_laplacian {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) (i : Fin n) : ℝ :=
 110  ∑ j : Fin n, G.weight i j * (ε i - ε j)
 111
 112/-- Stationarity of the Laplacian action implies the discrete Laplacian vanishes.
 113    This is: δS/δε_i = 0 ⟺ (Δε)_i = 0 for all i. -/
 114theorem stationarity_iff_laplacian_zero {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) :
 115    (∀ i, discrete_laplacian G ε i = 0) →
 116    ∀ i, ∑ j : Fin n, G.weight i j * (ε i - ε j) = 0 := by