ThetaProducts.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

Analytic theta products, zeros, and marked products

def OAI.Nagata.W21.thetaPositive line 24
def OAI.Nagata.W21.thetaProduct line 28
Source documentation
The negative-index product is written with index n+1, starting at zero.
```
noncomputable def thetaProduct (τ z : ℂ) : ℂ :=
…
```

theorem OAI.Nagata.W21.thetaPositive_multipliable line 32

Source documentation

Convergence of the positive half, valid at its zeros as well.

theorem thetaPositive_multipliable {τ : ℂ} (hτ : ‖τ‖ < 1) (z : ℂ) :
    Multipliable (fun n : ℕ ↦ 1 - τ ^ n * z) := by
…

theorem OAI.Nagata.W21.thetaNegative_multipliable line 39

Source documentation

Convergence of the second product as indexed in the manuscript.

theorem thetaNegative_multipliable {τ : ℂ} (hτ : ‖τ‖ < 1) (z : ℂ) :
    Multipliable (fun n : ℕ ↦ 1 - τ ^ (n + 1) / z) := by
…

theorem OAI.Nagata.W21.thetaProduct_eq_source line 45
Source documentation
The genuine product definition agrees with the two products in the source.
```
theorem thetaProduct_eq_source (τ z : ℂ) :
    thetaProduct τ z = (∏' n : ℕ, (1 - τ ^ n * z)) *
      ∏' n : ℕ, (1 - τ ^ (n + 1) / z) := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaPositive_shift line 51
Source documentation
Removing the first factor from a convergent product, without dividing by it.
```
theorem thetaPositive_shift {τ : ℂ} (hτ : ‖τ‖ < 1) (z : ℂ) :
    thetaPositive τ z = (1 - z) * thetaPositive τ (τ * z) := by
…
```
Mentions: OAI.Nagata.W21.thetaPositive

theorem OAI.Nagata.W21.thetaProduct_automorphy line 59

Source documentation

Theta automorphy on ℂ*, proved from convergent products.

theorem thetaProduct_automorphy {τ z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (hz : z ≠ 0) :
    thetaProduct τ (τ * z) = -z⁻¹ * thetaProduct τ z := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_automorphy_real line 81

Source documentation

The automorphy equation with the manuscript's real parameter hypotheses.

theorem thetaProduct_automorphy_real {τ : ℝ} (hτ0 : 0 < τ) (hτ1 : τ < 1)
    {z : ℂ} (hz : z ≠ 0) :
    thetaProduct (τ : ℂ) ((τ : ℂ) * z) = -z⁻¹ * thetaProduct (τ : ℂ) z := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_scaled_automorphy line 91
Source documentation
A theta factor with zero represented by a has multiplier -a. This is the covering-space equation used for D(1,-a) in the manuscript.
```
theorem thetaProduct_scaled_automorphy {τ a z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0) :
    thetaProduct τ ((τ * z) / a) = (-a) * z⁻¹ * thetaProduct τ (z / a) := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaPositive_ne_zero line 98
Source documentation
Away from zeros of its factors the positive product is nonzero.
```
theorem thetaPositive_ne_zero {τ : ℂ} (hτ : ‖τ‖ < 1) (z : ℂ)
    (hz : ∀ n : ℕ, 1 - τ ^ n * z ≠ 0) : thetaPositive τ z ≠ 0 := by
…
```
Mentions: OAI.Nagata.W21.thetaPositive
theorem OAI.Nagata.W21.thetaPositive_eq_zero_iff line 109
Source documentation
No extra zeros are introduced by passage to the infinite positive product.
```
theorem thetaPositive_eq_zero_iff {τ : ℂ} (hτ : ‖τ‖ < 1) (z : ℂ) :
    thetaPositive τ z = 0 ↔ ∃ n : ℕ, τ ^ n * z = 1 := by
…
```
Mentions: OAI.Nagata.W21.thetaPositive
theorem OAI.Nagata.W21.thetaProduct_eq_zero_iff_factors line 126
Source documentation
Exact factor-zero description of the full product, before identifying the index set with the integer powers of a nonzero parameter.
```
theorem thetaProduct_eq_zero_iff_factors {τ : ℂ} (hτ : ‖τ‖ < 1) (z : ℂ) :
    thetaProduct τ z = 0 ↔
      (∃ n : ℕ, τ ^ n * z = 1) ∨ (∃ n : ℕ, τ ^ n * (τ * z⁻¹) = 1) := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaPositive_hasProdUniformlyOn_comp line 145

Source documentation

Compact uniform convergence after any continuous bounded substitution.

theorem thetaPositive_hasProdUniformlyOn_comp {α : Type*} [TopologicalSpace α]
    {τ : ℂ} (hτ : ‖τ‖ < 1) {K : Set α} (hK : IsCompact K)
    (g : α → ℂ) (hg : ContinuousOn g K) (R : ℝ)
    (hR : ∀ x ∈ K, ‖g x‖ ≤ R) :
    HasProdUniformlyOn (fun (n : ℕ) x ↦ 1 - τ ^ n * g x)
      (fun x ↦ thetaPositive τ (g x)) K := by
…

Mentions: OAI.Nagata.W21.thetaPositive

theorem OAI.Nagata.W21.thetaNegative_hasProdUniformlyOn line 164

Source documentation

The second source product converges uniformly on every compact subset of ℂ*; compactness supplies a bound for inversion.

theorem thetaNegative_hasProdUniformlyOn {τ : ℂ} (hτ : ‖τ‖ < 1)
    {K : Set ℂ} (hK : IsCompact K) (hz : ∀ z ∈ K, z ≠ 0) :
    HasProdUniformlyOn (fun (n : ℕ) (z : ℂ) ↦ 1 - τ ^ (n + 1) / z)
      (fun z ↦ thetaPositive τ (τ * z⁻¹)) K := by
…

Mentions: OAI.Nagata.W21.thetaPositive

theorem OAI.Nagata.W21.thetaNegative_hasProdLocallyUniformlyOn line 176

Source documentation

The negative half converges locally uniformly on the punctured plane.

theorem thetaNegative_hasProdLocallyUniformlyOn {τ : ℂ} (hτ : ‖τ‖ < 1) :
    HasProdLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) ↦ 1 - τ ^ (n + 1) / z)
      (fun z ↦ thetaPositive τ (τ * z⁻¹)) {z : ℂ | z ≠ 0} := by
…

Mentions: OAI.Nagata.W21.thetaPositive

theorem OAI.Nagata.W21.thetaPositive_hasProdLocallyUniformlyOn line 184
Source documentation
The positive product converges locally uniformly on the whole complex plane.
```
theorem thetaPositive_hasProdLocallyUniformlyOn {τ : ℂ} (hτ : ‖τ‖ < 1) :
    HasProdLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) ↦ 1 - τ ^ n * z)
      (thetaPositive τ) Set.univ := by
…
```
Mentions: OAI.Nagata.W21.thetaPositive
theorem OAI.Nagata.W21.thetaPositive_differentiable line 194
Source documentation
The positive product is entire, by local uniform convergence of polynomials.
```
theorem thetaPositive_differentiable {τ : ℂ} (hτ : ‖τ‖ < 1) :
    Differentiable ℂ (thetaPositive τ) := by
…
```
Mentions: OAI.Nagata.W21.thetaPositive
theorem OAI.Nagata.W21.thetaProduct_differentiableAt line 206
Source documentation
The source theta product is holomorphic on the punctured complex plane.
```
theorem thetaProduct_differentiableAt {τ z : ℂ} (hτ : ‖τ‖ < 1) (hz : z ≠ 0) :
    DifferentiableAt ℂ (thetaProduct τ) z := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaPositive_parameter_ne_zero line 212
theorem OAI.Nagata.W21.thetaProduct_one line 225
Source documentation
The theta product vanishes at the representative 1.
```
theorem thetaProduct_one {τ : ℂ} (hτ : ‖τ‖ < 1) : thetaProduct τ 1 = 0 := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaProduct_hasDerivAt_one line 230
Source documentation
The derivative at 1 comes from its single zero factor.
```
theorem thetaProduct_hasDerivAt_one {τ : ℂ} (hτ : ‖τ‖ < 1) :
    HasDerivAt (thetaProduct τ) (-(thetaPositive τ τ) ^ 2) 1 := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct, OAI.Nagata.W21.thetaPositive
theorem OAI.Nagata.W21.thetaProduct_deriv_one_ne_zero line 248
Source documentation
Nonzero derivative certifies that the theta zero at 1 is simple.
```
theorem thetaProduct_deriv_one_ne_zero {τ : ℂ} (hτ : ‖τ‖ < 1) :
    deriv (thetaProduct τ) 1 ≠ 0 := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_eq_zero_iff_nat_powers line 262

Source documentation

Separate the inverse natural powers from the strictly positive powers.

theorem thetaProduct_eq_zero_iff_nat_powers {τ z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (hz : z ≠ 0) :
    thetaProduct τ z = 0 ↔
      (∃ n : ℕ, z = (τ ^ n)⁻¹) ∨ (∃ n : ℕ, z = τ ^ (n + 1)) := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_eq_zero_iff_zpow line 281
Source documentation
The source theta product has precisely the zeros τ^ℤ on ℂ*.
```
theorem thetaProduct_eq_zero_iff_zpow {τ z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (hz : z ≠ 0) :
    thetaProduct τ z = 0 ↔ ∃ k : ℤ, z = τ ^ k := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaProduct_scaled_eq_zero_iff line 299
Source documentation
The zeros of the theta factor Θ(z/a) are exactly the lifts of a in the multiplicative quotient. The quotient itself is not assumed here.
```
theorem thetaProduct_scaled_eq_zero_iff {τ a z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0) :
    thetaProduct τ (z / a) = 0 ↔ ∃ k : ℤ, z = a * τ ^ k := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaProduct_zpow_eq_zero line 320

theorem OAI.Nagata.W21.thetaProduct_deriv_mul_at_zero line 325

Source documentation

Differentiate the automorphy equation at a zero.

theorem thetaProduct_deriv_mul_at_zero {τ z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (hz : z ≠ 0) (hzero : thetaProduct τ z = 0) :
    deriv (thetaProduct τ) (τ * z) * τ = -z⁻¹ * deriv (thetaProduct τ) z := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_deriv_mul_ne_zero_iff line 341

Source documentation

At zeros, multiplying the argument by the nonzero period preserves a nonzero first derivative.

theorem thetaProduct_deriv_mul_ne_zero_iff {τ z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (hz : z ≠ 0) (hzero : thetaProduct τ z = 0) :
    deriv (thetaProduct τ) (τ * z) ≠ 0 ↔ deriv (thetaProduct τ) z ≠ 0 := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_deriv_pow_ne_zero line 356
Source documentation
The derivative is nonzero at every nonnegative power.
```
theorem thetaProduct_deriv_pow_ne_zero {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0)
    (n : ℕ) : deriv (thetaProduct τ) (τ ^ n) ≠ 0 := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct
theorem OAI.Nagata.W21.thetaProduct_deriv_inv_pow_ne_zero line 367
Source documentation
The derivative is nonzero at every inverse natural power.
```
theorem thetaProduct_deriv_inv_pow_ne_zero {τ : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0)
    (n : ℕ) : deriv (thetaProduct τ) ((τ ^ n)⁻¹) ≠ 0 := by
…
```
Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.thetaProduct_zero_has_nonzero_deriv line 383

Source documentation

Every theta zero on ℂ* has nonzero first derivative.

theorem thetaProduct_zero_has_nonzero_deriv {τ z : ℂ} (hτ : ‖τ‖ < 1)
    (hτ0 : τ ≠ 0) (hz : z ≠ 0) (hzero : thetaProduct τ z = 0) :
    deriv (thetaProduct τ) z ≠ 0 := by
…

Mentions: OAI.Nagata.W21.thetaProduct

def OAI.Nagata.W21.markedThetaProduct line 403
theorem OAI.Nagata.W21.thetaProduct_scaled_differentiableAt line 406
theorem OAI.Nagata.W21.markedThetaProduct_differentiableAt line 411
theorem OAI.Nagata.W21.markedThetaProduct_analyticOnNhd line 418
theorem OAI.Nagata.W21.markedThetaProduct_eq_zero_iff line 425

theorem OAI.Nagata.W21.thetaProduct_scaled_zero_has_nonzero_deriv line 434

Source documentation

The actual rescaling preserves simplicity of every theta zero.

theorem thetaProduct_scaled_zero_has_nonzero_deriv {τ a z : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0)
    (hf : thetaProduct τ (z / a) = 0) :
    deriv (fun w ↦ thetaProduct τ (w / a)) z ≠ 0 := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.finiteProduct_zero_has_nonzero_deriv line 447

Source documentation

An elementary finite-product simple-zero theorem used below.

theorem finiteProduct_zero_has_nonzero_deriv {ι : Type*} [Fintype ι]
    (f : ι → ℂ → ℂ) (z : ℂ) (hf : ∀ i, DifferentiableAt ℂ (f i) z)
    (i : ι) (hi : f i z = 0) (hdi : deriv (f i) z ≠ 0)
    (hother : ∀ j, j ≠ i → f j z ≠ 0) :
    deriv (fun w ↦ ∏ j, f j w) z ≠ 0 := by
…

theorem OAI.Nagata.W21.markedThetaFactors_unique_zero line 466

Source documentation

Distinct marked period orbits imply that no two shifted theta factors vanish at the same point.

theorem markedThetaFactors_unique_zero {ι : Type*} {τ : ℂ} {a : ι → ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j ↦ ∀ k : ℤ, a i ≠ a j * τ ^ k))
    {z : ℂ} (hz : z ≠ 0) {i j : ι} (hij : i ≠ j)
    (hi : thetaProduct τ (z / a i) = 0) : thetaProduct τ (z / a j) ≠ 0 := by
…

Mentions: OAI.Nagata.W21.thetaProduct

theorem OAI.Nagata.W21.markedThetaProduct_zero_has_nonzero_deriv line 480

Source documentation

The marked product has simple zeros when the marks represent distinct points in the period quotient.

theorem markedThetaProduct_zero_has_nonzero_deriv {ι : Type*} [Fintype ι]
    {τ : ℂ} {a : ι → ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0)
    (ha : ∀ i, a i ≠ 0)
    (hdisjoint : Pairwise (fun i j ↦ ∀ k : ℤ, a i ≠ a j * τ ^ k))
    {z : ℂ} (hz : z ≠ 0) (hzero : markedThetaProduct τ a z = 0) :
    deriv (markedThetaProduct τ a) z ≠ 0 := by
…

Mentions: OAI.Nagata.W21.markedThetaProduct