ThetaMatrices.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Theta jet matrices and their basis data

def OAI.Nagata.Workers.W11.thetaJetMatrix line 19
Source documentation
The actual mixed-derivative matrix of all three scalar coefficient branches. The marks are offsets aᵢ = x₀ - xᵢ in (0,1), as in §03's product limit; they are not the original point exponents xᵢ.
```
def thetaJetMatrix (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (marks : Fin 9 → ℝ) (τ : ℝ) :
    Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ :=
…
```

theorem OAI.Nagata.Workers.W11.tendsto_thetaJetMatrix_entries line 27

Source documentation

Entrywise convergence of the literal theta jet matrix, with no assumed derivative convergence: that input is discharged by the scalar analytic theorem.

theorem tendsto_thetaJetMatrix_entries
    {α : Type*} {l : Filter α} {τ : α → ℝ}
    (d : ℤ) (q m : ℕ) (a delta : ℝ) (marks : Fin 9 → ℝ)
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ t in l, 0 < τ t) :
    ∀ row col, Tendsto (fun t => thetaJetMatrix d q m a delta marks (τ t) row col)
      l (𝓝 (B0 d q m a delta row col)) := by
…

Mentions: OAI.Nagata.Workers.W11.thetaJetMatrix

def OAI.Nagata.Workers.W11.thetaScalarCombination line 39

Source documentation

The literal finite scalar expression for a coefficient vector.

def thetaScalarCombination (d : ℤ) (m : ℕ) (a delta : ℝ)
    (marks : Fin 9 → ℝ) (τ : ℝ) (v : Column d (m : ℤ) a delta → ℂ)
    (x y : ℂ) : ℂ :=
…

def OAI.Nagata.Workers.W11.thetaScalarCombinationLinear line 46

Source documentation

The actual finite scalar expansion is linear in its coefficients.

def thetaScalarCombinationLinear (d : ℤ) (m : ℕ) (a delta : ℝ)
    (marks : Fin 9 → ℝ) (τ : ℝ) :
    (Column d (m : ℤ) a delta → ℂ) →ₗ[ℂ] (ℂ → ℂ → ℂ) where
…

theorem OAI.Nagata.Workers.W11.thetaScalarCombination_injective_of_jets line 59

Source documentation

Jet determination of a coefficient vector implies noncancellation of the actual finite scalar expansion as a function, without assuming a basis.

theorem thetaScalarCombination_injective_of_jets
    (d : ℤ) (q m : ℕ) (a delta : ℝ) (marks : Fin 9 → ℝ) (τ : ℝ)
    (hjets : ∀ v : Column d (m : ℤ) a delta → ℂ,
      (∀ row : JetIndex q m,
        mixedJetAtZero (thetaScalarCombination d m a delta marks τ v)
          row.2.val row.1.val = 0) → v = 0) :
    Function.Injective (thetaScalarCombination d m a delta marks τ) := by
…

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

theorem OAI.Nagata.Workers.W11.eventually_thetaJetMatrix_kernel_iff_mixedJets line 78

Source documentation

For sufficiently small parameters the actual scalar expression has zero prescribed mixed jets iff its coefficient vector is a theta-matrix kernel vector. The differentiability needed for finite-sum linearity is discharged.

theorem eventually_thetaJetMatrix_kernel_iff_mixedJets
    {α : Type*} {l : Filter α} {τ : α → ℝ}
    (d : ℤ) (q m : ℕ) (a delta : ℝ) (marks : Fin 9 → ℝ)
    (hτ : Tendsto τ l (𝓝 0)) (hτpos : ∀ᶠ t in l, 0 < τ t) :
    ∀ᶠ t in l, ∀ v : Column d (m : ℤ) a delta → ℂ,
      (thetaJetMatrix d q m a delta marks (τ t)).mulVec v = 0 ↔
      ∀ row : JetIndex q m,
        mixedJetAtZero (thetaScalarCombination d m a delta marks (τ t) v)
          row.2.val row.1.val = 0 := by
…

Mentions: OAI.Nagata.Workers.W11.thetaJetMatrix, OAI.Nagata.Workers.W11.mixedJetAtZero, OAI.Nagata.Workers.W11.thetaScalarCombination

theorem OAI.Nagata.Workers.W11.eventually_injective_thetaJetMatrix line 111
theorem OAI.Nagata.Workers.W11.thetaJetMatrix_kernel_contradiction line 129

theorem OAI.Nagata.Workers.W11.eventually_thetaScalarCombination_jet_injective line 149

Source documentation

For sufficiently small positive parameters, the literal scalar combination can have all prescribed mixed jets zero only when every coefficient is zero. This result contains no assumed smoothness, derivative convergence or rank.

theorem eventually_thetaScalarCombination_jet_injective
    (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)
    (marks : Fin 9 → ℝ)
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1) :
    ∀ᶠ τ in 𝓝[>] (0 : ℝ), ∀ v : Column d (m : ℤ) a delta → ℂ,
      (∀ row : JetIndex q m,
…

theorem OAI.Nagata.Workers.W11.eventually_thetaScalarCombination_injective line 173

Source documentation

Noncancellation of the actual scalar column expansion for sufficiently small positive parameters: distinct coefficient vectors define distinct functions of the two local variables.

theorem eventually_thetaScalarCombination_injective
    (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)
    (marks : Fin 9 → ℝ)
    (hmarks : ∀ i, 0 < marks i) (hmarksone : ∀ i, marks i < 1) :
    ∀ᶠ τ in 𝓝[>] (0 : ℝ),
      Function.Injective (thetaScalarCombination d m a delta marks τ) :=
…

Mentions: OAI.Nagata.Workers.W11.thetaScalarCombination