pith. machine review for the scientific record. sign in
structure definition def or abbrev

WeakFieldReggeData

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)

 279structure WeakFieldReggeData (n : ℕ) where
 280  dArea : Fin n → Fin n → ℝ
 281  dDeficit : Fin n → Fin n → ℝ
 282  dArea_symm : ∀ i j, dArea i j = dArea j i
 283  dDeficit_symm : ∀ i j, dDeficit i j = dDeficit j i
 284
 285/-- The bilinear coefficient matrix induced by the linearization data:
 286    `M_{ij} = dArea_{ij} · dDeficit_{ij}` (the entry-wise product
 287    that appears in `S^(2) = Σ A^(1) δ^(1)` after the conformal
 288    expansion).
 289
 290    This is symmetric because both factors are symmetric. -/

used by (15)

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

depends on (9)

Lean names referenced from this declaration's body.