ThetaEvaluation.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Evaluation kernels and orbit jets of theta sections

theorem OAI.Nagata.W07.section_zero_mul_iff line 20

theorem OAI.Nagata.W07.section_deriv_mul_at_zero line 26

Source documentation

Differentiate the actual automorphy equation at a zero.

theorem section_deriv_mul_at_zero {τ γ z : ℂ} {n : ℤ}
    (hτ : τ ≠ 0) (hz : z ≠ 0) (f : automorphicSections τ n γ)
    (hfz : f.val z = 0) :
    deriv f.val (τ * z) * τ = (γ * z ^ (-n)) * deriv f.val z := by
…

theorem OAI.Nagata.W07.section_firstJet_zero_mul_iff line 41

theorem OAI.Nagata.W07.invariant_zpow line 59

Source documentation

Invariance under one invertible generator implies invariance under all integer powers.

theorem invariant_zpow {G α : Type*} [CommGroup G] (τ : G) (F : G → α)
    (hstep : ∀ z, F (τ * z) = F z) (z : G) (k : ℤ) : F (τ ^ k * z) = F z := by
…

theorem OAI.Nagata.W07.section_zero_orbit_iff line 73
theorem OAI.Nagata.W07.section_firstJet_zero_orbit_iff line 83

theorem OAI.Nagata.W07.section_order_one_iff line 96

Source documentation

Order at least one means the ordinary value vanishes, including the zero section.

theorem section_order_one_iff {τ γ z : ℂ} {n : ℤ}
    (f : automorphicSections τ n γ) (hz : z ≠ 0) :
    (1 : ℕ∞) ≤ analyticOrderAt f.val z ↔ f.val z = 0 := by
…

theorem OAI.Nagata.W07.section_order_two_iff line 104

Source documentation

Order at least two means the actual value and first derivative both vanish.

theorem section_order_two_iff {τ γ z : ℂ} {n : ℤ}
    (f : automorphicSections τ n γ) (hz : z ≠ 0) :
    (2 : ℕ∞) ≤ analyticOrderAt f.val z ↔ f.val z = 0 ∧ deriv f.val z = 0 := by
…

def OAI.Nagata.W07.pointThetaMultiply line 132

Source documentation

Multiplication by the actual marked theta section to its kth power.

def pointThetaMultiply {τ a : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0)
    (n : ℤ) (γ : ℂ) (k : ℕ) :
    automorphicSections τ (n - (k : ℤ)) (γ / (-a) ^ k) →ₗ[ℂ]
      automorphicSections τ n γ :=
…

theorem OAI.Nagata.W07.pointThetaMultiply_apply line 148

theorem OAI.Nagata.W07.pointTheta_order_ne_top line 155

Source documentation

The actual theta multiplier has finite zero order at every genuine point.

theorem pointTheta_order_ne_top {τ a z : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hz : z ≠ 0) :
    analyticOrderAt (thetaProductSection hτ hτ0 ha).val z ≠ ⊤ := by
…

theorem OAI.Nagata.W07.pointThetaMultiply_injective line 165

theorem OAI.Nagata.W07.pointThetaMultiply_range_eq_eval_kernel line 176

Source documentation

Dividing a section vanishing at the marked point by its genuine theta factor.

theorem pointThetaMultiply_range_eq_eval_kernel {τ a γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hγ : γ ≠ 0) (n : ℤ) :
    LinearMap.range (pointThetaMultiply hτ hτ0 ha n γ 1) =
      LinearMap.ker (sectionEval τ n γ a) := by
…

Mentions: OAI.Nagata.W07.pointThetaMultiply, OAI.Nagata.W07.sectionEval

theorem OAI.Nagata.W07.pointThetaMultiply_range_eq_firstJet_kernel line 207

Source documentation

The square of the actual theta factor identifies the genuine double-point kernel.

theorem pointThetaMultiply_range_eq_firstJet_kernel {τ a γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hγ : γ ≠ 0) (n : ℤ) :
    LinearMap.range (pointThetaMultiply hτ hτ0 ha n γ 2) =
      LinearMap.ker (sectionFirstJet τ n γ ha) := by
…

Mentions: OAI.Nagata.W07.pointThetaMultiply, OAI.Nagata.W07.sectionFirstJet

theorem OAI.Nagata.W07.sectionEval_kernel_finrank line 246

Source documentation

Exact kernel dimension transfer; the lower-degree section dimension remains explicit.

theorem sectionEval_kernel_finrank {τ a γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hγ : γ ≠ 0) (n : ℤ) :
    Module.finrank ℂ (LinearMap.ker (sectionEval τ n γ a)) =
      Module.finrank ℂ (automorphicSections τ (n - 1) (γ / (-a))) := by
…

Mentions: OAI.Nagata.W07.sectionEval

theorem OAI.Nagata.W07.sectionFirstJet_kernel_finrank line 255

def OAI.Nagata.W07.twoPointThetaMultiply line 281

Source documentation

Restrict multiplication by the first theta factor to sections vanishing at the second point.

def twoPointThetaMultiply {τ a : ℂ} (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0)
    (n : ℤ) (γ b : ℂ) :
    LinearMap.ker (sectionEval τ (n - (1 : ℤ)) (γ / (-a) ^ 1) b) →ₗ[ℂ]
      automorphicSections τ n γ :=
…

Mentions: OAI.Nagata.W07.sectionEval

theorem OAI.Nagata.W07.twoPointThetaMultiply_injective line 288

theorem OAI.Nagata.W07.twoPointThetaMultiply_range_eq_twoEval_kernel line 294

Source documentation

Exact range identification for two inequivalent lifts on the actual torus.

theorem twoPointThetaMultiply_range_eq_twoEval_kernel {τ a b γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hb : b ≠ 0)
    (hγ : γ ≠ 0) (hab : ¬ ∃ k : ℤ, b = a * τ ^ k) (n : ℤ) :
    LinearMap.range (twoPointThetaMultiply hτ hτ0 ha n γ b) =
      LinearMap.ker (sectionTwoEval τ n γ a b) := by
…

Mentions: OAI.Nagata.W07.twoPointThetaMultiply, OAI.Nagata.W07.sectionTwoEval

theorem OAI.Nagata.W07.sectionTwoEval_kernel_finrank line 326

Source documentation

Exact lower-degree dimension transfer for the two-point vanishing subspace.

theorem sectionTwoEval_kernel_finrank {τ a b γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (ha : a ≠ 0) (hb : b ≠ 0)
    (hγ : γ ≠ 0) (hab : ¬ ∃ k : ℤ, b = a * τ ^ k) (n : ℤ) :
    Module.finrank ℂ (LinearMap.ker (sectionTwoEval τ n γ a b)) =
      Module.finrank ℂ (automorphicSections τ (n - 2) ((γ / (-a)) / (-b))) := by
…

Mentions: OAI.Nagata.W07.sectionTwoEval