OAI/AlgebraicGeometry/PlaneCurves/ThetaPolynomialBases.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Nagata.Workers.W10.polynomialSectionCoordinates line 21
2. theorem OAI.Nagata.Workers.W10.polynomialSectionCoordinates_apply line 27
3. def OAI.Nagata.Workers.W10.polynomialSectionBasisFromCoefficients line 34

   Source documentation

   Conditional assembly from actual block coefficient maps and actual delta vectors. Each analytic input is exposed; no branch basis is supplied as a field.

   def polynomialSectionBasisFromCoefficients (τ γL γP : ℂ) (d m : ℤ) (P : ℂ → ℂ)
       (I : Fin ((d / 3).toNat + 1) → Type*) [∀ j, Fintype (I j)] [∀ j, DecidableEq (I j)]
       (c : ∀ j, coefficientSpace τ γL γP d m (j.val : ℤ) P →ₗ[ℂ] (I j → ℂ))
       (hc : ∀ j, Function.Injective (c j))
       (v : ∀ j, I j → coefficientSpace τ γL γP d m (j.val : ℤ) P)
       (hv : ∀ j i, c j (v j i) = Pi.single i 1) :
       Basis (Σ j, I j) ℂ (polynomialSections τ γL γP d m P) :=
   …

4. theorem OAI.Nagata.Workers.W10.polynomialSectionBasis_as_monomial line 46

   Source documentation

   Every basis vector is the literal fiber monomial with its actual block section.

   theorem polynomialSectionBasis_as_monomial (τ γL γP : ℂ) (d m : ℤ) (P : ℂ → ℂ)
       (I : Fin ((d / 3).toNat + 1) → Type*) [∀ j, Fintype (I j)] [∀ j, DecidableEq (I j)]
       (c : ∀ j, coefficientSpace τ γL γP d m (j.val : ℤ) P →ₗ[ℂ] (I j → ℂ))
       (hc : ∀ j, Function.Injective (c j))
       (v : ∀ j, I j → coefficientSpace τ γL γP d m (j.val : ℤ) P)
       (hv : ∀ j i, c j (v j i) = Pi.single i 1)
       (j : Fin ((d / 3).toNat + 1)) (i : I j) :
       (polynomialSectionBasisFromCoefficients τ γL γP d m P I c hc v hv ⟨j, i⟩).val =
         Polynomial.monomial j.val (v j i).val := by
   …

   Mentions: OAI.Nagata.Workers.W10.polynomialSectionBasisFromCoefficients

5. def OAI.Nagata.Workers.W10.centeredThetaSectionBasis line 81

   Source documentation

   The genuine centered source theta family is a basis for every real parameter 0 < tau < 1, with the literal nonintegral residue interval.

   def centeredThetaSectionBasis :
       Basis (thetaIndices (σ - x₀ * (n : ℝ)) n) ℂ
         (automorphicSections (τ : ℂ) n (ε * ((τ ^ σ : ℝ) : ℂ))) := by
   …

6. theorem OAI.Nagata.Workers.W10.centeredThetaSectionBasis_apply line 99
7. theorem OAI.Nagata.Workers.W10.centeredThetaSectionBasis_local line 107

   Source documentation

   Exact source series expression of the actual constructed basis vector.

   theorem centeredThetaSectionBasis_local
       (K : thetaIndices (σ - x₀ * (n : ℝ)) n) (x : ℂ) :
       (centeredThetaSectionBasis n hn σ x₀ hε hunit hτ hτone hC hU K).val
         (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
       ∑' p : ℤ, normalizedThetaTerm (n : ℝ) ((K.val : ℝ) - σ + x₀ * (n : ℝ))
         (K.val : ℝ) ε τ p x := by
   …

   Mentions: OAI.Nagata.Workers.W10.centeredThetaSectionBasis