ConstantSections.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Nagata.W19.contraction_invariant_nat_pow line 23
theorem OAI.Nagata.W19.contraction_invariant_zpow line 31
theorem OAI.Nagata.W19.bounded_holomorphic_contraction_constant line 45
theorem OAI.Nagata.W19.periodic_holomorphic_bounded line 89
theorem OAI.Nagata.W19.degree_zero_section_constant line 105
def OAI.Nagata.W19.degreeZeroSectionEquiv line 117
Source documentation
Evaluation at one is a genuine linear equivalence for actual sections.
```
def degreeZeroSectionEquiv {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) :
    automorphicSections (τ : ℂ) 0 1 ≃ₗ[ℂ] ℂ where
…
```

def OAI.Nagata.W19.degreeZeroConstantBasis line 132

Source documentation

A basis of the actual section space with its single constant-one vector.

def degreeZeroConstantBasis {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) :
    Module.Basis PUnit ℂ (automorphicSections (τ : ℂ) 0 1) :=
…