ThetaLimits.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Marked theta products and scalar-basis degeneration

def OAI.Nagata.W22.scaledThetaPositive line 20
Source documentation
One half of the theta product, after substituting a shrinking center.
```
def scaledThetaPositive (a : ℝ) (δ : ℂ) (τ : ℝ) (x : ℂ) : ℂ :=
…
```

theorem OAI.Nagata.W22.scaledThetaPositive_factor_norm_le line 24

Source documentation

The nonconstant product factors have one summable geometric majorant on a disk.

theorem scaledThetaPositive_factor_norm_le {a τ R : ℝ} {δ x : ℂ}
    (hτ : 0 ≤ τ) (hτhalf : τ ≤ 1 / 2) (hδ : ‖δ‖ ≤ 1)
    (hR : 0 ≤ R) (hx : ‖x‖ ≤ R) (t : ℕ) :
    ‖-((τ : ℂ) ^ t * (((τ ^ a : ℝ) : ℂ) * Complex.exp (δ * x)))‖ ≤
      (1 / 2 : ℝ) ^ t * (τ ^ a * Real.exp R) := by
…

theorem OAI.Nagata.W22.tendstoUniformlyOn_scaledThetaPositive line 42

Source documentation

Each half-product tends uniformly to one on a fixed disk when a>0.

theorem tendstoUniformlyOn_scaledThetaPositive
    {α : Type*} {l : Filter α} {τ : α → ℝ} {a R : ℝ} {δ : ℂ}
    (ha : 0 < a) (hδ : ‖δ‖ ≤ 1) (hR : 0 ≤ R)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    TendstoUniformlyOn (fun j => scaledThetaPositive a δ (τ j)) (fun _ => 1)
      l {x : ℂ | ‖x‖ ≤ R} := by
…

Mentions: OAI.Nagata.W22.scaledThetaPositive

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_scaledThetaPositive line 77

Source documentation

Local-uniform version of the same actual half-product degeneration.

theorem tendstoLocallyUniformlyOn_scaledThetaPositive
    {α : Type*} {l : Filter α} {τ : α → ℝ} {a : ℝ} {δ : ℂ}
    (ha : 0 < a) (hδ : ‖δ‖ ≤ 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    TendstoLocallyUniformlyOn (fun j => scaledThetaPositive a δ (τ j))
      (fun _ => 1) l Set.univ := by
…

Mentions: OAI.Nagata.W22.scaledThetaPositive

def OAI.Nagata.W22.shiftedThetaProduct line 91
Source documentation
The actual theta product evaluated at the shrinking center.
```
def shiftedThetaProduct (a : ℝ) (τ : ℝ) (x : ℂ) : ℂ :=
…
```
theorem OAI.Nagata.W22.shiftedThetaProduct_eq_halves line 95
Source documentation
The two source halves after the common-chart substitution.
```
theorem shiftedThetaProduct_eq_halves {τ : ℝ} (hτ : 0 < τ) (a : ℝ) (x : ℂ) :
    shiftedThetaProduct a τ x = scaledThetaPositive a 1 τ x *
      scaledThetaPositive (1 - a) (-1) τ x := by
…
```
Mentions: OAI.Nagata.W22.shiftedThetaProduct, OAI.Nagata.W22.scaledThetaPositive

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_shiftedThetaProduct line 105

Source documentation

The complete theta factor tends locally uniformly to one if 0<a<1.

theorem tendstoLocallyUniformlyOn_shiftedThetaProduct
    {α : Type*} {l : Filter α} {τ : α → ℝ} {a : ℝ}
    (ha : 0 < a) (haone : a < 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    TendstoLocallyUniformlyOn (fun j => shiftedThetaProduct a (τ j))
      (fun _ => 1) l Set.univ := by
…

Mentions: OAI.Nagata.W22.shiftedThetaProduct

def OAI.Nagata.W22.markedPi line 136
Source documentation
The product Π in the local covering frame, with offsets aᵢ=x₀−xᵢ.
```
def markedPi (a : Fin 9 → ℝ) (τ : ℝ) (x : ℂ) : ℂ :=
…
```
theorem OAI.Nagata.W22.shiftedThetaProduct_differentiable line 140
Source documentation
Every shifted theta factor is entire in the logarithmic coordinate.
```
theorem shiftedThetaProduct_differentiable {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1) (a : ℝ) :
    Differentiable ℂ (shiftedThetaProduct a τ) := by
…
```
Mentions: OAI.Nagata.W22.shiftedThetaProduct
theorem OAI.Nagata.W22.markedPi_differentiable line 151
Source documentation
The nine-factor product is entire in the logarithmic coordinate.
```
theorem markedPi_differentiable {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (a : Fin 9 → ℝ) : Differentiable ℂ (markedPi a τ) := by
…
```
Mentions: OAI.Nagata.W22.markedPi

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_markedPi line 156

Source documentation

The full product tends locally uniformly to one, with all nine marks present.

theorem tendstoLocallyUniformlyOn_markedPi
    {α : Type*} {l : Filter α} {τ : α → ℝ} {a : Fin 9 → ℝ}
    (ha : ∀ i, 0 < a i) (haone : ∀ i, a i < 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) :
    TendstoLocallyUniformlyOn (fun j => markedPi a (τ j)) (fun _ => 1) l Set.univ := by
…

Mentions: OAI.Nagata.W22.markedPi

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_markedPi_pow line 165

Source documentation

Every fixed nonnegative power of Π tends locally uniformly to one.

theorem tendstoLocallyUniformlyOn_markedPi_pow
    {α : Type*} {l : Filter α} {τ : α → ℝ} {a : Fin 9 → ℝ}
    (ha : ∀ i, 0 < a i) (haone : ∀ i, a i < 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (e : ℕ) :
    TendstoLocallyUniformlyOn (fun j x => markedPi a (τ j) x ^ e) (fun _ => 1) l Set.univ := by
…

Mentions: OAI.Nagata.W22.markedPi

theorem OAI.Nagata.W22.tendsto_iteratedDeriv_markedPi_pow_zero line 175

Source documentation

The degree-zero tip is retained: the coefficient Π^e has jets tending to those of the constant function one, including its zeroth jet.

theorem tendsto_iteratedDeriv_markedPi_pow_zero
    {α : Type*} {l : Filter α} {τ : α → ℝ} {marks : Fin 9 → ℝ}
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (e c : ℕ) :
    Tendsto (fun j => iteratedDeriv c (fun x => markedPi marks (τ j) x ^ e) 0)
      l (𝓝 ((0 : ℂ) ^ c)) := by
…

Mentions: OAI.Nagata.W22.markedPi

def OAI.Nagata.W22.rayMarkedSection line 203
Source documentation
The actual nine-mark multiplier section for ray lifts τ^ξᵢ.
```
def rayMarkedSection {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (ξ : Fin 9 → ℝ) :=
…
```
theorem OAI.Nagata.W22.rayMarkedSection_centered line 213
Source documentation
Evaluating the genuine section on the moving exponential chart gives exactly the scalar nine-factor product used in the jet limit.
```
theorem rayMarkedSection_centered {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (ξ : Fin 9 → ℝ) (x₀ : ℝ) (x : ℂ) :
    (rayMarkedSection hτ hτone ξ).val (((τ ^ x₀ : ℝ) : ℂ) * Complex.exp x) =
      markedPi (fun i => x₀ - ξ i) τ x := by
…
```
Mentions: OAI.Nagata.W22.rayMarkedSection, OAI.Nagata.W22.markedPi

def OAI.Nagata.W22.multipliedThetaCoefficient line 241

Source documentation

The exact second-branch scalar coefficient.

def multipliedThetaCoefficient (marks : Fin 9 → ℝ) (n a K : ℝ) (ε : ℂ)
    (e : ℕ) (τ : ℝ) (x : ℂ) : ℂ :=
…

theorem OAI.Nagata.W22.tendstoLocallyUniformlyOn_multipliedThetaCoefficient line 246

Source documentation

The complete positive-degree coefficient block has the required local limit.

theorem tendstoLocallyUniformlyOn_multipliedThetaCoefficient
    {α : Type*} {l : Filter α} {τ : α → ℝ} {marks : Fin 9 → ℝ}
    {n a K : ℝ} {ε : ℂ}
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1)
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (e : ℕ) :
    TendstoLocallyUniformlyOn (fun j => multipliedThetaCoefficient marks n a K ε e (τ j))
      (fun x => Complex.exp ((K : ℂ) * x)) l Set.univ := by
…

Mentions: OAI.Nagata.W22.multipliedThetaCoefficient

theorem OAI.Nagata.W22.tendsto_iteratedDeriv_multipliedThetaCoefficient_zero line 261

Source documentation

Derivative limits for the complete positive-degree second block at the jet origin.

theorem tendsto_iteratedDeriv_multipliedThetaCoefficient_zero
    {α : Type*} {l : Filter α} {τ : α → ℝ} {marks : Fin 9 → ℝ}
    {n a K : ℝ} {ε : ℂ}
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1)
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j) (e c : ℕ) :
    Tendsto (fun j => iteratedDeriv c (multipliedThetaCoefficient marks n a K ε e (τ j)) 0)
      l (𝓝 ((K : ℂ) ^ c)) := by
…

Mentions: OAI.Nagata.W22.multipliedThetaCoefficient

def OAI.Nagata.W22.basisCoefficient line 297
Source documentation
Actual scalar expression of every basis column, retaining the degree-zero tip.
```
def basisCoefficient (d m : ℤ) (ρ Δ : ℝ) (marks : Fin 9 → ℝ)
    (τ : ℝ) (col : Column d m ρ Δ) : ℂ → ℂ :=
…
```

theorem OAI.Nagata.W22.eventually_differentiableOn_basisCoefficient_disk line 312

Source documentation

All columns are eventually holomorphic on one fixed disk. This assertion uses the actual normal convergence and keeps all three source branches.

theorem eventually_differentiableOn_basisCoefficient_disk
    {α : Type*} {l : Filter α} {τ : α → ℝ} {d m : ℤ} {ρ Δ : ℝ}
    (marks : Fin 9 → ℝ) (hτ : Tendsto τ l (𝓝 0))
    (hτpos : ∀ᶠ t in l, 0 < τ t) :
    ∀ᶠ t in l, ∀ col : Column d m ρ Δ,
      DifferentiableOn ℂ (basisCoefficient d m ρ Δ marks (τ t) col)
        {x : ℂ | ‖x‖ < 1} := by
…

Mentions: OAI.Nagata.W22.basisCoefficient

theorem OAI.Nagata.W22.eventually_contDiffAt_basisCoefficient line 342

Source documentation

Eventual smoothness of every literal column, for the finite-jet linearity bridge.

theorem eventually_contDiffAt_basisCoefficient
    {α : Type*} {l : Filter α} {τ : α → ℝ} {d m : ℤ} {ρ Δ : ℝ}
    (marks : Fin 9 → ℝ) (hτ : Tendsto τ l (𝓝 0))
    (hτpos : ∀ᶠ j in l, 0 < τ j) :
    ∀ᶠ j in l, ∀ col : Column d m ρ Δ, ∀ c : ℕ,
      ContDiffAt ℂ c (basisCoefficient d m ρ Δ marks (τ j) col) 0 := by
…

Mentions: OAI.Nagata.W22.basisCoefficient

theorem OAI.Nagata.W22.tendsto_iteratedDeriv_basisCoefficient_zero line 354

Source documentation

Every genuine scalar coefficient has the expected limiting x-jets.

theorem tendsto_iteratedDeriv_basisCoefficient_zero
    {α : Type*} {l : Filter α} {τ : α → ℝ} {d m : ℤ} {ρ Δ : ℝ}
    {marks : Fin 9 → ℝ}
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ j in l, 0 < τ j)
    (col : Column d m ρ Δ) (c : ℕ) :
    Tendsto (fun t => iteratedDeriv c (basisCoefficient d m ρ Δ marks (τ t) col) 0)
      l (𝓝 ((col.val.2 : ℂ) ^ c)) := by
…

Mentions: OAI.Nagata.W22.basisCoefficient