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

pairEventAt

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)

 270def pairEventAt {siteCount : ℕ} (ns : IncompressibleNSOperator siteCount)
 271    (i : Fin siteCount) : PairEvent where
 272  amplitude := ns.pairAmplitude i

proof body

Definition body.

 273  stretchFactor := ns.pairStretchFactor i
 274  amplitude_pos := ns.pairAmplitude_pos i
 275  stretchFactor_pos := ns.pairStretchFactor_pos i
 276

used by (4)

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

depends on (4)

Lean names referenced from this declaration's body.