def definition def or abbrev

`dirichletForm`

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

formal statement (Lean)

 169def dirichletForm {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) : ℝ :=

Definition body.

 170  (1 / 2) * ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
 171
 172/-- The bilinear form: `Q[ξ; M] = Σ_{i,j} M_{ij} ξ_i ξ_j`. -/

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

dirichlet_eq_neg_quadratic in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
dirichletForm_diag_irrelevant in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
dirichletForm_edgeArea in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
dirichletForm_edgeArea_laplacianReggeData in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
dirichlet_form_eq_neg_quadratic in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
dirichletForm_flat in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
dirichletForm_neg in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
secondOrder_eq_half_laplacian_action in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
weak_field_conformal_reduction in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
weak_field_conformal_reduction_kappa in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
weak_field_conformal_reduction_laplacianData in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
weak_field_conformal_reduction_laplacianData_kappa in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
WeakFieldConformalReggeCert in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use

Lean names referenced from this declaration's body.

LogPotential in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use