LaurentCoefficients.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Analytic Laurent coefficients, integral transforms, and recurrences

def OAI.Nagata.W09.analyticLaurentCoeff line 27
Source documentation
The actual kth Laurent coefficient obtained on the circle of radius r.
```
noncomputable def analyticLaurentCoeff (r : ℝ) (f : ℂ → ℂ) (k : ℤ) : ℂ :=
…
```
theorem OAI.Nagata.W09.differentiableAt_laurentIntegrand line 31
theorem OAI.Nagata.W09.circleIntegrable_laurentIntegrand line 36
theorem OAI.Nagata.W09.analyticLaurentCoeff_add line 47
theorem OAI.Nagata.W09.analyticLaurentCoeff_smul line 56
def OAI.Nagata.W09.laurentCoefficientMap line 69
Source documentation
Actual Laurent-coefficient extraction at radius one is a linear map on the existing analytic automorphic-section space.
```
noncomputable def laurentCoefficientMap (τ : ℂ) (n : ℤ) (γ : ℂ) :
    Nagata.W08.automorphicSections τ n γ →ₗ[ℂ] (ℤ → ℂ) where
…
```
Mentions: OAI.Nagata.W08.automorphicSections
theorem OAI.Nagata.W09.laurentCoefficientMap_apply line 79

theorem OAI.Nagata.W09.hasSum_circleIntegral_of_summable_bound line 96

Source documentation

Countable circle-integral exchange under an actual summable bound on the circle. This is dominated convergence applied to the literal parametrization.

theorem hasSum_circleIntegral_of_summable_bound
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (F : ι → ℂ → ℂ) (f : ℂ → ℂ) (B : ι → ℝ)
    (hB : Summable B)
    (hcont : ∀ i, ContinuousOn (F i) (sphere 0 r))
    (hbound : ∀ i z, z ∈ sphere 0 r → ‖F i z‖ ≤ B i)
    (hsum : ∀ z, z ∈ sphere 0 r → HasSum (fun i => F i z) (f z)) :
    HasSum (fun i => ∮ z in C(0, r), F i z) (∮ z in C(0, r), f z) := by
…

theorem OAI.Nagata.W09.hasSum_analyticLaurentCoeff_of_summable_bound line 120

Source documentation

Actual Laurent coefficients commute with a pointwise series whose weighted terms have a summable uniform bound on the integration circle.

theorem hasSum_analyticLaurentCoeff_of_summable_bound
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (F : ι → ℂ → ℂ) (f : ℂ → ℂ) (k : ℤ) (B : ι → ℝ)
    (hB : Summable B)
    (hcont : ∀ i, ContinuousOn (F i) (sphere 0 r))
    (hbound : ∀ i z, z ∈ sphere 0 r → ‖z ^ (-k - 1) * F i z‖ ≤ B i)
    (hsum : ∀ z, z ∈ sphere 0 r → HasSum (fun i => F i z) (f z)) :
    HasSum (fun i => analyticLaurentCoeff r (F i) k) (analyticLaurentCoeff r f k) := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.hasSum_analyticLaurentCoeff_of_bound line 142

Source documentation

The convenient unweighted version: a summable uniform bound for the original series suffices for every fixed Laurent coefficient.

theorem hasSum_analyticLaurentCoeff_of_bound
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (F : ι → ℂ → ℂ) (f : ℂ → ℂ) (k : ℤ) (B : ι → ℝ)
    (hB : Summable B)
    (hcont : ∀ i, ContinuousOn (F i) (sphere 0 r))
    (hbound : ∀ i z, z ∈ sphere 0 r → ‖F i z‖ ≤ B i)
    (hsum : ∀ z, z ∈ sphere 0 r → HasSum (fun i => F i z) (f z)) :
    HasSum (fun i => analyticLaurentCoeff r (F i) k) (analyticLaurentCoeff r f k) := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.exists_circle_angle_of_mem_sphere line 160
Source documentation
Every point on a positive-radius circle has an angle in one fixed compact period; this permits the fixed-disk theta majorant to control the whole circle.
```
theorem exists_circle_angle_of_mem_sphere {r : ℝ} (hr : 0 < r) {z : ℂ}
    (hz : z ∈ sphere 0 r) :
    ∃ θ ∈ Set.Ioc (0 : ℝ) (2 * Real.pi), circleMap 0 r θ = z := by
…
```

theorem OAI.Nagata.W09.hasSum_analyticLaurentCoeff_of_parametric_bound line 170

Source documentation

The circle-bound criterion in the exact fixed-angle form used by the normalized theta series on the moving physical circle r=z0.

theorem hasSum_analyticLaurentCoeff_of_parametric_bound
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (F : ι → ℂ → ℂ) (f : ℂ → ℂ) (k : ℤ) (B : ι → ℝ)
    (hB : Summable B)
    (hcont : ∀ i, ContinuousOn (F i) (sphere 0 r))
    (hbound : ∀ i θ, θ ∈ Set.Ioc (0 : ℝ) (2 * Real.pi) →
      ‖F i (circleMap 0 r θ)‖ ≤ B i)
    (hsum : ∀ θ, θ ∈ Set.Ioc (0 : ℝ) (2 * Real.pi) →
      HasSum (fun i => F i (circleMap 0 r θ)) (f (circleMap 0 r θ))) :
    HasSum (fun i => analyticLaurentCoeff r (F i) k) (analyticLaurentCoeff r f k) := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.analyticLaurentCoeff_congr line 199

Source documentation

Agreement on the actual integration circle gives agreement of coefficients.

theorem analyticLaurentCoeff_congr {r : ℝ} (hr : 0 ≤ r) {f g : ℂ → ℂ}
    (h : Set.EqOn f g (Metric.sphere 0 r)) (k : ℤ) :
    analyticLaurentCoeff r f k = analyticLaurentCoeff r g k := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.circleIntegral_scale_real line 210

Source documentation

Change of parametrization for dilation by a real scalar.

theorem circleIntegral_scale_real (a r : ℝ) (f : ℂ → ℂ) :
    (∮ z in C(0, a * r), f z) =
      (a : ℂ) * ∮ z in C(0, r), f ((a : ℂ) * z) := by
…

theorem OAI.Nagata.W09.analyticLaurentCoeff_zpow_mul line 226

Source documentation

Multiplication by z^(-n) shifts the actual Laurent coefficient index by n.

theorem analyticLaurentCoeff_zpow_mul {r : ℝ} (hr : 0 < r)
    (f : ℂ → ℂ) (n k : ℤ) :
    analyticLaurentCoeff r (fun z => z ^ (-n) * f z) k =
      analyticLaurentCoeff r f (k + n) := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.analyticLaurentCoeff_comp_pos_mul line 245
Source documentation
Dilation transforms the genuine circle coefficient by the corresponding integer power. This identity itself does not require holomorphy.
```
theorem analyticLaurentCoeff_comp_pos_mul {a : ℝ} (ha : 0 < a)
    (r : ℝ) (f : ℂ → ℂ) (k : ℤ) :
    analyticLaurentCoeff r (fun z => f ((a : ℂ) * z)) k =
      (a : ℂ) ^ k * analyticLaurentCoeff (a * r) f k := by
…
```
Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.circleIntegral_radius_eq_of_holomorphic_punctured line 281

Source documentation

Cauchy-Goursat on a genuine closed annulus, specialized to functions holomorphic on the whole punctured plane.

theorem circleIntegral_radius_eq_of_holomorphic_punctured
    {r R : ℝ} (hr : 0 < r) (hle : r ≤ R) {f : ℂ → ℂ}
    (hf : ∀ z, z ≠ 0 → DifferentiableAt ℂ f z) :
    (∮ z in C(0, R), f z) = ∮ z in C(0, r), f z := by
…

theorem OAI.Nagata.W09.analyticLaurentCoeff_radius_independent line 302
Source documentation
Laurent coefficients of a genuinely holomorphic punctured-plane function are independent of the positive circle radius.
```
theorem analyticLaurentCoeff_radius_independent
    {r s : ℝ} (hr : 0 < r) (hs : 0 < s) {f : ℂ → ℂ}
    (hf : ∀ z, z ≠ 0 → DifferentiableAt ℂ f z) (k : ℤ) :
    analyticLaurentCoeff r f k = analyticLaurentCoeff s f k := by
…
```
Mentions: OAI.Nagata.W09.analyticLaurentCoeff
def OAI.Nagata.W09.supportedOrbitCoefficient line 330
Source documentation
Extend the explicit orbit formula by zero outside the residue class of K.
```
noncomputable def supportedOrbitCoefficient (τ γ : F) (n K : ℤ) (c₀ : F) (k : ℤ) : F :=
…
```
theorem OAI.Nagata.W09.supportedOrbitCoefficient_initial line 333
theorem OAI.Nagata.W09.supportedOrbitCoefficient_support line 337
theorem OAI.Nagata.W09.supportedOrbitCoefficient_residue line 342
theorem OAI.Nagata.W09.supportedOrbitCoefficient_on_orbit line 347

theorem OAI.Nagata.W09.supportedOrbitCoefficient_recurrence line 355

Source documentation

The supported sequence satisfies the original one-step Laurent recurrence at every integer, including positions outside its support.

theorem supportedOrbitCoefficient_recurrence (τ γ : F) (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    {n : ℤ} (hn : n ≠ 0) (K : ℤ) (c₀ : F) (k : ℤ) :
    supportedOrbitCoefficient τ γ n K c₀ (k + n) =
      γ⁻¹ * τ ^ k * supportedOrbitCoefficient τ γ n K c₀ k := by
…

Mentions: OAI.Nagata.W09.supportedOrbitCoefficient

theorem OAI.Nagata.W09.analyticLaurentCoeff_balance_pos_real line 388
Source documentation
The multiplier equation gives the exact coefficient balance by genuine circle integration. Positive real tau is the manuscript's actual parameter.
```
theorem analyticLaurentCoeff_balance_pos_real {τ : ℝ} (hτ : 0 < τ)
    (n : ℤ) (γ : ℂ) (f : Nagata.W08.automorphicSections (τ : ℂ) n γ) (k : ℤ) :
    (τ : ℂ) ^ k * analyticLaurentCoeff 1 f.val k =
      γ * analyticLaurentCoeff 1 f.val (k + n) := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.laurentCoefficientMap_recurrence_pos_real line 413

Source documentation

The genuine analytic extraction map satisfies the exact source recurrence; no recurrence is assumed as a field of the analytic section space.

theorem laurentCoefficientMap_recurrence_pos_real {τ : ℝ} (hτ : 0 < τ)
    (n : ℤ) (γ : ℂ) (hγ : γ ≠ 0)
    (f : Nagata.W08.automorphicSections (τ : ℂ) n γ) (k : ℤ) :
    laurentCoefficientMap (τ : ℂ) n γ f (k + n) =
      γ⁻¹ * (τ : ℂ) ^ k * laurentCoefficientMap (τ : ℂ) n γ f k := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W09.laurentCoefficientMap

theorem OAI.Nagata.W09.analyticLaurentCoeff_monomial line 433
Source documentation
The actual circle integral extracts precisely one Laurent monomial.
```
theorem analyticLaurentCoeff_monomial {r : ℝ} (hr : 0 < r) (j k : ℤ) :
    analyticLaurentCoeff r (fun z => z ^ j) k = if j = k then 1 else 0 := by
…
```
Mentions: OAI.Nagata.W09.analyticLaurentCoeff
theorem OAI.Nagata.W09.analyticLaurentCoeff_smul_monomial line 467
Source documentation
Scalar Laurent monomials have their literal scalar as the extracted coefficient, and zero in every other integer degree.
```
theorem analyticLaurentCoeff_smul_monomial {r : ℝ} (hr : 0 < r)
    (a : ℂ) (j k : ℤ) :
    analyticLaurentCoeff r (fun z => a * z ^ j) k = if j = k then a else 0 := by
…
```
Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.laurent_recurrence_eq_of_thetaIndices line 485

Source documentation

A genuine Laurent recurrence sequence is determined by its coefficients in one complete residue interval. This proves uniqueness of coefficients, not existence or injectivity of analytic Laurent expansion.

theorem laurent_recurrence_eq_of_thetaIndices
    {F : Type*} [CommGroupWithZero F] (τ γ : F) (hτ : τ ≠ 0) (hγ : γ ≠ 0)
    (U : ℝ) {n : ℤ} (hn : 0 < n) (c d : ℤ → F)
    (hc : ∀ k, c (k + n) = γ⁻¹ * τ ^ k * c k)
    (hd : ∀ k, d (k + n) = γ⁻¹ * τ ^ k * d k)
    (hinitial : ∀ K ∈ thetaIndices U n, c K = d K) : c = d := by
…

Mentions: OAI.Nagata.W09.thetaIndices

theorem OAI.Nagata.W09.continuousOn_scalar_monomial_circle line 511

theorem OAI.Nagata.W09.hasSum_analyticLaurentCoeff_of_monomial_series line 523

Source documentation

Coefficient extraction from a genuinely normally convergent Laurent-monomial series is the sum of the literal coefficients in the matching integer degree.

theorem hasSum_analyticLaurentCoeff_of_monomial_series
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (a : ι → ℂ) (N : ι → ℤ) (f : ℂ → ℂ) (B : ι → ℝ)
    (hB : Summable B)
    (hbound : ∀ i z, z ∈ sphere 0 r → ‖a i * z ^ N i‖ ≤ B i)
    (hsum : ∀ z, z ∈ sphere 0 r → HasSum (fun i => a i * z ^ N i) (f z)) (k : ℤ) :
    HasSum (fun i => if N i = k then a i else 0) (analyticLaurentCoeff r f k) := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.analyticLaurentCoeff_monomial_series_at line 536

Source documentation

With distinct exponents, the analytic coefficient equals the corresponding coefficient of the actual convergent monomial series.

theorem analyticLaurentCoeff_monomial_series_at
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (a : ι → ℂ) (N : ι → ℤ) (hN : Function.Injective N)
    (f : ℂ → ℂ) (B : ι → ℝ) (hB : Summable B)
    (hbound : ∀ i z, z ∈ sphere 0 r → ‖a i * z ^ N i‖ ≤ B i)
    (hsum : ∀ z, z ∈ sphere 0 r → HasSum (fun i => a i * z ^ N i) (f z)) (i₀ : ι) :
    analyticLaurentCoeff r f (N i₀) = a i₀ := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W09.analyticLaurentCoeff_monomial_series_eq_zero line 552

Source documentation

No analytic coefficient outside the actual exponent range can occur.

theorem analyticLaurentCoeff_monomial_series_eq_zero
    {ι : Type*} [Countable ι] {r : ℝ} (hr : 0 < r)
    (a : ι → ℂ) (N : ι → ℤ) (f : ℂ → ℂ) (B : ι → ℝ) (hB : Summable B)
    (hbound : ∀ i z, z ∈ sphere 0 r → ‖a i * z ^ N i‖ ≤ B i)
    (hsum : ∀ z, z ∈ sphere 0 r → HasSum (fun i => a i * z ^ N i) (f z))
    (k : ℤ) (hk : k ∉ Set.range N) : analyticLaurentCoeff r f k = 0 := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff