ThetaSeries.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

Theta series, normal convergence, and derivatives

theorem OAI.Nagata.W22.iteratedDeriv_scalar_exp line 28

Source documentation

The formal frequency factor is the actual iterated complex derivative.

theorem iteratedDeriv_scalar_exp (A B x : ℂ) (c : ℕ) :
    iteratedDeriv c (fun y : ℂ => A * Complex.exp (B * y)) x =
      B ^ c * (A * Complex.exp (B * x)) := by
…

theorem OAI.Nagata.W22.differentiableOn_iteratedDeriv line 43

Source documentation

Iterating holomorphic differentiation stays holomorphic on the open domain.

theorem differentiableOn_iteratedDeriv {f : ℂ → ℂ} {U : Set ℂ}
    (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (c : ℕ) :
    DifferentiableOn ℂ (iteratedDeriv c f) U := by
…

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_iteratedDeriv line 52

Source documentation

All fixed derivatives of holomorphic functions converge locally uniformly whenever the original functions converge locally uniformly.

theorem tendstoLocallyUniformlyOn_iteratedDeriv
    {α : Type*} {l : Filter α} {F : α → ℂ → ℂ} {f : ℂ → ℂ} {U : Set ℂ}
    (h : TendstoLocallyUniformlyOn F f l U)
    (hF : ∀ᶠ a in l, DifferentiableOn ℂ (F a) U) (hU : IsOpen U) (c : ℕ) :
    TendstoLocallyUniformlyOn (fun a => iteratedDeriv c (F a)) (iteratedDeriv c f) l U := by
…

theorem OAI.Nagata.W22.summable_weighted_half line 65
Source documentation
The polynomially weighted geometric majorant in the theta estimate is summable.
```
theorem summable_weighted_half (c : ℕ) :
    Summable (fun t : ℕ => ((t + 1 : ℕ) : ℝ) ^ c * (1 / 2 : ℝ) ^ t) := by
…
```

theorem OAI.Nagata.W22.weighted_term_le line 76

Source documentation

Uniform linear-in-z domination, for any nonnegative weight sequence.

theorem weighted_term_le {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    {z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) (t : ℕ) :
    w t * z ^ (t + 1) ≤ z * (w t * (1 / 2 : ℝ) ^ t) := by
…

theorem OAI.Nagata.W22.summable_weighted_tail line 86

Source documentation

A summable geometric majorant proves summability of every dominated tail.

theorem summable_weighted_tail {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    {z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) :
    Summable (fun t => w t * z ^ (t + 1)) := by
…

theorem OAI.Nagata.W22.weighted_tail_le line 95

Source documentation

The entire tail is bounded by a fixed finite constant times z.

theorem weighted_tail_le {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    {z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) :
    (∑' t, w t * z ^ (t + 1)) ≤
      z * (∑' t, w t * (1 / 2 : ℝ) ^ t) := by
…

theorem OAI.Nagata.W22.tendsto_weighted_tail_zero line 108

Source documentation

The theta-tail comparison tends to zero for any parameter approaching zero within the interval [0,1/2]. No interchange of an unbounded series is assumed.

theorem tendsto_weighted_tail_zero {α : Type*} {l : Filter α} {z : α → ℝ}
    {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    (hz : Tendsto z l (𝓝 0))
    (hzrange : ∀ᶠ a in l, 0 ≤ z a ∧ z a ≤ 1 / 2) :
    Tendsto (fun a => ∑' t, w t * z a ^ (t + 1)) l (𝓝 0) := by
…

theorem OAI.Nagata.W22.tendsto_polynomial_tail_zero line 120

Source documentation

Polynomial weights specialize the preceding estimate to the theta derivative tail.

theorem tendsto_polynomial_tail_zero {α : Type*} {l : Filter α} {z : α → ℝ}
    (c : ℕ) (hz : Tendsto z l (𝓝 0))
    (hzrange : ∀ᶠ a in l, 0 ≤ z a ∧ z a ≤ 1 / 2) :
    Tendsto (fun a => ∑' t : ℕ, ((t + 1 : ℕ) : ℝ) ^ c * z a ^ (t + 1))
      l (𝓝 0) :=
…

theorem OAI.Nagata.W22.affine_weight_le line 129

Source documentation

The actual affine polynomial weight of the derivative estimate is dominated by a constant times (t+1)^c.

theorem affine_weight_le {A n : ℝ} (hA : 0 ≤ A) (hn : 0 ≤ n)
    (c t : ℕ) :
    (A + n * ((t + 1 : ℕ) : ℝ)) ^ c ≤
      (A + n) ^ c * ((t + 1 : ℕ) : ℝ) ^ c := by
…

theorem OAI.Nagata.W22.summable_affine_weighted_half line 139

Source documentation

Summability of the exact derivative majorant displayed in the manuscript.

theorem summable_affine_weighted_half {A n : ℝ} (hA : 0 ≤ A) (hn : 0 ≤ n)
    (c : ℕ) :
    Summable (fun t : ℕ => (A + n * ((t + 1 : ℕ) : ℝ)) ^ c * (1 / 2 : ℝ) ^ t) := by
…

theorem OAI.Nagata.W22.tendsto_affine_weighted_tail_zero line 153

Source documentation

Vanishing of the exact polynomially weighted series used to bound every fixed order derivative of the normalized theta series.

theorem tendsto_affine_weighted_tail_zero {α : Type*} {l : Filter α} {z : α → ℝ}
    {A n : ℝ} (hA : 0 ≤ A) (hn : 0 ≤ n) (c : ℕ)
    (hz : Tendsto z l (𝓝 0))
    (hzrange : ∀ᶠ a in l, 0 ≤ z a ∧ z a ≤ 1 / 2) :
    Tendsto (fun a => ∑' t : ℕ,
      (A + n * ((t + 1 : ℕ) : ℝ)) ^ c * z a ^ (t + 1)) l (𝓝 0) :=
…

theorem OAI.Nagata.W22.summable_of_weighted_bound line 163

Source documentation

A norm bound by a summable weighted geometric sequence gives summability.

theorem summable_of_weighted_bound {E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    {f : ℕ → E} {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    {C z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2)
    (hf : ∀ t, ‖f t‖ ≤ C * (w t * z ^ (t + 1))) : Summable f := by
…

theorem OAI.Nagata.W22.norm_tsum_le_weighted_bound line 171

Source documentation

Uniform scalar majorants also bound the norm of the whole series.

theorem norm_tsum_le_weighted_bound {E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    {f : ℕ → E} {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    {C z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2)
    (hf : ∀ t, ‖f t‖ ≤ C * (w t * z ^ (t + 1))) :
    ‖∑' t, f t‖ ≤ C * (∑' t, w t * z ^ (t + 1)) := by
…

theorem OAI.Nagata.W22.tsum_int_eq_center_add_tails line 186

Source documentation

A bilateral summable sequence is its central term plus its two positive tails.

theorem tsum_int_eq_center_add_tails {E : Type*} [NormedAddCommGroup E]
    {f : ℤ → E}
    (hp : Summable (fun t : ℕ => f (t + 1)))
    (hm : Summable (fun t : ℕ => f (-(t + 1)))) :
    (∑' p : ℤ, f p) = f 0 +
      (∑' t : ℕ, f (t + 1)) + (∑' t : ℕ, f (-(t + 1))) := by
…

theorem OAI.Nagata.W22.tendstoUniformlyOn_tsum_zero_of_weighted_bound line 197

Source documentation

Uniform domination by vanishing weighted tails implies uniform convergence to zero.

theorem tendstoUniformlyOn_tsum_zero_of_weighted_bound
    {α β E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    {l : Filter α} {s : Set β} {f : α → ℕ → β → E} {z : α → ℝ}
    {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    (C : ℝ) (hz : Tendsto z l (𝓝 0))
    (hrange : ∀ᶠ a in l, 0 ≤ z a ∧ z a ≤ 1 / 2)
    (hbound : ∀ᶠ a in l, ∀ t x, x ∈ s →
      ‖f a t x‖ ≤ C * (w t * z a ^ (t + 1))) :
    TendstoUniformlyOn (fun a x => ∑' t, f a t x) (fun _ => 0) l s := by
…

theorem OAI.Nagata.W22.norm_tsum_int_sub_center_le_weighted_bound line 216

theorem OAI.Nagata.W22.tendstoUniformlyOn_tsum_int_center_of_weighted_bound line 239

Source documentation

A bilateral series with a fixed central term and uniformly vanishing positive and negative tails converges uniformly to that central term.

theorem tendstoUniformlyOn_tsum_int_center_of_weighted_bound
    {α β E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    {l : Filter α} {s : Set β} {f : α → ℤ → β → E} {g : β → E} {z : α → ℝ}
    {w : ℕ → ℝ} (hw : ∀ t, 0 ≤ w t)
    (hs : Summable (fun t => w t * (1 / 2 : ℝ) ^ t))
    (C : ℝ) (hz : Tendsto z l (𝓝 0))
    (hrange : ∀ᶠ a in l, 0 ≤ z a ∧ z a ≤ 1 / 2)
    (hcenter : ∀ a x, f a 0 x = g x)
    (hpos : ∀ᶠ a in l, ∀ t : ℕ, ∀ x ∈ s,
      ‖f a (t + 1) x‖ ≤ C * (w t * z a ^ (t + 1)))
    (hneg : ∀ᶠ a in l, ∀ t : ℕ, ∀ x ∈ s,
      ‖f a (-(t + 1)) x‖ ≤ C * (w t * z a ^ (t + 1))) :
…

def OAI.Nagata.W22.thetaDiskMajorant line 270
Source documentation
An explicit summable majorant for all integer indices on a fixed disk.
```
def thetaDiskMajorant (n K R z : ℝ) (c : ℕ) (p : ℤ) : ℝ :=
…
```
theorem OAI.Nagata.W22.summable_thetaDiskMajorant line 272
def OAI.Nagata.W22.normalizedThetaSeries line 296
Source documentation
Exactly the bilateral exponential series of equation eq:normalized-theta.
```
def normalizedThetaSeries (n a K : ℝ) (ε : ℂ) (τ : ℝ) (x : ℂ) : ℂ :=
…
```
def OAI.Nagata.W22.normalizedThetaDerivativeSeries line 301
Source documentation
Sum of the explicit derivative summands. Identification with the derivative of normalizedThetaSeries is recorded separately.
```
def normalizedThetaDerivativeSeries (n a K : ℝ) (ε : ℂ) (τ : ℝ)
    (c : ℕ) (x : ℂ) : ℂ :=
…
```
theorem OAI.Nagata.W22.normalizedThetaDerivativeSeries_zero line 305

theorem OAI.Nagata.W22.theta_geometric_parameter_tendsto_zero line 311

Source documentation

The concrete geometric parameter used in the compact-disk estimate vanishes.

theorem theta_geometric_parameter_tendsto_zero
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a R : ℝ}
    (ha : 0 < a) (han : a < n) (hτ : Tendsto τ l (𝓝 0)) :
    Tendsto (fun j => Real.exp (n * R) * τ j ^ thetaMargin n a) l (𝓝 0) := by
…

theorem OAI.Nagata.W22.tendstoUniformlyOn_normalizedThetaDerivativeSeries line 322

Source documentation

Every fixed formal derivative series converges uniformly on every disk to the corresponding exponential derivative. Bounds and summability are discharged.

theorem tendstoUniformlyOn_normalizedThetaDerivativeSeries
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K R : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1) (hR : 0 ≤ R)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (c : ℕ) :
    TendstoUniformlyOn (fun j => normalizedThetaDerivativeSeries n a K ε (τ j) c)
      (fun x => (K : ℂ) ^ c * Complex.exp ((K : ℂ) * x)) l
      {x : ℂ | ‖x‖ ≤ R} := by
…

Mentions: OAI.Nagata.W22.normalizedThetaDerivativeSeries

theorem OAI.Nagata.W22.tendstoUniformlyOn_normalizedThetaSeries line 355

Source documentation

The normalized theta series itself degenerates uniformly on compact disks.

theorem tendstoUniformlyOn_normalizedThetaSeries
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K R : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1) (hR : 0 ≤ R)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    TendstoUniformlyOn (fun j => normalizedThetaSeries n a K ε (τ j))
      (fun x => Complex.exp ((K : ℂ) * x)) l {x : ℂ | ‖x‖ ≤ R} := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_normalizedThetaSeries line 367

Source documentation

Compact-uniform degeneration on the entire complex logarithmic coordinate plane.

theorem tendstoLocallyUniformlyOn_normalizedThetaSeries
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    TendstoLocallyUniformlyOn (fun j => normalizedThetaSeries n a K ε (τ j))
      (fun x => Complex.exp ((K : ℂ) * x)) l Set.univ := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.W22.hasDerivAt_normalizedThetaDerivativeTerm line 387

Source documentation

The candidate frequency factor is exactly the actual complex derivative.

theorem hasDerivAt_normalizedThetaDerivativeTerm
    (n a K : ℝ) (ε : ℂ) (τ : ℝ) (c : ℕ) (p : ℤ) (x : ℂ) :
    HasDerivAt (normalizedThetaDerivativeTerm n a K ε τ c p)
      (normalizedThetaDerivativeTerm n a K ε τ (c + 1) p x) x := by
…

theorem OAI.Nagata.W22.iteratedDeriv_normalizedThetaTerm line 400

Source documentation

Every frequency factor is the genuine iterated derivative of the summand.

theorem iteratedDeriv_normalizedThetaTerm
    (n a K : ℝ) (ε : ℂ) (τ : ℝ) (c : ℕ) (p : ℤ) (x : ℂ) :
    iteratedDeriv c (normalizedThetaTerm n a K ε τ p) x =
      normalizedThetaDerivativeTerm n a K ε τ c p x := by
…

theorem OAI.Nagata.W22.deriv_normalizedThetaDerivativeSeries line 421

Source documentation

Termwise differentiation is legitimate on a disk where the geometric bound is at most one half. No differentiation rule is assumed for the series.

theorem deriv_normalizedThetaDerivativeSeries
    {n a K τ R : ℝ} {ε x : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hzhalf : Real.exp (n * R) * τ ^ thetaMargin n a ≤ 1 / 2)
    (hx : ‖x‖ < R) (c : ℕ) :
    deriv (normalizedThetaDerivativeSeries n a K ε τ c) x =
      normalizedThetaDerivativeSeries n a K ε τ (c + 1) x := by
…

Mentions: OAI.Nagata.W22.normalizedThetaDerivativeSeries

theorem OAI.Nagata.W22.iteratedDeriv_normalizedThetaSeries line 446

Source documentation

The entire derivative series is the iterated derivative of the genuine theta series throughout the interior of the same disk.

theorem iteratedDeriv_normalizedThetaSeries
    {n a K τ R : ℝ} {ε x : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hzhalf : Real.exp (n * R) * τ ^ thetaMargin n a ≤ 1 / 2)
    (hx : ‖x‖ < R) (c : ℕ) :
    iteratedDeriv c (normalizedThetaSeries n a K ε τ) x =
      normalizedThetaDerivativeSeries n a K ε τ c x := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries, OAI.Nagata.W22.normalizedThetaDerivativeSeries

theorem OAI.Nagata.W22.tendstoUniformlyOn_iteratedDeriv_normalizedThetaSeries line 467

Source documentation

All actual complex derivatives of the normalized theta series converge uniformly on every fixed compact disk. The auxiliary disk bound is discharged by choosing the larger radius R+1 and taking τ sufficiently small.

theorem tendstoUniformlyOn_iteratedDeriv_normalizedThetaSeries
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K R : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1) (hR : 0 ≤ R)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (c : ℕ) :
    TendstoUniformlyOn (fun j => iteratedDeriv c (normalizedThetaSeries n a K ε (τ j)))
      (fun x => (K : ℂ) ^ c * Complex.exp ((K : ℂ) * x)) l
      {x : ℂ | ‖x‖ ≤ R} := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.W22.tendsto_iteratedDeriv_normalizedThetaSeries_zero line 485

Source documentation

The precise limiting x-jet entry needed in the finite matrix.

theorem tendsto_iteratedDeriv_normalizedThetaSeries_zero
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (c : ℕ) :
    Tendsto (fun j => iteratedDeriv c (normalizedThetaSeries n a K ε (τ j)) 0)
      l (𝓝 ((K : ℂ) ^ c)) := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.W22.summable_normalizedThetaTerm_norm_on_disk line 505

Source documentation

Pointwise absolute summability with the same concrete disk majorant.

theorem summable_normalizedThetaTerm_norm_on_disk
    {n a K τ R : ℝ} {ε x : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hzhalf : Real.exp (n * R) * τ ^ thetaMargin n a ≤ 1 / 2)
    (hx : ‖x‖ ≤ R) :
    Summable (fun p : ℤ => ‖normalizedThetaTerm n a K ε τ p x‖) := by
…

theorem OAI.Nagata.W22.hasSum_normalizedThetaTerm_on_disk line 518

Source documentation

The actual bilateral series has the stated sum at every point of the disk.

theorem hasSum_normalizedThetaTerm_on_disk
    {n a K τ R : ℝ} {ε x : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hzhalf : Real.exp (n * R) * τ ^ thetaMargin n a ≤ 1 / 2)
    (hx : ‖x‖ ≤ R) :
    HasSum (fun p : ℤ => normalizedThetaTerm n a K ε τ p x)
      (normalizedThetaSeries n a K ε τ x) :=
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.W22.tendstoUniformlyOn_normalizedThetaSeries_partialSums line 528

Source documentation

Uniform finite-sum convergence of the literal two-sided series on a disk.

theorem tendstoUniformlyOn_normalizedThetaSeries_partialSums
    {n a K τ R : ℝ} {ε : ℂ}
    (hn : 0 ≤ n) (hτ : 0 < τ) (hτone : τ ≤ 1) (hε : ‖ε‖ = 1)
    (hR : 0 ≤ R) (hzhalf : Real.exp (n * R) * τ ^ thetaMargin n a ≤ 1 / 2) :
    TendstoUniformlyOn
      (fun S : Finset ℤ => fun x => ∑ p ∈ S, normalizedThetaTerm n a K ε τ p x)
      (normalizedThetaSeries n a K ε τ) atTop {x : ℂ | ‖x‖ ≤ R} := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.W22.eventually_normalizedThetaSeries_partialSums line 543

Source documentation

On any fixed disk the literal finite-sum convergence applies for all sufficiently small positive values of the degeneration parameter.

theorem eventually_normalizedThetaSeries_partialSums
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K R : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1) (hR : 0 ≤ R)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    ∀ᶠ j in l, TendstoUniformlyOn
      (fun S : Finset ℤ => fun x => ∑ p ∈ S, normalizedThetaTerm n a K ε (τ j) p x)
      (normalizedThetaSeries n a K ε (τ j)) atTop {x : ℂ | ‖x‖ ≤ R} := by
…

Mentions: OAI.Nagata.W22.normalizedThetaSeries