InitialExponents.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Initial exponents of algebraic power series

The algebraic relation bounds initial exponents uniformly in the weights. Generic positive perturbations extend this bound to least faces of nonnegative weights, as used in the logarithmic jet argument of Uniform Cartier sections for Fano-type contractions.

def OAI.CartierSections.IsInitialExponent line 25
Source documentation
A nonzero coefficient of least real weight.
```
def IsInitialExponent (w : ι → ℝ) (f : MvPowerSeries ι k) (d : ι →₀ ℕ) : Prop :=
…
```
theorem OAI.CartierSections.exists_initial_exponent line 29
theorem OAI.CartierSections.IsInitialExponent.unique line 51
theorem OAI.CartierSections.IsInitialExponent.coeff_eq_zero line 56

theorem OAI.CartierSections.coeff_mul_initial line 63

Source documentation

Rationally independent weights prevent cancellation of initial terms.

theorem coeff_mul_initial {w : ι → ℝ} (hw : Function.Injective (realWeight w))
    {f g : MvPowerSeries ι k} {d e : ι →₀ ℕ}
    (hd : IsInitialExponent w f d) (he : IsInitialExponent w g e) :
    MvPowerSeries.coeff (d + e) (f * g) =
      MvPowerSeries.coeff d f * MvPowerSeries.coeff e g := by
…

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

theorem OAI.CartierSections.IsInitialExponent.mul line 85
theorem OAI.CartierSections.initial_one line 103
theorem OAI.CartierSections.IsInitialExponent.pow line 112

theorem OAI.CartierSections.initial_tie_of_sum_eq_zero line 127

Source documentation

A vanishing finite sum with a nonzero term has two terms with the same minimal exponent, for injective real weights. This follows by cancellation at the least-weight coefficient.

theorem initial_tie_of_sum_eq_zero (w : ι → ℝ)
    (hw : Function.Injective (realWeight w))
    (s : Finset J) (F : J → MvPowerSeries ι k) (d : J → (ι →₀ ℕ))
    (hlead : ∀ j ∈ s, F j ≠ 0 → IsInitialExponent w (F j) (d j))
    (hnonzero : ∃ j ∈ s, F j ≠ 0) (hsum : ∑ j ∈ s, F j = 0) :
    ∃ j ∈ s, ∃ l ∈ s, j ≠ l ∧ F j ≠ 0 ∧ F l ≠ 0 ∧ d j = d l := by
…

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

def OAI.CartierSections.exponentDegree line 156
theorem OAI.CartierSections.exponentDegree_add line 158
theorem OAI.CartierSections.exponentDegree_nsmul line 162
theorem OAI.CartierSections.initial_polynomial_degree_le line 166
theorem OAI.CartierSections.algebraic_initial_degree_le line 177
Source documentation
Every initial exponent of a nonzero algebraic power series has degree bounded by the degrees of the polynomial coefficients of its algebraic relation. The bound is independent of the choice of positive rationally independent weights. This algebraic degree estimate bounds the jets in the logarithmic jet argument.
```
theorem algebraic_initial_degree_le [IsDomain k]
    {w : ι → ℝ} (hwpos : ∀ i, 0 < w i) (hw : LinearIndependent ℚ w)
    {f : MvPowerSeries ι k} {γ : ι →₀ ℕ}
    (hγ : IsInitialExponent w f γ)
    (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) :
    exponentDegree γ ≤ N := by
…
```
Mentions: OAI.CartierSections.IsInitialExponent, OAI.CartierSections.exponentDegree
theorem OAI.CartierSections.exists_independent_fin_box line 236
Source documentation
Any finite family of nonempty real intervals contains a rationally independent tuple. The proof uses countability of a finite rational span.
```
theorem exists_independent_fin_box (n : ℕ) (l u : Fin n → ℝ)
    (hlu : ∀ i, l i < u i) :
    ∃ w : Fin n → ℝ, LinearIndependent ℚ w ∧ ∀ i, l i < w i ∧ w i < u i := by
…
```
theorem OAI.CartierSections.exists_independent_box line 259
theorem OAI.CartierSections.realWeight_one_eq_degree line 275
theorem OAI.CartierSections.realWeight_mono line 279
theorem OAI.CartierSections.realWeight_add_const line 283

theorem OAI.CartierSections.degree_perturbation_bound line 289

Source documentation

A useful exact small-perturbation bound.

theorem degree_perturbation_bound {ε : ℝ} (hε : 0 < ε) (N : ℕ) :
    0 < ε / (N + 1 : ℝ) ∧ ε / (N + 1 : ℝ) * N < ε := by
…

theorem OAI.CartierSections.exists_bounded_initial_exponent line 301

Source documentation

An algebraic power series has a coefficient of bounded total degree on its least face for every nonnegative weight, including faces with zero weights. This includes least faces with zero-weight transverse coordinates.

theorem exists_bounded_initial_exponent
    {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) :
    ∃ d, IsInitialExponent w f d ∧ exponentDegree d ≤ N := by
…

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

def OAI.CartierSections.partialDegree line 348
theorem OAI.CartierSections.partialDegree_le line 350
theorem OAI.CartierSections.realWeight_sub_on line 355

theorem OAI.CartierSections.algebraic_initial_partial_degree_le line 364

Source documentation

All exponents on a least face have bounded degree in the coordinates whose weights are positive. A small generic perturbation gives the bound for every exponent on the face.

theorem algebraic_initial_partial_degree_le
    {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)
    {d : ι →₀ ℕ} (hd : IsInitialExponent w f d) :
    partialDegree B d ≤ N := by
…

Mentions: OAI.CartierSections.IsInitialExponent, OAI.CartierSections.partialDegree