ThetaExponents.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Theta exponents, normalization, and individual terms

def OAI.Nagata.W07.thetaExponent line 25
Source documentation
Exponent of the theta parameter, with a = K - U.
```
def thetaExponent (n a p : ℝ) : ℝ := p * a + n * p * (p - 1) / 2
```
def OAI.Nagata.W07.thetaMargin line 28
Source documentation
Distance of the selected exponent from the two endpoints.
```
def thetaMargin (n a : ℝ) : ℝ := min a (n - a)
```
theorem OAI.Nagata.W07.thetaMargin_pos line 30
theorem OAI.Nagata.W07.thetaExponent_zero line 34
theorem OAI.Nagata.W07.thetaExponent_positive_index line 37
theorem OAI.Nagata.W07.thetaExponent_negative_index line 40
theorem OAI.Nagata.W07.thetaExponent_quadratic_lower line 46
Source documentation
The quadratic bound is valid for real indices, before using integrality.
```
theorem thetaExponent_quadratic_lower (n a p : ℝ) :
    thetaMargin n a * |p| + n * |p| * (|p| - 1) / 2 ≤
      thetaExponent n a p := by
…
```
Mentions: OAI.Nagata.W07.thetaMargin, OAI.Nagata.W07.thetaExponent
theorem OAI.Nagata.W07.thetaExponent_integer_lower line 62
Source documentation
Both positive and negative integer indices have the manuscript's linear bound.
```
theorem thetaExponent_integer_lower {n a : ℝ} (hn : 0 ≤ n) (p : ℤ) :
    thetaMargin n a * |(p : ℝ)| ≤ thetaExponent n a (p : ℝ) := by
…
```
Mentions: OAI.Nagata.W07.thetaMargin, OAI.Nagata.W07.thetaExponent
theorem OAI.Nagata.W07.thetaExponent_integer_pos line 79
Source documentation
The exponent is strictly positive away from the constant term.
```
theorem thetaExponent_integer_pos {n a : ℝ} (ha : 0 < a) (han : a < n)
    {p : ℤ} (hp : p ≠ 0) : 0 < thetaExponent n a (p : ℝ) := by
…
```
Mentions: OAI.Nagata.W07.thetaExponent
theorem OAI.Nagata.W07.thetaExponent_integer_eq_zero_iff line 87
Source documentation
The central coefficient is the unique term of exponent zero.
```
theorem thetaExponent_integer_eq_zero_iff {n a : ℝ} (ha : 0 < a)
    (han : a < n) (p : ℤ) : thetaExponent n a (p : ℝ) = 0 ↔ p = 0 := by
…
```
Mentions: OAI.Nagata.W07.thetaExponent
theorem OAI.Nagata.W07.thetaExponent_quarter_square_lower line 98
Source documentation
A uniform quadratic lower bound outside the two central indices.
```
theorem thetaExponent_quarter_square_lower {n a p : ℝ}
    (ha : 0 ≤ a) (han : a ≤ n) (hp : 2 ≤ |p|) :
    n / 4 * p ^ 2 ≤ thetaExponent n a p := by
…
```
Mentions: OAI.Nagata.W07.thetaExponent

theorem OAI.Nagata.W07.normalized_theta_exponent_lower line 112

Source documentation

Exact manuscript form, with an integer selected exponent K.

theorem normalized_theta_exponent_lower {n U : ℝ} {K p : ℤ}
    (hUK : U < (K : ℝ)) (hKU : (K : ℝ) < U + n) :
    min ((K : ℝ) - U) (n - ((K : ℝ) - U)) * |(p : ℝ)| ≤
      (p : ℝ) * ((K : ℝ) - U) + n * (p : ℝ) * ((p : ℝ) - 1) / 2 := by
…

theorem OAI.Nagata.W07.normalized_theta_exponent_pos line 118

theorem OAI.Nagata.W07.laurentExponent_cast_real line 136

Source documentation

Real cast of the exact integer-valued Laurent exponent.

theorem laurentExponent_cast_real (n K p : ℤ) :
    (Nagata.W08.laurentExponent n K p : ℝ) =
      (p : ℝ) * (K : ℝ) + (n : ℝ) * (p : ℝ) * ((p : ℝ) - 1) / 2 := by
…

Mentions: OAI.Nagata.W08.laurentExponent

theorem OAI.Nagata.W07.normalized_exponent_identity line 147

Source documentation

Cancellation of the normalization and moving-center exponents is exact.

theorem normalized_exponent_identity (n K p : ℤ) (σ x₀ : ℝ) :
    -x₀ * (K : ℝ) + (-σ * (p : ℝ) + (Nagata.W08.laurentExponent n K p : ℝ)) +
      x₀ * ((K + n * p : ℤ) : ℝ) =
      thetaExponent (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ)) (p : ℝ) := by
…

Mentions: OAI.Nagata.W08.laurentExponent, OAI.Nagata.W07.thetaExponent

def OAI.Nagata.W07.normalizedThetaTerm line 171
Source documentation
The actual normalized Laurent summand in logarithmic local coordinates.
```
def normalizedThetaTerm (n a K : ℝ) (ε : ℂ) (τ : ℝ) (p : ℤ) (x : ℂ) : ℂ :=
…
```
def OAI.Nagata.W07.normalizedThetaDerivativeTerm line 176
Source documentation
The candidate order-c derivative summand, with its explicit frequency factor.
```
def normalizedThetaDerivativeTerm (n a K : ℝ) (ε : ℂ) (τ : ℝ)
    (c : ℕ) (p : ℤ) (x : ℂ) : ℂ :=
…
```
theorem OAI.Nagata.W07.normalizedThetaTerm_zero line 180
theorem OAI.Nagata.W07.normalizedThetaDerivativeTerm_zero_order line 184
theorem OAI.Nagata.W07.normalizedThetaDerivativeTerm_zero_index line 190
theorem OAI.Nagata.W07.natAbs_real line 196
theorem OAI.Nagata.W07.theta_power_le_geometric line 200
Source documentation
The real power factor of a normalized summand is bounded by a geometric power.
```
theorem theta_power_le_geometric {n a τ : ℝ} (hn : 0 ≤ n)
    (hτ : 0 < τ) (hτone : τ ≤ 1) (p : ℤ) :
    τ ^ thetaExponent n a (p : ℝ) ≤ (τ ^ thetaMargin n a) ^ p.natAbs := by
…
```
Mentions: OAI.Nagata.W07.thetaExponent, OAI.Nagata.W07.thetaMargin
theorem OAI.Nagata.W07.theta_frequency_le line 211
Source documentation
The frequency of either the positive or negative index has the same bound.
```
theorem theta_frequency_le {n : ℝ} (hn : 0 ≤ n) (K : ℝ) (p : ℤ) :
    |K + n * (p : ℝ)| ≤ |K| + n * (p.natAbs : ℝ) := by
…
```
theorem OAI.Nagata.W07.norm_normalizedThetaDerivativeTerm_le line 223
Source documentation
Uniform majorant for every explicit derivative summand on the disk ‖x‖≤R.
This statement includes p=0; the series tail uses its restriction to nonzero indices. The hypotheses on a are needed to make thetaMargin positive when taking a parameter limit, but are not needed for this norm inequality itself.
```
theorem norm_normalizedThetaDerivativeTerm_le {n a K τ R : ℝ} {ε x : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hx : ‖x‖ ≤ R) (c : ℕ) (p : ℤ) :
    ‖normalizedThetaDerivativeTerm n a K ε τ c p x‖ ≤
      Real.exp (|K| * R) * (|K| + n * (p.natAbs : ℝ)) ^ c *
        (Real.exp (n * R) * τ ^ thetaMargin n a) ^ p.natAbs := by
…
```
Mentions: OAI.Nagata.W07.normalizedThetaDerivativeTerm, OAI.Nagata.W07.thetaMargin

theorem OAI.Nagata.W07.norm_normalizedThetaTerm_le line 268

Source documentation

The order-zero bound used to establish convergence of the actual series.

theorem norm_normalizedThetaTerm_le {n a K τ R : ℝ} {ε x : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hx : ‖x‖ ≤ R) (p : ℤ) :
    ‖normalizedThetaTerm n a K ε τ p x‖ ≤ Real.exp (|K| * R) *
      (Real.exp (n * R) * τ ^ thetaMargin n a) ^ p.natAbs := by
…

Mentions: OAI.Nagata.W07.normalizedThetaTerm, OAI.Nagata.W07.thetaMargin

theorem OAI.Nagata.W07.complex_rpow_zpow line 292

Source documentation

Integer powers of a positive real power, viewed in the complex field.

theorem complex_rpow_zpow {τ : ℝ} (hτ : 0 ≤ τ) (s : ℝ) (p : ℤ) :
    (((τ ^ s : ℝ) : ℂ) ^ p) = ((τ ^ (s * (p : ℝ)) : ℝ) : ℂ) := by
…

def OAI.Nagata.W07.normalizedLaurentCoefficient line 297
Source documentation
The coefficient chosen in the manuscript, before evaluating at the moving center.
```
def normalizedLaurentCoefficient (τ σ x₀ : ℝ) (ε : ℂ) (n K p : ℤ) : ℂ :=
…
```
theorem OAI.Nagata.W07.normalizedLaurentCoefficient_zero line 301

theorem OAI.Nagata.W07.normalizedLaurentCoefficient_source_formula line 308

Source documentation

The printed real-quadratic form of the chosen coefficient.

theorem normalizedLaurentCoefficient_source_formula
    (τ σ x₀ : ℝ) (ε : ℂ) (n K p : ℤ) :
    normalizedLaurentCoefficient τ σ x₀ ε n K p =
      ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) * ε ^ (-p) *
        ((τ ^ (-σ * (p : ℝ) + (p : ℝ) * (K : ℝ) +
          (n : ℝ) * (p : ℝ) * ((p : ℝ) - 1) / 2) : ℝ) : ℂ) := by
…

Mentions: OAI.Nagata.W07.normalizedLaurentCoefficient

theorem OAI.Nagata.W07.normalizedLaurentCoefficient_eq_orbitValue line 319

theorem OAI.Nagata.W07.normalizedLaurentCoefficient_add_one line 331

Source documentation

The explicitly defined chosen coefficients themselves obey the Laurent recurrence.

theorem normalizedLaurentCoefficient_add_one {τ : ℝ} (hτ : 0 < τ)
    (σ x₀ : ℝ) {ε : ℂ} (hε : ε ≠ 0) (n K p : ℤ) :
    normalizedLaurentCoefficient τ σ x₀ ε n K (p + 1) =
      ((ε * ((τ ^ σ : ℝ) : ℂ))⁻¹ * (τ : ℂ) ^ (K + n * p)) *
        normalizedLaurentCoefficient τ σ x₀ ε n K p := by
…

Mentions: OAI.Nagata.W07.normalizedLaurentCoefficient

theorem OAI.Nagata.W07.normalizedLaurentCoefficient_of_recurrence line 345

Source documentation

The coefficient is exactly the nonzero starting coefficient propagated through the Laurent recurrence, with γ = ε * τ^σ.

theorem normalizedLaurentCoefficient_of_recurrence {τ : ℝ} (hτ : 0 < τ)
    (σ x₀ : ℝ) {ε : ℂ} (hε : ε ≠ 0) (n K : ℤ) (c : ℤ → ℂ)
    (hc : ∀ L : ℤ, c (L + n) =
      (ε * ((τ ^ σ : ℝ) : ℂ))⁻¹ * (τ : ℂ) ^ L * c L)
    (hstart : c K = ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ)) (p : ℤ) :
    c (K + n * p) = normalizedLaurentCoefficient τ σ x₀ ε n K p := by
…

Mentions: OAI.Nagata.W07.normalizedLaurentCoefficient

theorem OAI.Nagata.W07.normalizedLaurentCoefficient_eval line 368

Source documentation

Evaluating the propagated coefficient at z₀*exp x, with z₀=τ^x₀, gives exactly the normalized summand used in the analytic estimates.

theorem normalizedLaurentCoefficient_eval {τ : ℝ} (hτ : 0 < τ)
    (σ x₀ : ℝ) (ε x : ℂ) (n K p : ℤ) :
    normalizedLaurentCoefficient τ σ x₀ ε n K p *
        (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) ^ (K + n * p) =
      normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
        (K : ℝ) ε τ p x := by
…

Mentions: OAI.Nagata.W07.normalizedLaurentCoefficient, OAI.Nagata.W07.normalizedThetaTerm

theorem OAI.Nagata.W07.normalized_recurrence_eval line 394

Source documentation

Combined recurrence-to-local-summand bridge, without an intermediate model.

theorem normalized_recurrence_eval {τ : ℝ} (hτ : 0 < τ)
    (σ x₀ : ℝ) {ε : ℂ} (hε : ε ≠ 0) (n K : ℤ) (c : ℤ → ℂ)
    (hc : ∀ L : ℤ, c (L + n) =
      (ε * ((τ ^ σ : ℝ) : ℂ))⁻¹ * (τ : ℂ) ^ L * c L)
    (hstart : c K = ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ)) (p : ℤ) (x : ℂ) :
    c (K + n * p) * (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) ^ (K + n * p) =
      normalizedThetaTerm (n : ℝ) ((K : ℝ) - σ + x₀ * (n : ℝ))
        (K : ℝ) ε τ p x := by
…

Mentions: OAI.Nagata.W07.normalizedThetaTerm

theorem OAI.Nagata.W07.normalizedThetaTerm_shift line 408

Source documentation

The equivalent termwise normalization in logarithmic coordinates.

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

Mentions: OAI.Nagata.W07.normalizedThetaTerm

theorem OAI.Nagata.W07.normalization_scalar_pos line 440
Source documentation
Real rescaling used for the selected starting coefficient is strictly positive.
```
theorem normalization_scalar_pos {τ : ℝ} (hτ : 0 < τ) (x₀ : ℝ) (K : ℤ) :
    0 < τ ^ (-x₀ * (K : ℝ)) := Real.rpow_pos_of_pos hτ _
```
theorem OAI.Nagata.W07.normalization_scalar_ne_zero line 444
Source documentation
In particular, the normalized starting coefficient is nonzero in the complex field.
```
theorem normalization_scalar_ne_zero {τ : ℝ} (hτ : 0 < τ) (x₀ : ℝ) (K : ℤ) :
    ((τ ^ (-x₀ * (K : ℝ)) : ℝ) : ℂ) ≠ 0 := by
…
```

theorem OAI.Nagata.W07.normalizedLaurentCoefficient_ne_zero line 449

Source documentation

No propagated coefficient in the selected residue class vanishes.

theorem normalizedLaurentCoefficient_ne_zero {τ : ℝ} (hτ : 0 < τ)
    (σ x₀ : ℝ) {ε : ℂ} (hε : ε ≠ 0) (n K p : ℤ) :
    normalizedLaurentCoefficient τ σ x₀ ε n K p ≠ 0 := by
…

Mentions: OAI.Nagata.W07.normalizedLaurentCoefficient