pith. machine review for the scientific record. sign in
theorem proved tactic proof

dirichletForm_edgeArea

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 378theorem dirichletForm_edgeArea
 379    {n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) :
 380    dirichletForm (edgeArea W) ε
 381      = - dirichletForm (bilinearCoefficient W) ε := by

proof body

Tactic-mode proof.

 382  have h := dirichletForm_neg (bilinearCoefficient W) ε
 383  -- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`.
 384  exact h
 385
 386/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).**
 387
 388    Under the Schläfli row-sum hypothesis (§3) on the linearization
 389    data `W`, the second-order Regge action equals the discrete
 390    Dirichlet energy on the conformal mode `ε`, with edge weights
 391    `A_{ij} = − dArea_{ij} · dDeficit_{ij}`:
 392
 393        secondOrderReggeAction W ε
 394            = (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij}
 395            = ½ · dirichletForm A ε.
 396
 397    Multiplying through by `1/κ` recovers Jon's equation (d):
 398
 399        S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
 400
 401    Proof:
 402    1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`.
 403    2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum.
 404    3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε`
 405       by `dirichlet_eq_neg_quadratic` (§2).
 406    4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε`
 407       by `dirichletForm_edgeArea`.
 408    Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D)
 409                  = (1/2) · dirichletForm (edgeArea W) ε = RHS`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (28)

Lean names referenced from this declaration's body.