IsolatedJets.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Isolation of algebraic power series jets

Bounded Euler and transverse differential operators isolate a monomial modulo the ideal of strictly higher weight. Dickson finiteness identifies support conditions with membership in algebraic monomial ideals.

theorem OAI.CartierSections.euler_isolates_coefficients line 23

Source documentation

Bounded Euler and partial operators isolate the chosen boundary exponent.

theorem euler_isolates_coefficients
    (B : Finset ι) (N : ℕ) (w : ι → ℝ)
    (hwzero : ∀ i ∉ B, w i = 0)
    {f : MvPowerSeries ι k} {γ : ι →₀ ℕ}
    (hγ : IsInitialExponent w f γ)
    (hbound : ∀ d, IsInitialExponent w f d → partialDegree B d ≤ N) :
    ∃ α β : ι →₀ ℕ,
      α + β = γ ∧
      (∀ i ∉ B, α i = 0) ∧ (∀ i ∈ B, β i = 0) ∧
      let g := iterPartial β.toMultiset.toList (iterEuler (eulerFactors B N α) f)
…

Mentions: OAI.CartierSections.IsInitialExponent, OAI.CartierSections.partialDegree, OAI.CartierSections.iterPartial, OAI.CartierSections.iterEuler, OAI.CartierSections.eulerFactors

theorem OAI.CartierSections.isolated_series_unit_remainder line 87

Source documentation

An isolated initial coefficient is a monomial times a formal unit, up to terms of strictly greater weight.

theorem isolated_series_unit_remainder
    (B : Finset ι) (w : ι → ℝ) (α : ι →₀ ℕ)
    (hα : ∀ i ∉ B, α i = 0)
    (g : MvPowerSeries ι k) (hcoeff : MvPowerSeries.coeff α g ≠ 0)
    (hle : ∀ d, MvPowerSeries.coeff d g ≠ 0 → realWeight w α ≤ realWeight w d)
    (hisolate : ∀ d, MvPowerSeries.coeff d g ≠ 0 →
      realWeight w d = realWeight w α → ∀ i ∈ B, d i = α i) :
    ∃ u q : MvPowerSeries ι k, IsUnit u ∧
      g = MvPowerSeries.monomial α 1 * u + q ∧
      ∀ d, MvPowerSeries.coeff d q ≠ 0 → realWeight w α < realWeight w d := by
…

Mentions: OAI.CartierSections.realWeight

theorem OAI.CartierSections.finite_dominated_generators line 129
Source documentation
Dickson finiteness supplies a finite subset of any collection of exponent vectors, with every vector dominating one of those generators.
```
theorem finite_dominated_generators [Fintype ι] (S : Set (ι →₀ ℕ)) :
    ∃ T : Finset (ι →₀ ℕ), (↑T : Set (ι →₀ ℕ)) ⊆ S ∧
      ∀ d ∈ S, ∃ e ∈ T, e ≤ d := by
…
```

theorem OAI.CartierSections.series_mem_span_finite_monomials line 147

Source documentation

A formal power series supported on multiples of finitely many monomials is a finite sum of those monomials times formal power series.

theorem series_mem_span_finite_monomials
    (T : Finset (ι →₀ ℕ)) (f : MvPowerSeries ι k)
    (hcover : ∀ d, MvPowerSeries.coeff d f ≠ 0 → ∃ e ∈ T, e ≤ d) :
    f ∈ Ideal.span ((fun e => (MvPowerSeries.monomial e 1 : MvPowerSeries ι k)) ''
      (T : Set (ι →₀ ℕ))) := by
…

theorem OAI.CartierSections.series_mem_span_monomials line 187

Source documentation

Coefficient support in an arbitrary monomial up-set implies membership in the algebraic ideal span.

theorem series_mem_span_monomials [Fintype ι]
    (S : Set (ι →₀ ℕ)) (f : MvPowerSeries ι k)
    (hcover : ∀ d, MvPowerSeries.coeff d f ≠ 0 → ∃ e ∈ S, e ≤ d) :
    f ∈ Ideal.span ((fun e => (MvPowerSeries.monomial e 1 : MvPowerSeries ι k)) '' S) := by
…

def OAI.CartierSections.boundaryWeightIdeal line 208
Source documentation
The ideal generated by boundary monomials of weight strictly above L.
```
noncomputable def boundaryWeightIdeal (B : Finset ι) (w : ι → ℝ) (L : ℝ) :
    Ideal (MvPowerSeries ι k) :=
…
```
theorem OAI.CartierSections.strict_support_mem_boundaryWeightIdeal line 213

theorem OAI.CartierSections.algebraic_series_isolated_jet line 235

Source documentation

An algebraic power series admits an isolated jet modulo the boundary weight ideal, with a uniform linear bound on differential order.

theorem algebraic_series_isolated_jet [CharZero k]
    {f : MvPowerSeries ι k} (hf : f ≠ 0)
    (s : Finset ℕ) (p : ℕ → MvPolynomial ι k) (N : ℕ)
    (hdeg : ∀ j ∈ s, (p j).totalDegree ≤ N)
    (hnonzero : ∃ j ∈ s, p j ≠ 0)
    (hrelation : ∑ j ∈ s, (p j : MvPowerSeries ι k) * f ^ j = 0)
    (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (B : Finset ι)
    (hB : ∀ i ∈ B, 0 < w i) (hwzero : ∀ i ∉ B, w i = 0) :
    ∃ (γ α β : ι →₀ ℕ) (u q : MvPowerSeries ι k),
      IsInitialExponent w f γ ∧ exponentDegree γ ≤ N ∧
      α + β = γ ∧ (∀ i ∉ B, α i = 0) ∧ (∀ i ∈ B, β i = 0) ∧
      realWeight w α = realWeight w γ ∧
…

Mentions: OAI.CartierSections.IsInitialExponent, OAI.CartierSections.exponentDegree, OAI.CartierSections.realWeight