JetGerms.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Local holomorphic jets and finite jet noncancellation

theorem OAI.Nagata.Workers.W11.eventually_differentiableOn_normalizedThetaSeries_disk line 25

Source documentation

For sufficiently small positive parameters the literal normalized theta series is holomorphic on the fixed unit disk. The proof takes the locally uniform limit of its actual finite sums of entire exponential functions.

theorem eventually_differentiableOn_normalizedThetaSeries_disk
    {α : Type*} {l : Filter α} {τ : α → ℝ} {n a K : ℝ} {ε : ℂ}
    (ha : 0 < a) (han : a < n) (hε : ‖ε‖ = 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ t in l, 0 < τ t) :
    ∀ᶠ t in l, DifferentiableOn ℂ (normalizedThetaSeries n a K ε (τ t))
      {x : ℂ | ‖x‖ < 1} := by
…

def OAI.Nagata.Workers.W11.mixedJetAtZero line 70
Source documentation
First take b derivatives in y, then ell derivatives in x, at the origin, exactly as in the source's jet rows.
```
def mixedJetAtZero (F : ℂ → ℂ → ℂ) (ell b : ℕ) : ℂ :=
…
```
theorem OAI.Nagata.Workers.W11.mixedJetAtZero_separated line 75
Source documentation
The separated-variable formula, including zero derivative orders and zero frequencies, holds for actual derivatives.
```
theorem mixedJetAtZero_separated (f : ℂ → ℂ) (j : ℂ) (ell b : ℕ) :
    mixedJetAtZero (fun x y => f x * Complex.exp (j * y)) ell b =
      iteratedDeriv ell f 0 * j ^ b := by
…
```
Mentions: OAI.Nagata.Workers.W11.mixedJetAtZero

def OAI.Nagata.Workers.W11.separatedJetMatrix line 87

Source documentation

Genuine mixed-derivative matrix on the source's fixed row and column types.

def separatedJetMatrix (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (coeff : Column d (m : ℤ) a delta → ℂ → ℂ) :
    Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ :=
…

theorem OAI.Nagata.Workers.W11.tendsto_separatedJetMatrix_entries line 96

Source documentation

Coefficient derivative convergence implies entrywise convergence of the actual mixed-derivative matrix to B0.

theorem tendsto_separatedJetMatrix_entries
    {α : Type*} {l : Filter α} (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (coeff : α → Column d (m : ℤ) a delta → ℂ → ℂ)
    (hcoeff : ∀ col ell, Tendsto (fun t => iteratedDeriv ell (coeff t col) 0) l
      (𝓝 ((col.val.2 : ℂ) ^ ell))) :
    ∀ row col, Tendsto (fun t => separatedJetMatrix d q m a delta (coeff t) row col)
      l (𝓝 (B0 d q m a delta row col)) := by
…

Mentions: OAI.Nagata.Workers.W11.separatedJetMatrix

theorem OAI.Nagata.Workers.W11.mixedJetAtZero_congr_of_eventuallyEq line 123
Source documentation
Equality on a genuine neighborhood in ℂ² implies equality of every mixed iterated derivative at the origin. No global identity is required.
```
theorem mixedJetAtZero_congr_of_eventuallyEq
    {F G : ℂ → ℂ → ℂ} (ell b : ℕ)
    (h : ∀ᶠ z : ℂ × ℂ in 𝓝 (0, 0), F z.1 z.2 = G z.1 z.2) :
    mixedJetAtZero F ell b = mixedJetAtZero G ell b := by
…
```
Mentions: OAI.Nagata.Workers.W11.mixedJetAtZero
theorem OAI.Nagata.Workers.W11.mixedJetAtZero_eq_zero_of_locally_zero line 136
Source documentation
A scalar expression vanishing on a chart neighborhood has all its prescribed mixed jets zero. This is valid for each finite jet order independently.
```
theorem mixedJetAtZero_eq_zero_of_locally_zero
    {F : ℂ → ℂ → ℂ} (ell b : ℕ)
    (h : ∀ᶠ z : ℂ × ℂ in 𝓝 (0, 0), F z.1 z.2 = 0) :
    mixedJetAtZero F ell b = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W11.mixedJetAtZero

theorem OAI.Nagata.Workers.W11.mixedJetAtZero_separated_sum line 165

Source documentation

Actual mixed derivatives commute with the finite scalar expansion when the coefficient functions have the required derivatives.

theorem mixedJetAtZero_separated_sum {ι : Type*} [Fintype ι]
    (f : ι → ℂ → ℂ) (j c : ι → ℂ) (ell b : ℕ)
    (hf : ∀ i, ContDiffAt ℂ ell (f i) 0) :
    mixedJetAtZero (fun x y => ∑ i, c i * f i x * Complex.exp (j i * y)) ell b =
      ∑ i, c i * (iteratedDeriv ell (f i) 0 * j i ^ b) := by
…

Mentions: OAI.Nagata.Workers.W11.mixedJetAtZero

theorem OAI.Nagata.Workers.W11.separatedJetMatrix_mulVec_eq_mixedJet line 191

Source documentation

Multiplying the actual mixed-derivative matrix by coefficients is exactly the mixed jet of their finite scalar combination.

theorem separatedJetMatrix_mulVec_eq_mixedJet
    (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (coeff : Column d (m : ℤ) a delta → ℂ → ℂ)
    (v : Column d (m : ℤ) a delta → ℂ) (row : JetIndex q m)
    (hcoeff : ∀ col, ContDiffAt ℂ row.2.val (coeff col) 0) :
    (separatedJetMatrix d q m a delta coeff).mulVec v row =
      mixedJetAtZero (fun x y => ∑ col, v col * coeff col x *
        Complex.exp ((col.val.1 : ℂ) * y)) row.2.val row.1.val := by
…

Mentions: OAI.Nagata.Workers.W11.separatedJetMatrix, OAI.Nagata.Workers.W11.mixedJetAtZero

theorem OAI.Nagata.Workers.W11.separatedJetMatrix_kernel_iff_mixedJets line 207

Source documentation

Consequently the entire source-shaped finite jet system vanishes exactly when the actual scalar combination has all its prescribed mixed jets zero.

theorem separatedJetMatrix_kernel_iff_mixedJets
    (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (coeff : Column d (m : ℤ) a delta → ℂ → ℂ)
    (v : Column d (m : ℤ) a delta → ℂ)
    (hcoeff : ∀ row : JetIndex q m, ∀ col, ContDiffAt ℂ row.2.val (coeff col) 0) :
    (separatedJetMatrix d q m a delta coeff).mulVec v = 0 ↔
      ∀ row : JetIndex q m, mixedJetAtZero (fun x y => ∑ col,
        v col * coeff col x * Complex.exp ((col.val.1 : ℂ) * y))
        row.2.val row.1.val = 0 := by
…

Mentions: OAI.Nagata.Workers.W11.separatedJetMatrix, OAI.Nagata.Workers.W11.mixedJetAtZero

theorem OAI.Nagata.Workers.W11.eventually_injective_finite_jet_matrix line 245

Source documentation

On the manuscript's actual finite index types, its numerical parameter hypotheses and entrywise convergence give eventual injectivity.

theorem eventually_injective_finite_jet_matrix
    {α : Type*} {l : Filter α}
    (d : ℤ) (q m : ℕ) (rho a delta lam : ℝ)
    (ha : 0 < a) (hm : 0 < m) (hrho : 0 ≤ rho) (hdelta : 0 ≤ delta)
    (hlam : 0 < lam) (hlam1 : lam < 1)
    (hratio : 3 * ((d : ℝ) - 3 * (m : ℝ)) = (m : ℝ) * rho)
    (hslack : rho + delta * rho / 9 < lam * a - 9 * (1 - lam))
    (hcoef : 2 * a + a ^ 2 / 9 = (q : ℝ))
    (hmargin : 1 ≤ (q : ℝ) * (1 - lam) * m)
    (B : α → Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ)
    (hB : ∀ row col, Tendsto (fun t => B t row col) l
      (𝓝 ((col.val.2 : ℂ) ^ row.2.val * (col.val.1 : ℂ) ^ row.1.val))) :
…

theorem OAI.Nagata.Workers.W11.finite_jet_matrix_contradiction line 265

Source documentation

The fixed-index matrix contradiction under the stated numerical and kernel hypotheses. No regular choice of kernel vector is required.

theorem finite_jet_matrix_contradiction
    {α : Type*} {l : Filter α} [NeBot l]
    (d : ℤ) (q m : ℕ) (rho a delta lam : ℝ)
    (ha : 0 < a) (hm : 0 < m) (hrho : 0 ≤ rho) (hdelta : 0 ≤ delta)
    (hlam : 0 < lam) (hlam1 : lam < 1)
    (hratio : 3 * ((d : ℝ) - 3 * (m : ℝ)) = (m : ℝ) * rho)
    (hslack : rho + delta * rho / 9 < lam * a - 9 * (1 - lam))
    (hcoef : 2 * a + a ^ 2 / 9 = (q : ℝ))
    (hmargin : 1 ≤ (q : ℝ) * (1 - lam) * m)
    (B : α → Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ)
    (hB : ∀ row col, Tendsto (fun t => B t row col) l
      (𝓝 ((col.val.2 : ℂ) ^ row.2.val * (col.val.1 : ℂ) ^ row.1.val)))
…