PolynomialBlocks.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coefficient blocks with positive and zero degrees

def OAI.Nagata.Workers.W10.boundedCoefficientPolynomials line 21
Source documentation
Genuine bounded polynomials, with each coefficient in its specified submodule.
```
def boundedCoefficientPolynomials (u : ℕ) (S : ℕ → Submodule R A) :
    Submodule R (Polynomial A) where
…
```
def OAI.Nagata.Workers.W10.boundedPolynomialCoordinates line 37
Source documentation
Read the complete finite tuple of actual coefficients.
```
def boundedPolynomialCoordinates (u : ℕ) (S : ℕ → Submodule R A) :
    boundedCoefficientPolynomials u S →ₗ[R] ((j : Fin (u + 1)) → S j.val) where
…
```
Mentions: OAI.Nagata.Workers.W10.boundedCoefficientPolynomials
theorem OAI.Nagata.Workers.W10.boundedPolynomialCoordinates_injective line 43
def OAI.Nagata.Workers.W10.finiteCoefficientPolynomial line 54
Source documentation
Synthesize the polynomial from its finite tuple of actual coefficients.
```
def finiteCoefficientPolynomial (u : ℕ) (S : ℕ → Submodule R A)
    (a : (j : Fin (u + 1)) → S j.val) : Polynomial A :=
…
```
theorem OAI.Nagata.Workers.W10.finiteCoefficientPolynomial_coeff line 58
theorem OAI.Nagata.Workers.W10.finiteCoefficientPolynomial_coeff_above line 65
theorem OAI.Nagata.Workers.W10.boundedPolynomialCoordinates_surjective line 75
def OAI.Nagata.Workers.W10.boundedPolynomialEquiv line 93
Source documentation
The direct product description is a proved linear equivalence.
```
def boundedPolynomialEquiv (u : ℕ) (S : ℕ → Submodule R A) :
    boundedCoefficientPolynomials u S ≃ₗ[R] ((j : Fin (u + 1)) → S j.val) :=
…
```
Mentions: OAI.Nagata.Workers.W10.boundedCoefficientPolynomials
def OAI.Nagata.Workers.W10.boundedPolynomialBasis line 99
Source documentation
Bases of coefficient subspaces assemble into a basis of genuine polynomials.
```
def boundedPolynomialBasis (u : ℕ) (S : ℕ → Submodule R A)
    (I : Fin (u + 1) → Type*) (b : ∀ j, Basis (I j) R (S j.val)) :
    Basis (Σ j, I j) R (boundedCoefficientPolynomials u S) :=
…
```
Mentions: OAI.Nagata.Workers.W10.boundedCoefficientPolynomials

theorem OAI.Nagata.Workers.W10.boundedPolynomialBasis_coeff line 105

Source documentation

The assembled basis has precisely one nonzero polynomial coefficient.

theorem boundedPolynomialBasis_coeff (u : ℕ) (S : ℕ → Submodule R A)
    (I : Fin (u + 1) → Type*) (b : ∀ j, Basis (I j) R (S j.val))
    (j : Fin (u + 1)) (i : I j) (k : Fin (u + 1)) :
    ((boundedPolynomialBasis u S I b ⟨j, i⟩).val).coeff k.val =
      ((Pi.single (M := fun k : Fin (u + 1) => S k.val) j (b j i)) k).val := by
…

Mentions: OAI.Nagata.Workers.W10.boundedPolynomialBasis

theorem OAI.Nagata.Workers.W10.boundedPolynomialBasis_as_monomial line 116

Source documentation

Each actual polynomial basis vector is the indicated coefficient times X^j.

theorem boundedPolynomialBasis_as_monomial (u : ℕ) (S : ℕ → Submodule R A)
    (I : Fin (u + 1) → Type*) (b : ∀ j, Basis (I j) R (S j.val))
    (j : Fin (u + 1)) (i : I j) :
    (boundedPolynomialBasis u S I b ⟨j, i⟩).val =
      Polynomial.monomial j.val (b j i).val := by
…

Mentions: OAI.Nagata.Workers.W10.boundedPolynomialBasis