SectionBases.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Coefficient, residue-class, and degree-zero bases of section spaces

theorem OAI.Nagata.Workers.W10.coefficientMap_surjective line 25

Source documentation

Delta-valued coefficient vectors give every finite coefficient array.

theorem coefficientMap_surjective (c : V →ₗ[R] (I → R)) (v : I → V)
    (hv : ∀ i, c (v i) = Pi.single i 1) : Function.Surjective c := by
…

def OAI.Nagata.Workers.W10.coefficientEquiv line 33

Source documentation

Injectivity and checked delta coefficient values produce a linear equivalence.

def coefficientEquiv (c : V →ₗ[R] (I → R)) (hc : Function.Injective c)
    (v : I → V) (hv : ∀ i, c (v i) = Pi.single i 1) : V ≃ₗ[R] (I → R) :=
…

def OAI.Nagata.Workers.W10.basisFromCoefficients line 38

Source documentation

The basis is constructed from the proved equivalence, not supplied as data.

def basisFromCoefficients (c : V →ₗ[R] (I → R)) (hc : Function.Injective c)
    (v : I → V) (hv : ∀ i, c (v i) = Pi.single i 1) : Basis I R V :=
…

theorem OAI.Nagata.Workers.W10.basisFromCoefficients_apply line 43

Source documentation

Its actual vectors are exactly the specified coefficient-delta vectors.

@[simp] theorem basisFromCoefficients_apply
    (c : V →ₗ[R] (I → R)) (hc : Function.Injective c)
    (v : I → V) (hv : ∀ i, c (v i) = Pi.single i 1) (i : I) :
    basisFromCoefficients c hc v hv i = v i := by
…

Mentions: OAI.Nagata.Workers.W10.basisFromCoefficients

theorem OAI.Nagata.Workers.W10.basisFromCoefficients_repr line 53

Source documentation

Coordinate extraction computes the basis representation exactly.

theorem basisFromCoefficients_repr
    (c : V →ₗ[R] (I → R)) (hc : Function.Injective c)
    (v : I → V) (hv : ∀ i, c (v i) = Pi.single i 1) (x : V) (i : I) :
    (basisFromCoefficients c hc v hv).repr x i = c x i := by
…

Mentions: OAI.Nagata.Workers.W10.basisFromCoefficients

theorem OAI.Nagata.Workers.W10.coefficient_reconstruction line 61

Source documentation

Every vector is the finite sum of its actual extracted coefficients.

theorem coefficient_reconstruction
    (c : V →ₗ[R] (I → R)) (hc : Function.Injective c)
    (v : I → V) (hv : ∀ i, c (v i) = Pi.single i 1) (x : V) :
    ∑ i, c x i • v i = x := by
…

def OAI.Nagata.Workers.W10.normalizedConstantSection line 85
Source documentation
A genuine constant section on C*, represented by zero extension at zero.
```
def normalizedConstantSection (τ : ℂ) (hτ : τ ≠ 0) (a : ℂ) :
    automorphicSections τ 0 1 :=
…
```
theorem OAI.Nagata.Workers.W10.normalizedConstantSection_apply line 90

def OAI.Nagata.Workers.W10.zeroCoefficientMap line 95

Source documentation

The coefficient at zero is the unique finite coordinate of the constant tip.

def zeroCoefficientMap {V : Type*} [AddCommMonoid V] [Module ℂ V]
    (C : V →ₗ[ℂ] (ℤ → ℂ)) : V →ₗ[ℂ] (PUnit → ℂ) where
…

theorem OAI.Nagata.Workers.W10.zeroDegree_coeff_eq_zero line 102

Source documentation

Degree-zero automorphy forces every nonzero-index coefficient to vanish.

theorem zeroDegree_coeff_eq_zero {V : Type*} [AddCommMonoid V] [Module ℂ V]
    (C : V →ₗ[ℂ] (ℤ → ℂ)) {τ : ℂ} (hτnorm : ‖τ‖ < 1)
    (hrec : ∀ f k, C f k = τ ^ k * C f k) (f : V) {k : ℤ} (hk : k ≠ 0) :
    C f k = 0 := by
…

theorem OAI.Nagata.Workers.W10.zeroCoefficientMap_injective line 115

Source documentation

All Laurent coefficients reduce to the one zero-index coordinate.

theorem zeroCoefficientMap_injective {V : Type*} [AddCommMonoid V] [Module ℂ V]
    (C : V →ₗ[ℂ] (ℤ → ℂ)) (hC : Function.Injective C)
    {τ : ℂ} (hτnorm : ‖τ‖ < 1)
    (hrec : ∀ f k, C f k = τ ^ k * C f k) :
    Function.Injective (zeroCoefficientMap C) := by
…

Mentions: OAI.Nagata.Workers.W10.zeroCoefficientMap

def OAI.Nagata.Workers.W10.zeroDegreeBasisOfLaurentData line 131

Source documentation

The actual normalized constant section is the degree-zero basis vector, once its actual coefficient and analytic Laurent uniqueness are established.

def zeroDegreeBasisOfLaurentData (τ : ℂ) (hτ : τ ≠ 0) (hτnorm : ‖τ‖ < 1)
    (C : automorphicSections τ 0 1 →ₗ[ℂ] (ℤ → ℂ)) (hC : Function.Injective C)
    (hrec : ∀ f k, C f k = τ ^ k * C f k)
    (hconstant : C (normalizedConstantSection τ hτ 1) 0 = 1) :
    Basis PUnit ℂ (automorphicSections τ 0 1) := by
…

Mentions: OAI.Nagata.Workers.W10.normalizedConstantSection

theorem OAI.Nagata.Workers.W10.zeroDegreeBasisOfLaurentData_apply line 143

def OAI.Nagata.Workers.W10.residueCoefficientMap line 165

Source documentation

Restrict an actual coefficient map to the manuscript's finite residue interval.

def residueCoefficientMap {V : Type*} [AddCommMonoid V] [Module ℂ V]
    (C : V →ₗ[ℂ] (ℤ → ℂ)) (U : ℝ) (n : ℤ) :
    V →ₗ[ℂ] (thetaIndices U n → ℂ) where
…

theorem OAI.Nagata.Workers.W10.residueCoefficientMap_injective line 174

Source documentation

Recurrence determination turns analytic uniqueness of all Laurent coefficients into injectivity of the finitely many residue coefficients.

theorem residueCoefficientMap_injective {V : Type*} [AddCommMonoid V] [Module ℂ V]
    (C : V →ₗ[ℂ] (ℤ → ℂ)) (hC : Function.Injective C)
    (τ γ : ℂ) (hτ : τ ≠ 0) (hγ : γ ≠ 0) (U : ℝ) {n : ℤ} (hn : 0 < n)
    (hrec : ∀ f k, C f (k + n) = γ⁻¹ * τ ^ k * C f k) :
    Function.Injective (residueCoefficientMap C U n) := by
…

Mentions: OAI.Nagata.Workers.W10.residueCoefficientMap

def OAI.Nagata.Workers.W10.sectionBasisOfLaurentData line 188

Source documentation

A basis of the actual section space follows once actual Laurent uniqueness, recurrence, and the theta coefficient identities have been proved.

def sectionBasisOfLaurentData (τ γ : ℂ) (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (U : ℝ) (n : ℤ) (hn : 0 < n)
    (C : automorphicSections τ n γ →ₗ[ℂ] (ℤ → ℂ))
    (hC : Function.Injective C)
    (hrec : ∀ f k, C f (k + n) = γ⁻¹ * τ ^ k * C f k)
    (theta : thetaIndices U n → automorphicSections τ n γ)
    (htheta : ∀ K, residueCoefficientMap C U n (theta K) = Pi.single K 1) :
    Basis (thetaIndices U n) ℂ (automorphicSections τ n γ) := by
…

Mentions: OAI.Nagata.Workers.W10.residueCoefficientMap

theorem OAI.Nagata.Workers.W10.sectionBasisOfLaurentData_apply line 200

def OAI.Nagata.Workers.W10.normalizedResidueMap line 227

Source documentation

Divide each actual residue coefficient by its nonzero normalization scalar.

def normalizedResidueMap (C : V →ₗ[ℂ] (ℤ → ℂ)) (U : ℝ) (n : ℤ)
    (a : thetaIndices U n → ℂ) : V →ₗ[ℂ] (thetaIndices U n → ℂ) where
…

theorem OAI.Nagata.Workers.W10.normalizedResidueMap_injective line 233

theorem OAI.Nagata.Workers.W10.normalizedResidueMap_delta line 247

Source documentation

Orbit support and the diagonal coefficient imply the full finite delta identity, since the chosen indices have distinct residues.

theorem normalizedResidueMap_delta (C : V →ₗ[ℂ] (ℤ → ℂ))
    (τ γ : ℂ) (U : ℝ) (n : ℤ) (a : thetaIndices U n → ℂ)
    (ha : ∀ K, a K ≠ 0) (theta : thetaIndices U n → V)
    (hcoeff : ∀ K k, C (theta K) k = supportedOrbitCoefficient τ γ n K.val (a K) k)
    (K : thetaIndices U n) :
    normalizedResidueMap C U n a (theta K) = Pi.single K 1 := by
…

Mentions: OAI.Nagata.Workers.W10.normalizedResidueMap

def OAI.Nagata.Workers.W10.basisFromSupportedOrbits line 269

Source documentation

The actual centered vectors themselves form a basis. No rescaling of the vectors is needed; normalization occurs only in coefficient extraction.

def basisFromSupportedOrbits (C : V →ₗ[ℂ] (ℤ → ℂ))
    (τ γ : ℂ) (U : ℝ) (n : ℤ) (a : thetaIndices U n → ℂ)
    (ha : ∀ K, a K ≠ 0)
    (hc : Function.Injective (residueCoefficientMap C U n))
    (theta : thetaIndices U n → V)
    (hcoeff : ∀ K k, C (theta K) k = supportedOrbitCoefficient τ γ n K.val (a K) k) :
    Basis (thetaIndices U n) ℂ V :=
…

Mentions: OAI.Nagata.Workers.W10.residueCoefficientMap

theorem OAI.Nagata.Workers.W10.basisFromSupportedOrbits_apply line 280