Multipliers.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Scalar normalization of automorphic multipliers; Low- and high-degree coefficient-space correspondence

def OAI.Nagata.W02.multiplierSigma line 20
Source documentation
Real exponent carrying the absolute value of the multiplier.
```
def multiplierSigma (τ : ℝ) (γ : ℂ) : ℝ := Real.log ‖γ‖ / Real.log τ
```
def OAI.Nagata.W02.multiplierPhase line 23
Source documentation
Unit-norm phase, defined directly from the original multiplier.
```
def multiplierPhase (γ : ℂ) : ℂ := γ / (‖γ‖ : ℂ)
```

theorem OAI.Nagata.W02.rpow_multiplierSigma line 26

Source documentation

The real scaling is exactly the multiplier norm.

theorem rpow_multiplierSigma {τ : ℝ} {γ : ℂ}
    (hτ : 0 < τ) (hτ1 : τ < 1) (hγ : γ ≠ 0) :
    τ ^ multiplierSigma τ γ = ‖γ‖ := by
…

Mentions: OAI.Nagata.W02.multiplierSigma

theorem OAI.Nagata.W02.norm_multiplierPhase line 36
Source documentation
The phase is genuinely unit norm, for every nonzero multiplier.
```
theorem norm_multiplierPhase {γ : ℂ} (hγ : γ ≠ 0) : ‖multiplierPhase γ‖ = 1 := by
…
```
Mentions: OAI.Nagata.W02.multiplierPhase
theorem OAI.Nagata.W02.multiplier_factorization line 43
Source documentation
The original complex multiplier is recovered exactly, with all real/complex coercions explicit.
```
theorem multiplier_factorization {τ : ℝ} {γ : ℂ}
    (hτ : 0 < τ) (hτ1 : τ < 1) (hγ : γ ≠ 0) :
    γ = multiplierPhase γ * ((τ ^ multiplierSigma τ γ : ℝ) : ℂ) := by
…
```
Mentions: OAI.Nagata.W02.multiplierPhase, OAI.Nagata.W02.multiplierSigma
def OAI.Nagata.W02.thetaFrameCenter line 53
Source documentation
Frame center forcing the source interval's left endpoint to be one half.
```
def thetaFrameCenter (n σ : ℝ) : ℝ := (σ - 1 / 2) / n
```
theorem OAI.Nagata.W02.thetaFrameCenter_endpoint line 55
theorem OAI.Nagata.W02.half_not_integer line 61
theorem OAI.Nagata.W02.thetaFrameCenter_nonintegral line 69

theorem OAI.Nagata.W02.exists_normalized_multiplier_frame line 76

Source documentation

Fully explicit phase/exponent/frame choices for arbitrary γ in ℂ*. No unit-norm or nonintegrality premise is left to the caller.

theorem exists_normalized_multiplier_frame {n τ : ℝ} {γ : ℂ}
    (hn : 0 < n) (hτ : 0 < τ) (hτ1 : τ < 1) (hγ : γ ≠ 0) :
    ∃ (σ x0 : ℝ) (ε : ℂ), ‖ε‖ = 1 ∧
      γ = ε * ((τ ^ σ : ℝ) : ℂ) ∧
      σ - x0 * n = 1 / 2 ∧
      σ - x0 * n ∉ Set.range (Int.cast : ℤ → ℝ) := by
…

theorem OAI.Nagata.BundleArithmetic.coefficient_degree line 99
Source documentation
The degree of T ⊗ A^(m-j) is independent of j, because A has degree zero.
```
theorem coefficient_degree (d m j : ℝ) :
    3 * (d - 3 * m) + (m - j) * (3 * 3 - 9) = 3 * (d - 3 * m) := by
…
```
theorem OAI.Nagata.BundleArithmetic.source_degree line 104
Source documentation
Degree of the source of the second coefficient block.
```
theorem source_degree (d m j : ℝ) :
    3 * (d - 3 * j) = 3 * (d - 3 * m) - 9 * (j - m) := by
…
```
theorem OAI.Nagata.BundleArithmetic.twisted_source_degree line 109
Source documentation
Multiplication by the marked divisor raises that source degree to h.
```
theorem twisted_source_degree (d m j : ℝ) :
    3 * (d - 3 * j) + 9 * (j - m) = 3 * (d - 3 * m) := by
…
```
theorem OAI.Nagata.BundleArithmetic.normal_minus_marked_exponent line 114
Source documentation
Scalar exponent in the multiplier of A = L^3 ⊗ O(-P).
```
theorem normal_minus_marked_exponent (s a : ℝ) :
    3 * ((s + a) / 3) - s = a := by
…
```
theorem OAI.Nagata.BundleArithmetic.eta_shift line 119
Source documentation
The defining marked-point relation fixes the shifted exponent exactly.
```
theorem eta_shift (s a Δ x₀ : ℝ) (hs : s = 9 * x₀ - Δ) :
    (s + a) / 3 - 3 * x₀ = (a - Δ) / 3 := by
…
```
theorem OAI.Nagata.BundleArithmetic.total_bundle_exponent line 125
Source documentation
Exponent identity for T ⊗ A^m = L^d ⊗ O(-mP).
```
theorem total_bundle_exponent (d m s a : ℝ) :
    (d - 3 * m) * ((s + a) / 3) + m * a =
      d * ((s + a) / 3) - m * s := by
…
```

theorem OAI.Nagata.BundleArithmetic.twisted_source_exponent line 131

Source documentation

Exponent compatibility of the positive-j source with the marked twist.

theorem twisted_source_exponent (d m j s a : ℝ) :
    (d - 3 * j) * ((s + a) / 3) + (j - m) * s =
      (d - 3 * m) * ((s + a) / 3) + (m - j) * a := by
…

theorem OAI.Nagata.BundleArithmetic.first_interval_parameter line 137

Source documentation

Subtracting x₀ times degree yields the first theta interval's U_j.

theorem first_interval_parameter (d m j s a Δ x₀ : ℝ)
    (hs : s = 9 * x₀ - Δ) :
    ((d - 3 * m) * ((s + a) / 3) + (m - j) * a) -
        x₀ * (3 * (d - 3 * m)) =
      (3 * (d - 3 * m)) / 9 * (a - Δ) + (m - j) * a := by
…

theorem OAI.Nagata.BundleArithmetic.second_interval_parameter line 146

Source documentation

The corresponding parameter for the second block's untwisted source.

theorem second_interval_parameter (d j s a Δ x₀ : ℝ)
    (hs : s = 9 * x₀ - Δ) :
    (d - 3 * j) * ((s + a) / 3) - x₀ * (3 * (d - 3 * j)) =
      (3 * (d - 3 * j)) / 9 * (a - Δ) := by
…

theorem OAI.Nagata.BundleArithmetic.interval_seam line 154

Source documentation

At j=m the two interval formulas agree, including their length.

theorem interval_seam (d m a Δ : ℝ) :
    (3 * (d - 3 * m)) / 9 * (a - Δ) + (m - m) * a =
      (3 * (d - 3 * m)) / 9 * (a - Δ) := by
…

theorem OAI.Nagata.BundleArithmetic.first_interval_translation line 160
Source documentation
The first block's interval is translated from the j=0 interval by -a*j.
```
theorem first_interval_translation (h m j a Δ : ℝ) :
    h / 9 * (a - Δ) + (m - j) * a =
      (h / 9 * (a - Δ) + m * a) - a * j := by
…
```
theorem OAI.Nagata.BundleArithmetic.degree_zero_index line 166
Source documentation
The degree-zero index is the unique real solution of d-3j=0.
```
theorem degree_zero_index (d j : ℝ) (hz : d - 3 * j = 0) :
    j = d / 3 := by
…
```
theorem OAI.Nagata.BundleArithmetic.degree_zero_after_m line 171
Source documentation
With d>3m, the degree-zero block belongs to the second branch.
```
theorem degree_zero_after_m (d m j : ℝ) (hd : 3 * m < d)
    (hz : d - 3 * j = 0) : m < j := by
…
```
theorem OAI.Nagata.BundleArithmetic.degree_zero_tip_index line 176
Source documentation
The j-coordinate of the tip in terms of h.
```
theorem degree_zero_tip_index (d m j : ℝ) (hz : d - 3 * j = 0) :
    j = m + (3 * (d - 3 * m)) / 9 := by
…
```

theorem OAI.Nagata.BundleArithmetic.degree_zero_endpoints line 181

Source documentation

Both source interval endpoints collapse to K=0 at a zero-degree block.

theorem degree_zero_endpoints (d j a Δ : ℝ) (hz : d - 3 * j = 0) :
    (3 * (d - 3 * j)) / 9 * (a - Δ) = 0 ∧
      (3 * (d - 3 * j)) / 9 * (a - Δ) + 3 * (d - 3 * j) = 0 := by
…

theorem OAI.Nagata.BundleArithmetic.degree_zero_divisibility line 187
Source documentation
Integer indices with degree-zero source exist only at degrees divisible by 3.
```
theorem degree_zero_divisibility (d j : ℤ) (hz : d - 3 * j = 0) : 3 ∣ d := by
…
```
theorem OAI.Nagata.BundleArithmetic.degree_zero_index_unique line 192
Source documentation
At most one integer index can contribute a degree-zero block.
```
theorem degree_zero_index_unique (d j k : ℤ)
    (hj : d - 3 * j = 0) (hk : d - 3 * k = 0) : j = k := by
…
```
theorem OAI.Nagata.CoefficientSpaces.coefficient_multiplier_identity line 207
Source documentation
Fixed-frame multiplier identity for the source coefficient twisted by the marked divisor. Unlike the real exponent identities, this is an equality of actual complex transition multipliers with integer powers.
```
theorem coefficient_multiplier_identity {L Q : ℂ} (hL : L ≠ 0) (d m j : ℤ) :
    L ^ (d - 3 * j) * Q ^ (j - m) =
      L ^ (d - 3 * m) * normalMinusMarkedMultiplier L Q ^ (m - j) := by
…
```
Mentions: OAI.Nagata.CoefficientSpaces.normalMinusMarkedMultiplier
theorem OAI.Nagata.CoefficientSpaces.quotient_coefficient_multiplier line 221
Source documentation
The low-index quotient has exactly the common coefficient multiplier.
```
theorem quotient_coefficient_multiplier {L Q : ℂ} (hL : L ≠ 0) (d m j : ℤ) :
    L ^ (d - 3 * j) / Q ^ (m - j) =
      L ^ (d - 3 * m) * normalMinusMarkedMultiplier L Q ^ (m - j) := by
…
```
Mentions: OAI.Nagata.CoefficientSpaces.normalMinusMarkedMultiplier
theorem OAI.Nagata.CoefficientSpaces.coefficientSpace_le_common line 239
Source documentation
Every literal coefficient block lies in the common multiplier section space. This proves the global transition compatibility of both source branches.
```
theorem coefficientSpace_le_common {τ L Q : ℂ} (hL : L ≠ 0)
    (d m j : ℤ) (P : ℂ → ℂ)
    (hP : P ∈ Nagata.W08.automorphicSections τ 9 Q) :
    coefficientSpace τ L Q d m j P ≤
      Nagata.W08.automorphicSections τ (3 * (d - 3 * m))
        (L ^ (d - 3 * m) * normalMinusMarkedMultiplier L Q ^ (m - j)) := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.coefficientSpace, OAI.Nagata.CoefficientSpaces.normalMinusMarkedMultiplier

theorem OAI.Nagata.CoefficientSpaces.exists_low_coefficient line 262

Source documentation

Actual low-index division constructs a coefficient in V_j, including all marked points: the source section's ordinary vanishing order supplies extension.

theorem exists_low_coefficient {τ L Q : ℂ} (hτ : τ ≠ 0) (hL : L ≠ 0) (hQ : Q ≠ 0)
    (d m j : ℤ) (hj : j ≤ m)
    (P : Nagata.W08.automorphicSections τ 9 Q)
    (f : Nagata.W08.automorphicSections τ (3 * (d - 3 * j)) (L ^ (d - 3 * j)))
    (hP : AnalyticOnNhd ℂ P.val {z | z ≠ 0})
    (hf : AnalyticOnNhd ℂ f.val {z | z ≠ 0})
    (hzero : ∀ z ≠ 0, P.val z = 0 → deriv P.val z ≠ 0 ∧
      ((m - j).toNat : ℕ∞) ≤ analyticOrderAt f.val z) :
    ∃ g ∈ coefficientSpace τ L Q d m j P.val,
      ∀ z ≠ 0, f.val z = P.val z ^ (m - j).toNat * g z := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.coefficientSpace