PolynomialFiniteAssembly.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite polynomial families can be padded to a common degree and added without changing their values or their smooth-coefficient property.

lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_sumFinset line 16
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.sum_fin_zero_extension line 27
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.padTensorPolynomial line 49
Source documentation
Higher unused powers have the actual zero expression as coefficient.
```
def padTensorPolynomial {n N : ℕ} (P : Fin 3 → Fin n → Expression) :
    Fin 3 → Fin N → Expression :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.padTensorPolynomial_smooth line 53
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.padTensorPolynomial_value line 61
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.polynomialFamilyDegree line 83
Source documentation
The largest number of powers in a finite dependent family.
```
def polynomialFamilyDegree {ι : Type*} [Fintype ι] (n : ι → ℕ) : ℕ :=
…
```
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.le_polynomialFamilyDegree line 86
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.sumTensorPolynomials line 92
Source documentation
Add the coefficient expressions after padding every member to the same degree. No map or perturbation parameter enters this construction.
```
def sumTensorPolynomials {ι : Type*} [Fintype ι] {n : ι → ℕ}
    (P : (i : ι) → Fin 3 → Fin (n i) → Expression) :
    Fin 3 → Fin (polynomialFamilyDegree n) → Expression :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.polynomialFamilyDegree
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.sumTensorPolynomials_smooth line 97
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.sumTensorPolynomials_value line 106