Automorphic.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Automorphic section spaces, Laurent recurrences, and period freeness

def OAI.Nagata.W08.automorphicSections line 28
Source documentation
Holomorphic functions on ℂ* with the multiplier of D(n,γ). The zero extension at the omitted point is part of the representation.
```
noncomputable def automorphicSections (τ : ℂ) (n : ℤ) (γ : ℂ) :
    Submodule ℂ (ℂ → ℂ) where
…
```
theorem OAI.Nagata.W08.mem_automorphicSections_iff line 60
theorem OAI.Nagata.W08.automorphicSections_ext line 66
Source documentation
Agreement on the genuine domain ℂ* determines the represented section.
```
theorem automorphicSections_ext {τ γ : ℂ} {n : ℤ}
    (f g : automorphicSections τ n γ)
    (h : ∀ z, z ≠ 0 → f.val z = g.val z) : f = g := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections
def OAI.Nagata.W08.sectionRestriction line 77
Source documentation
Forget the forced zero value and restrict to the actual punctured-plane domain.
```
def sectionRestriction (τ : ℂ) (n : ℤ) (γ : ℂ) :
    automorphicSections τ n γ →ₗ[ℂ] ({z : ℂ // z ≠ 0} → ℂ) where
…
```
Mentions: OAI.Nagata.W08.automorphicSections
theorem OAI.Nagata.W08.sectionRestriction_injective line 84
Source documentation
The zero-extension representation adds no sections invisible on ℂ*.
```
theorem sectionRestriction_injective (τ : ℂ) (n : ℤ) (γ : ℂ) :
    Function.Injective (sectionRestriction τ n γ) := by
…
```
Mentions: OAI.Nagata.W08.sectionRestriction
def OAI.Nagata.W08.normalizeAtZero line 92
Source documentation
Extend the values on ℂ* by zero at the omitted point.
```
noncomputable def normalizeAtZero (f : ℂ → ℂ) (z : ℂ) : ℂ :=
…
```
theorem OAI.Nagata.W08.normalizeAtZero_zero line 95
theorem OAI.Nagata.W08.normalizeAtZero_of_ne line 98
theorem OAI.Nagata.W08.normalizeAtZero_eventuallyEq line 103
Source documentation
Changing the value at zero changes no germ on the punctured plane.
```
theorem normalizeAtZero_eventuallyEq (f : ℂ → ℂ) {z : ℂ} (hz : z ≠ 0) :
    normalizeAtZero f =ᶠ[𝓝 z] f :=
…
```
Mentions: OAI.Nagata.W08.normalizeAtZero
theorem OAI.Nagata.W08.normalizeAtZero_differentiableAt_iff line 108
Source documentation
The zero-extension representation preserves holomorphy at every genuine point.
```
theorem normalizeAtZero_differentiableAt_iff (f : ℂ → ℂ) {z : ℂ} (hz : z ≠ 0) :
    DifferentiableAt ℂ (normalizeAtZero f) z ↔ DifferentiableAt ℂ f z :=
…
```
Mentions: OAI.Nagata.W08.normalizeAtZero
theorem OAI.Nagata.W08.normalizeAtZero_mem_automorphicSections line 114
Source documentation
Construct a concrete section from an actual holomorphic automorphic function. The assumptions state only holomorphy and the defining multiplier equation.
```
theorem normalizeAtZero_mem_automorphicSections {τ γ : ℂ} {n : ℤ}
    (hτ : τ ≠ 0) (f : ℂ → ℂ)
    (hf : ∀ z, z ≠ 0 → DifferentiableAt ℂ f z)
    (he : ∀ z, z ≠ 0 → f (τ * z) = γ * z ^ (-n) * f z) :
    normalizeAtZero f ∈ automorphicSections τ n γ := by
…
```
Mentions: OAI.Nagata.W08.normalizeAtZero, OAI.Nagata.W08.automorphicSections

def OAI.Nagata.W08.sectionOfFunction line 127

Source documentation

The resulting element of the genuine section space.

noncomputable def sectionOfFunction {τ γ : ℂ} {n : ℤ}
    (hτ : τ ≠ 0) (f : ℂ → ℂ)
    (hf : ∀ z, z ≠ 0 → DifferentiableAt ℂ f z)
    (he : ∀ z, z ≠ 0 → f (τ * z) = γ * z ^ (-n) * f z) :
    automorphicSections τ n γ :=
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.W08.sectionOfFunction_apply line 134
def OAI.Nagata.W08.triangular line 153
Source documentation
The integer-valued quadratic appearing in a bi-infinite Laurent orbit.
```
def triangular (p : Int) : Int := p * (p - 1) / 2
```
theorem OAI.Nagata.W08.triangular_zero line 155
theorem OAI.Nagata.W08.triangular_add_one line 158
Source documentation
This identity is valid also for negative p.
```
theorem triangular_add_one (p : Int) : triangular (p + 1) = triangular p + p := by
…
```
Mentions: OAI.Nagata.W08.triangular
theorem OAI.Nagata.W08.triangular_sub_one line 166
def OAI.Nagata.W08.laurentExponent line 173
Source documentation
The exact exponent, before distributing the factor n inside the quotient.
```
def laurentExponent (n K p : Int) : Int := p * K + n * triangular p
```
Mentions: OAI.Nagata.W08.triangular
theorem OAI.Nagata.W08.laurentExponent_zero line 175
theorem OAI.Nagata.W08.laurentExponent_add_one line 178
theorem OAI.Nagata.W08.laurentExponent_sub_one line 183

theorem OAI.Nagata.W08.biInfinite_unique line 191

Source documentation

A recurrence with reversible transitions is determined at every integer by its value at zero.

theorem biInfinite_unique {α : Type u} (step : Int → α → α)
    (injective_step : ∀ p x y, step p x = step p y → x = y)
    (a b : Int → α) (ha : ∀ p, a (p + 1) = step p (a p))
    (hb : ∀ p, b (p + 1) = step p (b p)) (hzero : a 0 = b 0) : a = b := by
…

theorem OAI.Nagata.W08.two_mul_triangular line 221
Source documentation
The division in the triangular exponent is exact, for every integer.
```
theorem two_mul_triangular (p : Int) : 2 * triangular p = p * (p - 1) := by
…
```
Mentions: OAI.Nagata.W08.triangular
theorem OAI.Nagata.W08.two_dvd_mul_pred line 234
theorem OAI.Nagata.W08.laurentExponent_eq_source line 238
Source documentation
Moves n through the exact integer quotient in the manuscript exponent.
```
theorem laurentExponent_eq_source (n K p : Int) :
    laurentExponent n K p = p * K + n * p * (p - 1) / 2 := by
…
```
Mentions: OAI.Nagata.W08.laurentExponent
theorem OAI.Nagata.W08.period_zpow_eq_one line 253
Source documentation
A complex period strictly inside the unit circle has no nontrivial integral period.
```
theorem period_zpow_eq_one {τ : ℂ} (hτ : ‖τ‖ < 1) {k : ℤ}
    (hk : τ ^ k = 1) : k = 0 := by
…
```

theorem OAI.Nagata.W08.period_zpow_mul_eq_self line 260

Source documentation

The period acts freely on every nonzero point.

theorem period_zpow_mul_eq_self {τ z : ℂ} (hτ : ‖τ‖ < 1) (hz : z ≠ 0)
    {k : ℤ} (hk : τ ^ k * z = z) : k = 0 := by
…

theorem OAI.Nagata.W08.unitPeriod_free line 266
Source documentation
The unit-valued form used by the genuine torus and multiplier quotients.
```
theorem unitPeriod_free (τ : ℂˣ) (hτ : ‖(τ : ℂ)‖ < 1) (k : ℤ)
    (hk : τ ^ k = 1) : k = 0 := by
…
```

theorem OAI.Nagata.W08.periodic_eq_of_exp_eq line 289

Source documentation

Equality of exponential images identifies values of a deck-invariant function.

theorem periodic_eq_of_exp_eq (F : ℂ → ℂ)
    (hperiod : ∀ x (k : ℤ), F (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) = F x)
    {x y : ℂ} (hxy : Complex.exp x = Complex.exp y) : F x = F y := by
…

theorem OAI.Nagata.W08.periodic_log_eq_localLog line 296

Source documentation

Use any local logarithm about z₀; the value agrees with the principal-log formula.

theorem periodic_log_eq_localLog (F : ℂ → ℂ)
    (hperiod : ∀ x (k : ℤ), F (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) = F x)
    {z z₀ : ℂ} (hz : z ≠ 0) (hz₀ : z₀ ≠ 0) :
    F (Complex.log z) = F (Complex.log (z / z₀) + Complex.log z₀) := by
…

theorem OAI.Nagata.W08.periodic_log_differentiableAt line 306

Source documentation

The expression using principal log is holomorphic even at its branch cut, because locally it agrees with a holomorphic choice centered at the point.

theorem periodic_log_differentiableAt (F : ℂ → ℂ) (hF : Differentiable ℂ F)
    (hperiod : ∀ x (k : ℤ), F (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) = F x)
    {z₀ : ℂ} (hz₀ : z₀ ≠ 0) :
    DifferentiableAt ℂ (fun z ↦ F (Complex.log z)) z₀ := by
…

theorem OAI.Nagata.W08.periodic_log_automorphy line 325

Source documentation

A shift law on the exponential cover gives the actual multiplicative law on ℂ*.

theorem periodic_log_automorphy (F : ℂ → ℂ)
    (hperiod : ∀ x (k : ℤ), F (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) = F x)
    {τ γ : ℂ} {n : ℤ} (hτ : τ ≠ 0)
    (hshift : ∀ x, F (x + Complex.log τ) =
      γ * Complex.exp (((-n : ℤ) : ℂ) * x) * F x)
    {z : ℂ} (hz : z ≠ 0) :
    F (Complex.log (τ * z)) = γ * z ^ (-n) * F (Complex.log z) := by
…

def OAI.Nagata.W08.automorphicSectionOfPeriodicFunction line 340

Source documentation

Package the descended actual function as a genuine holomorphic multiplier section. Entire holomorphy, deck invariance and the scalar shift law remain explicit inputs.

def automorphicSectionOfPeriodicFunction (F : ℂ → ℂ) (hF : Differentiable ℂ F)
    (hperiod : ∀ x (k : ℤ), F (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) = F x)
    {τ γ : ℂ} {n : ℤ} (hτ : τ ≠ 0)
    (hshift : ∀ x, F (x + Complex.log τ) =
      γ * Complex.exp (((-n : ℤ) : ℂ) * x) * F x) :
    automorphicSections τ n γ :=
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.W08.automorphicSectionOfPeriodicFunction_exp line 351

Source documentation

Every exponential-cover value is recovered exactly, independently of branch choices.

theorem automorphicSectionOfPeriodicFunction_exp (F : ℂ → ℂ) (hF : Differentiable ℂ F)
    (hperiod : ∀ x (k : ℤ), F (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) = F x)
    {τ γ : ℂ} {n : ℤ} (hτ : τ ≠ 0)
    (hshift : ∀ x, F (x + Complex.log τ) =
      γ * Complex.exp (((-n : ℤ) : ℂ) * x) * F x) (x : ℂ) :
    (automorphicSectionOfPeriodicFunction F hF hperiod hτ hshift).val (Complex.exp x) = F x := by
…

Mentions: OAI.Nagata.W08.automorphicSectionOfPeriodicFunction

def OAI.Nagata.W08.orbitValue line 379
Source documentation
Candidate values along one residue class. The starting coefficient can be zero.
```
def orbitValue (τ γ : F) (n K : ℤ) (c₀ : F) (p : ℤ) : F :=
…
```
theorem OAI.Nagata.W08.orbitValue_zero line 382
theorem OAI.Nagata.W08.orbitValue_add_one line 386

theorem OAI.Nagata.W08.laurent_recurrence_all_int line 396

Source documentation

The Laurent recurrence iterated through all integers, including negative ones.

theorem laurent_recurrence_all_int (τ γ : F) (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (n : ℤ) (c : ℤ → F)
    (hc : ∀ K, c (K + n) = γ⁻¹ * τ ^ K * c K) (K p : ℤ) :
    c (K + n * p) = c K * γ ^ (-p) * τ ^ (p * K + n * (p * (p - 1) / 2)) := by
…

theorem OAI.Nagata.W08.laurent_recurrence_source_formula line 417

Source documentation

The formula exactly as printed in eq:laurent-recurrence.

theorem laurent_recurrence_source_formula (τ γ : F) (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (n : ℤ) (c : ℤ → F)
    (hc : ∀ K, c (K + n) = γ⁻¹ * τ ^ K * c K) (K p : ℤ) :
    c (K + n * p) = c K * γ ^ (-p) * τ ^ (p * K + n * p * (p - 1) / 2) := by
…

theorem OAI.Nagata.W08.recurrence_of_coefficient_balance line 427

Source documentation

Rearrangement of the coefficient equality obtained from the functional equation.

theorem recurrence_of_coefficient_balance (τ γ : F) (hγ : γ ≠ 0)
    (n : ℤ) (c : ℤ → F)
    (hbalance : ∀ K, τ ^ K * c K = γ * c (K + n)) :
    ∀ K, c (K + n) = γ⁻¹ * τ ^ K * c K := by
…

theorem OAI.Nagata.W08.laurent_formula_of_coefficient_balance line 438

Source documentation

The entire bi-infinite formula follows from the coefficient balance equation.

theorem laurent_formula_of_coefficient_balance (τ γ : F) (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (n : ℤ) (c : ℤ → F)
    (hbalance : ∀ K, τ ^ K * c K = γ * c (K + n)) (K p : ℤ) :
    c (K + n * p) = c K * γ ^ (-p) * τ ^ (p * K + n * p * (p - 1) / 2) :=
…