CollisionBounds.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Coefficient convergence, collision estimates, and compactness

theorem OAI.Nagata.W20.uniform_linear_combination_of_bounds line 38

Source documentation

Finite coefficient convergence is uniform wherever all basis functions have fixed uniform bounds.

theorem uniform_linear_combination_of_bounds {ι X : Type*} [Fintype ι]
    (K : Set X) (b : ι → X → R) (B : ι → ℝ)
    (hB : ∀ i z, z ∈ K → ‖b i z‖ ≤ B i)
    (c : ℕ → ι → R) (c₀ : ι → R)
    (hc : ∀ i, Tendsto (fun n => c n i) atTop (𝓝 (c₀ i))) :
    TendstoUniformlyOn (fun n z => ∑ i, c n i * b i z)
      (fun z => ∑ i, c₀ i * b i z) atTop K := by
…

theorem OAI.Nagata.W20.uniform_linear_combination_on_compact line 72

Source documentation

On a compact set, continuity of the finitely many fixed basis functions supplies the required bounds.

theorem uniform_linear_combination_on_compact {ι X : Type*} [Fintype ι]
    [TopologicalSpace X] (K : Set X) (hK : IsCompact K)
    (b : ι → X → R) (hb : ∀ i, ContinuousOn (b i) K)
    (c : ℕ → ι → R) (c₀ : ι → R)
    (hc : ∀ i, Tendsto (fun n => c n i) atTop (𝓝 (c₀ i))) :
    TendstoUniformlyOn (fun n z => ∑ i, c n i * b i z)
      (fun z => ∑ i, c₀ i * b i z) atTop K := by
…

theorem OAI.Nagata.W20.locally_uniform_linear_combination line 89

Source documentation

For a finite holomorphic (or merely continuous) local basis on an open complex domain, coefficient convergence gives locally uniform convergence.

theorem locally_uniform_linear_combination {ι X : Type*} [Fintype ι]
    [TopologicalSpace X] [LocallyCompactSpace X]
    {U : Set X} (hU : IsOpen U) (b : ι → X → R)
    (hb : ∀ i, ContinuousOn (b i) U)
    (c : ℕ → ι → R) (c₀ : ι → R)
    (hc : ∀ i, Tendsto (fun n => c n i) atTop (𝓝 (c₀ i))) :
    TendstoLocallyUniformlyOn (fun n z => ∑ i, c n i * b i z)
      (fun z => ∑ i, c₀ i * b i z) atTop U := by
…

theorem OAI.Nagata.W20.unit_subsequence line 114

Source documentation

Unit coefficient vectors have a subsequence with a nonzero unit limit. The ProperSpace instance is supplied by finite dimensionality over ℝ or ℂ.

theorem unit_subsequence {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
    (v : ℕ → E) (hv : ∀ n, ‖v n‖ = 1) :
    ∃ a : E, ‖a‖ = 1 ∧ a ≠ 0 ∧
      ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (v ∘ φ) atTop (𝓝 a) := by
…

theorem OAI.Nagata.W20.continuous_zero_at_limit line 129

Source documentation

A fixed continuous map which vanishes on a convergent sequence vanishes at the limit. This applies to each fixed finite-dimensional jet functional.

theorem continuous_zero_at_limit {E F : Type*}
    [TopologicalSpace E] [TopologicalSpace F] [T2Space F] [Zero F]
    (f : E → F) (hf : Continuous f) (v : ℕ → E) (a : E)
    (hv : Tendsto v atTop (𝓝 a)) (hzero : ∀ n, f (v n) = 0) : f a = 0 := by
…

theorem OAI.Nagata.W20.nonzero_kernel_limit line 140

Source documentation

Compactness and continuity preserve a nontrivial kernel witness. The map is fixed: varying jet centers require the separate analytic collision bridge.

theorem nonzero_kernel_limit {E F : Type*} [NormedAddCommGroup E] [ProperSpace E]
    [TopologicalSpace F] [T2Space F] [Zero F]
    (f : E → F) (hf : Continuous f)
    (v : ℕ → E) (hv : ∀ n, ‖v n‖ = 1) (hz : ∀ n, f (v n) = 0) :
    ∃ a : E, ‖a‖ = 1 ∧ a ≠ 0 ∧ f a = 0 := by
…

theorem OAI.Nagata.W20.boundary_distance_lower line 161
Source documentation
A point in the half disk stays at least half a radius from its boundary.
```
theorem boundary_distance_lower {z ξ : 𝕜} {r : ℝ}
    (hz : ‖z‖ = r) (hξ : ‖ξ‖ ≤ r / 2) : r / 2 ≤ ‖z - ξ‖ := by
…
```

theorem OAI.Nagata.W20.collision_product_boundary_lower line 167

Source documentation

Uniform lower bound on the collision divisor along the boundary circle.

theorem collision_product_boundary_lower {ι : Type*} [Fintype ι]
    (ξ : ι → 𝕜) (k : ℕ) {r : ℝ} (hr : 0 < r)
    (hξ : ∀ i, ‖ξ i‖ ≤ r / 2) {z : 𝕜} (hz : ‖z‖ = r) :
    (r / 2) ^ (k * Fintype.card ι) ≤ ‖∏ i, (z - ξ i) ^ k‖ := by
…

theorem OAI.Nagata.W20.collision_product_tendsto line 184

Source documentation

The explicit collision factors converge to the expected power, with exponent equal to the sum of the multiplicities of all factors.

theorem collision_product_tendsto {ι : Type*} [Fintype ι]
    (ξ : ℕ → ι → 𝕜) (k : ℕ) (hξ : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
    (z : 𝕜) :
    Tendsto (fun n => ∏ i, (z - ξ n i) ^ k) atTop
      (𝓝 (z ^ (k * Fintype.card ι))) := by
…

theorem OAI.Nagata.W20.collision_limit_growth line 197

Source documentation

Bounded holomorphic quotients are enough for the quantitative collision estimate; convergence of the quotients themselves is unnecessary. This lemma is pointwise and its quotient bound is supplied by the maximum modulus lemma.

theorem collision_limit_growth {ι : Type*} [Fintype ι]
    (ξ : ℕ → ι → 𝕜) (k : ℕ) (hξ : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
    (H G : ℕ → 𝕜 → 𝕜) (f : 𝕜 → 𝕜) (z : 𝕜) (C : ℝ)
    (hlim : Tendsto (fun n => H n z) atTop (𝓝 (f z)))
    (hfactor : ∀ n, H n z = (∏ i, (z - ξ n i) ^ k) * G n z)
    (hbound : ∀ n, ‖G n z‖ ≤ C) :
    ‖f z‖ ≤ ‖z‖ ^ (k * Fintype.card ι) * C := by
…

theorem OAI.Nagata.W20.collision_limit_growth_eventually line 213

Source documentation

Version of the collision growth estimate allowing a finite initial segment to be discarded, as required by locally uniform convergence.

theorem collision_limit_growth_eventually {ι : Type*} [Fintype ι]
    (ξ : ℕ → ι → 𝕜) (k : ℕ) (hξ : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
    (H G : ℕ → 𝕜 → 𝕜) (f : 𝕜 → 𝕜) (z : 𝕜) (C : ℝ)
    (hlim : Tendsto (fun n => H n z) atTop (𝓝 (f z)))
    (hfactor : ∀ n, H n z = (∏ i, (z - ξ n i) ^ k) * G n z)
    (hbound : ∀ᶠ n in atTop, ‖G n z‖ ≤ C) :
    ‖f z‖ ≤ ‖z‖ ^ (k * Fintype.card ι) * C := by
…

def OAI.Nagata.W20.collisionCenters line 241
Source documentation
Distinct real points in the complex disk, scaled to zero.
```
noncomputable def collisionCenters (q : ℕ) (r : ℝ) (n : ℕ) (i : Fin q) : ℂ :=
…
```
theorem OAI.Nagata.W20.collisionCenters_injective line 244
theorem OAI.Nagata.W20.collisionCenters_mem_ball line 255
theorem OAI.Nagata.W20.collisionCenters_tendsto line 267

theorem OAI.Nagata.W20.exists_collision_centers line 278

Source documentation

Every open neighborhood of zero admits one sequence of injective q-tuples, all lying in the neighborhood, with every point converging to zero.

theorem exists_collision_centers {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
    (q : ℕ) : ∃ ξ : ℕ → Fin q → ℂ,
      (∀ n, Function.Injective (ξ n)) ∧ (∀ n i, ξ n i ∈ U) ∧
      (∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0)) := by
…

theorem OAI.Nagata.W20.analyticOrderAt_lower_of_growth line 303

Source documentation

A holomorphic function bounded by C |z|^N has vanishing order at least N. The proof uses the actual removable-singularity theorem, not an order axiom.

theorem analyticOrderAt_lower_of_growth (f : ℂ → ℂ) (N : ℕ) {r C : ℝ}
    (hr : 0 < r) (hf : DifferentiableOn ℂ f (ball 0 r))
    (hbound : ∀ z ∈ ball (0 : ℂ) r, ‖f z‖ ≤ ‖z‖ ^ N * C) :
    (N : ℕ∞) ≤ analyticOrderAt f 0 := by
…

theorem OAI.Nagata.W20.iteratedDeriv_zero_of_growth line 341

Source documentation

The same growth estimate expressed in the derivative form used by the collision jet matrix.

theorem iteratedDeriv_zero_of_growth (f : ℂ → ℂ) (N : ℕ) {r C : ℝ}
    (hr : 0 < r) (hf : DifferentiableOn ℂ f (ball 0 r))
    (hbound : ∀ z ∈ ball (0 : ℂ) r, ‖f z‖ ≤ ‖z‖ ^ N * C) :
    ∀ ℓ < N, iteratedDeriv ℓ f 0 = 0 :=
…

theorem OAI.Nagata.W20.eventual_uniform_bound_on_compact line 364

Source documentation

Uniform convergence on a compact set gives one bound for all sufficiently late functions, by bounding the limit and taking uniform error at most one.

theorem eventual_uniform_bound_on_compact {X : Type*} [TopologicalSpace X]
    (K : Set X) (hK : IsCompact K) (H : ℕ → X → E) (f : X → E)
    (hf : ContinuousOn f K) (hlim : TendstoUniformlyOn H f atTop K) :
    ∃ M : ℝ, ∀ᶠ n in atTop, ∀ z ∈ K, ‖H n z‖ ≤ M := by
…

theorem OAI.Nagata.W20.centers_eventually_half_disk line 378

Source documentation

Finitely many centers converging to zero eventually all belong to the same half disk. No uniformity in an infinite index set is presumed.

theorem centers_eventually_half_disk {ι : Type*} [Finite ι]
    (ξ : ℕ → ι → E) (hξ : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
    {r : ℝ} (hr : 0 < r) :
    ∀ᶠ n in atTop, ∀ i, ‖ξ n i‖ ≤ r / 2 := by
…

theorem OAI.Nagata.W20.quotient_bound_on_closedBall line 400

Source documentation

Maximum-modulus quotient estimate. If f=P*g on the boundary, P is bounded away from zero there, and the actual quotient g is holomorphic inside, then g is uniformly bounded on the whole closed disk.

theorem quotient_bound_on_closedBall (f P g : ℂ → ℂ) {r a M : ℝ}
    (hr : 0 < r) (ha : 0 < a)
    (hg : DiffContOnCl ℂ g (ball 0 r))
    (hfactor : ∀ z ∈ sphere (0 : ℂ) r, f z = P z * g z)
    (hlower : ∀ z ∈ sphere (0 : ℂ) r, a ≤ ‖P z‖)
    (hupper : ∀ z ∈ sphere (0 : ℂ) r, ‖f z‖ ≤ M)
    {z : ℂ} (hz : z ∈ closedBall (0 : ℂ) r) : ‖g z‖ ≤ M / a := by
…