J_log_error_bound

formal source

  72/-- The quartic error bound. For |ε| < 1, the error in the
  73    quadratic approximation is bounded by ε⁴/24.
  74    This is the standard Taylor remainder for cosh. -/
  75def J_log_error_bound (ε : ℝ) : ℝ := |ε| ^ 4 / 24
  76
  77/-! ## The Coupling Cost
  78
  79The cost of a mismatch between neighboring simplices. -/
  80
  81/-- The coupling cost between two simplices with log-potentials ε₁, ε₂.
  82    J(ψ₁/ψ₂) = J(e^(ε₁−ε₂)) ≈ (ε₁−ε₂)²/2 at leading order. -/
  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