CoefficientSpaces.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Coefficient spaces of restricted normal polynomials

def OAI.Nagata.CoefficientSpaces.multiplyPower line 20
Source documentation
Multiplication by a fixed function power is a linear map on actual functions.
```
noncomputable def multiplyPower (P : ℂ → ℂ) (e : ℕ) :
    (ℂ → ℂ) →ₗ[ℂ] (ℂ → ℂ) where
…
```
theorem OAI.Nagata.CoefficientSpaces.multiplyPower_apply line 26

theorem OAI.Nagata.CoefficientSpaces.multiplyPower_mem_sections line 31

Source documentation

Multiplication by a genuine holomorphic automorphic section has exactly the tensor-product transition multiplier and degree.

theorem multiplyPower_mem_sections {τ γ δ : ℂ} {n s : ℤ} {P f : ℂ → ℂ}
    (hP : P ∈ Nagata.W08.automorphicSections τ s δ)
    (hf : f ∈ Nagata.W08.automorphicSections τ n γ) (e : ℕ) :
    multiplyPower P e f ∈ Nagata.W08.automorphicSections τ
      (n + (e : ℤ) * s) (γ * δ ^ e) := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.multiplyPower

def OAI.Nagata.CoefficientSpaces.normalMinusMarkedMultiplier line 51
Source documentation
The multiplier of A=L^3⊗O(-P), in fixed covering-space frames.
```
noncomputable def normalMinusMarkedMultiplier (γL γP : ℂ) : ℂ := γL ^ 3 / γP
```
def OAI.Nagata.CoefficientSpaces.coefficientSpace line 55
Source documentation
Coefficient block V_j of the actual polynomial space W_tau. Parameters d,m,j are integers, so tensor exponents remain integer powers as in the source.
```
noncomputable def coefficientSpace (τ γL γP : ℂ) (d m j : ℤ) (P : ℂ → ℂ) :
    Submodule ℂ (ℂ → ℂ) :=
…
```

theorem OAI.Nagata.CoefficientSpaces.mem_coefficientSpace_second line 65

Source documentation

Membership in the second block means an actual section multiplied by P^(j-m).

theorem mem_coefficientSpace_second {τ γL γP : ℂ} {d m j : ℤ} {P g : ℂ → ℂ}
    (hj : m < j) :
    g ∈ coefficientSpace τ γL γP d m j P ↔
      ∃ f ∈ Nagata.W08.automorphicSections τ (3 * (d - 3 * j))
        (γL ^ (d - 3 * j)), multiplyPower P (j - m).toNat f = g := by
…

Mentions: OAI.Nagata.CoefficientSpaces.coefficientSpace, OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.multiplyPower

theorem OAI.Nagata.CoefficientSpaces.coefficientSpace_differentiableAt line 75
Source documentation
Every coefficient is genuinely holomorphic off zero. The positive-index branch inherits this from its source section and the marked product.
```
theorem coefficientSpace_differentiableAt {τ γL γP : ℂ} {d m j : ℤ}
    {P f : ℂ → ℂ}
    (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
    (hf : f ∈ coefficientSpace τ γL γP d m j P) {z : ℂ} (hz : z ≠ 0) :
    DifferentiableAt ℂ f z := by
…
```
Mentions: OAI.Nagata.CoefficientSpaces.coefficientSpace
theorem OAI.Nagata.CoefficientSpaces.coefficientSpace_zero_value line 87
Source documentation
The forced zero value at the omitted point introduces no extra coefficient.
```
theorem coefficientSpace_zero_value {τ γL γP : ℂ} {d m j : ℤ}
    {P f : ℂ → ℂ} (hf : f ∈ coefficientSpace τ γL γP d m j P) : f 0 = 0 := by
…
```
Mentions: OAI.Nagata.CoefficientSpaces.coefficientSpace
def OAI.Nagata.CoefficientSpaces.polynomialSections line 99
Source documentation
Actual finite-degree polynomials in the fibre coordinate with coefficients in the above spaces. The degree bound is imposed coefficientwise and therefore includes the zero polynomial without a special degree convention.
```
noncomputable def polynomialSections (τ γL γP : ℂ) (d m : ℤ) (P : ℂ → ℂ) :
    Submodule ℂ (Polynomial (ℂ → ℂ)) where
…
```
def OAI.Nagata.CoefficientSpaces.scalarExpression line 125
Source documentation
The scalar expression of an actual polynomial section in the covering frame.
```
noncomputable def scalarExpression (F : Polynomial (ℂ → ℂ)) (z v : ℂ) : ℂ :=
…
```
theorem OAI.Nagata.CoefficientSpaces.polynomialSections_ext line 129
Source documentation
Equality of every actual coefficient is equality of polynomial sections.
```
theorem polynomialSections_ext {τ γL γP : ℂ} {d m : ℤ} {P : ℂ → ℂ}
    (F G : polynomialSections τ γL γP d m P)
    (h : ∀ j, F.val.coeff j = G.val.coeff j) : F = G := by
…
```
Mentions: OAI.Nagata.CoefficientSpaces.polynomialSections