NormalizedExponents.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Normalized exponent intervals for automorphic sections

def OAI.Nagata.W08.thetaJacobiParameter line 19
Source documentation
The upper-half-plane period parameter corresponding to the real nome τ.
```
def thetaJacobiParameter (n τ : ℝ) : ℂ :=
…
```
def OAI.Nagata.W08.thetaJacobiArgument line 23
Source documentation
The affine first argument of Jacobi theta for the source normalized series.
```
def thetaJacobiArgument (n a : ℝ) (ε : ℂ) (τ : ℝ) (x : ℂ) : ℂ :=
…
```

theorem OAI.Nagata.W08.normalizedThetaTerm_eq_exponential line 28

Source documentation

Exact equality of actual summands, retaining every scalar normalization.

theorem normalizedThetaTerm_eq_exponential (n a K : ℝ) {ε : ℂ} (hε : ε ≠ 0)
    {τ : ℝ} (hτ : 0 < τ) (p : ℤ) (x : ℂ) :
    normalizedThetaTerm n a K ε τ p x =
      Complex.exp ((K : ℂ) * x) *
        Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (p : ℂ) * thetaJacobiArgument n a ε τ x +
          (Real.pi : ℂ) * Complex.I * (p : ℂ) ^ 2 * thetaJacobiParameter n τ) := by
…

Mentions: OAI.Nagata.W08.thetaJacobiArgument, OAI.Nagata.W08.thetaJacobiParameter

theorem OAI.Nagata.W08.thetaJacobiParameter_im_pos line 49
Source documentation
The Jacobi parameter lies in the genuine convergence domain.
```
theorem thetaJacobiParameter_im_pos {n τ : ℝ}
    (hn : 0 < n) (hτ : 0 < τ) (hτone : τ < 1) :
    0 < (thetaJacobiParameter n τ).im := by
…
```
Mentions: OAI.Nagata.W08.thetaJacobiParameter

theorem OAI.Nagata.W08.normalizedThetaTerm_integerPeriod line 65

Source documentation

Integer-frequency summands are independent of the logarithm branch.

theorem normalizedThetaTerm_integerPeriod (n K k : ℤ) (a : ℝ) (ε : ℂ) (τ : ℝ)
    (p : ℤ) (x : ℂ) :
    normalizedThetaTerm (n : ℝ) a (K : ℝ) ε τ p
        (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) =
      normalizedThetaTerm (n : ℝ) a (K : ℝ) ε τ p x := by
…

theorem OAI.Nagata.W08.normalizedThetaSeries_integerPeriod line 81

Source documentation

Branch independence of the actual tsum, without any hidden convergence hypothesis.

theorem normalizedThetaSeries_integerPeriod (n K k : ℤ) (a : ℝ) (ε : ℂ) (τ : ℝ)
    (x : ℂ) :
    (∑' p : ℤ, normalizedThetaTerm (n : ℝ) a (K : ℝ) ε τ p
      (x + (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I))) =
    (∑' p : ℤ, normalizedThetaTerm (n : ℝ) a (K : ℝ) ε τ p x) :=
…

theorem OAI.Nagata.W08.normalizedThetaTerm_eq_singleExp line 89

Source documentation

The literal normalized summand as one complex exponential.

theorem normalizedThetaTerm_eq_singleExp (n a K : ℝ) {ε : ℂ} (hε : ε ≠ 0)
    {τ : ℝ} (hτ : 0 < τ) (p : ℤ) (x : ℂ) :
    normalizedThetaTerm n a K ε τ p x =
      Complex.exp (((-p : ℤ) : ℂ) * Complex.log ε +
        ((Real.log τ * thetaExponent n a (p : ℝ) : ℝ) : ℂ) +
        (((K + n * (p : ℝ) : ℝ) : ℂ) * x)) := by
…

theorem OAI.Nagata.W08.normalizedThetaTerm_realShift_index line 102

Source documentation

One scalar shift agrees exactly with one integer reindexing of actual summands.

theorem normalizedThetaTerm_realShift_index (n a K : ℝ) {ε : ℂ} (hε : ε ≠ 0)
    {τ : ℝ} (hτ : 0 < τ) (p : ℤ) (x : ℂ) :
    normalizedThetaTerm n a K ε τ p (x + (Real.log τ : ℂ)) =
      ((ε * ((τ ^ (K - a) : ℝ) : ℂ)) * Complex.exp (-(n : ℂ) * x)) *
        normalizedThetaTerm n a K ε τ (p + 1) x := by
…

theorem OAI.Nagata.W08.normalizedThetaSeries_realShift line 119

Source documentation

The exact additive multiplier law, proved by integer reindexing without Jacobi theta.

theorem normalizedThetaSeries_realShift (n a K : ℝ) {ε : ℂ} (hε : ε ≠ 0)
    {τ : ℝ} (hτ : 0 < τ) (x : ℂ) :
    (∑' p : ℤ, normalizedThetaTerm n a K ε τ p (x + (Real.log τ : ℂ))) =
      (ε * ((τ ^ (K - a) : ℝ) : ℂ)) * Complex.exp (-(n : ℂ) * x) *
        (∑' p : ℤ, normalizedThetaTerm n a K ε τ p x) := by
…