AlgebraDefs.lean`

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Polynomial spaces, interpolation weights, crossing tensors, and support evaluation.

abbrev OAI.Paper170.Poly2 line 25
abbrev OAI.Paper170.Poly4 line 26
def OAI.Paper170.nodeWeight line 28
def OAI.Paper170.omittedNodePolynomial line 31
def OAI.Paper170.rectangle line 35
def OAI.Paper170.box4 line 39
def OAI.Paper170.swapFirstPair line 42
def OAI.Paper170.swapSecondPair line 45
def OAI.Paper170.endpointSymmetricSpace line 48
def OAI.Paper170.evalTwo line 52
def OAI.Paper170.evalFour line 55
def OAI.Paper170.evenTriangle line 59
Source documentation
The manuscript's one-based L_s, translated to zero-based Fin indices.
```
def evenTriangle (s : ℕ) : Finset (Fin (2 * s) × Fin (2 * s)) :=
…
```
abbrev OAI.Paper170.EvenTriangleCoord line 63
def OAI.Paper170.triangleEvaluation line 65
def OAI.Paper170.halfOrder line 70
def OAI.Paper170.weightedPairing line 74
def OAI.Paper170.orderPairing line 80
abbrev OAI.Paper170.CrossingTensor line 84
def OAI.Paper170.chainBoundary line 86
def OAI.Paper170.chainPairing line 89
def OAI.Paper170.polynomialTest line 93
def OAI.Paper170.supportedPairs line 99
Source documentation
Canonical orientation within each edge; the two edges remain ordered.
```
def supportedPairs {n : ℕ} (J : CrossingTensor n) :
    Finset ((Fin n × Fin n) × (Fin n × Fin n)) :=
…
```
Mentions: OAI.Paper170.CrossingTensor
abbrev OAI.Paper170.SupportCoord line 107
def OAI.Paper170.supportEvaluation line 109
def OAI.Paper170.collisionFactor line 115
Source documentation
C=(x-y)(x-v)(u-y)(u-v), with coordinates x,u,y,v.
```
def collisionFactor : Poly4 :=
…
```
Mentions: OAI.Paper170.Poly4
def OAI.Paper170.fullDifference line 122
Source documentation
The complete six-difference product in the source's stated order.
```
def fullDifference : Poly4 :=
…
```
Mentions: OAI.Paper170.Poly4
def OAI.Paper170.vertexSpecialization line 127
Source documentation
Substitute x=y=t, leaving u,v as the two variables.
```
def vertexSpecialization (t : ℝ) : Poly4 →ₐ[ℝ] Poly2 :=
…
```
Mentions: OAI.Paper170.Poly4, OAI.Paper170.Poly2
def OAI.Paper170.diagonalSpecialization line 132
Source documentation
Substitute y=x, leaving x,u,v as three variables.
```
def diagonalSpecialization : Poly4 →ₐ[ℝ] MvPolynomial (Fin 3) ℝ :=
…
```
Mentions: OAI.Paper170.Poly4
def OAI.Paper170.supportDiagonal line 136
def OAI.Paper170.supportBilinear line 144
def OAI.Paper170.weightedChain line 148
def OAI.Paper170.collisionFactors line 151
def OAI.Paper170.liftUnivariate line 157
def OAI.Paper170.liftBivariate line 160
def OAI.Paper170.localTestPolynomial line 163