PolynomialValuation.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Weighted valuations on polynomial rings

The least weight of a nonzero coefficient defines a valuation, including weights with ties or zero coordinates. Nonnegative combinations of weight vectors give a domination inequality within a fixed coordinate chart.

def OAI.CartierSections.Monomial.value line 23
Source documentation
The value is the minimum monomial weight, with value infinity at zero.
```
def value (w : σ → ℝ≥0) (p : MvPolynomial σ k) : ENNReal :=
…
```
lemma OAI.CartierSections.Monomial.value_zero line 26
lemma OAI.CartierSections.Monomial.value_le_weight line 29
lemma OAI.CartierSections.Monomial.le_value_iff line 33
lemma OAI.CartierSections.Monomial.value_attained line 37
lemma OAI.CartierSections.Monomial.value_lt_top line 41
lemma OAI.CartierSections.Monomial.value_one line 47
lemma OAI.CartierSections.Monomial.value_add line 50
lemma OAI.CartierSections.Monomial.le_value_mul line 61
Source documentation
No cancellation can create a term below the sum of the two minima.
```
lemma le_value_mul (w : σ → ℝ≥0) (p q : MvPolynomial σ k) :
    value w p + value w q ≤ value w (p*q) := by
…
```
Mentions: OAI.CartierSections.Monomial.value

lemma OAI.CartierSections.Monomial.component_mul_at_lower_bounds line 73

Source documentation

At the sum of the lower bounds, the initial part of a product is the product of the initial parts. This includes non-generic tied weights.

lemma component_mul_at_lower_bounds (w : σ → ℝ≥0) (p q : MvPolynomial σ k)
    (a b : ℝ≥0)
    (hp : ∀ d ∈ p.support, a ≤ Finsupp.weight w d)
    (hq : ∀ d ∈ q.support, b ≤ Finsupp.weight w d) :
    MvPolynomial.weightedHomogeneousComponent w (a+b) (p*q) =
      MvPolynomial.weightedHomogeneousComponent w a p *
        MvPolynomial.weightedHomogeneousComponent w b q := by
…

lemma OAI.CartierSections.Monomial.component_ne_zero_of_attained line 118
lemma OAI.CartierSections.Monomial.value_mul line 130
def OAI.CartierSections.Monomial.valuation line 157
Source documentation
Weighted monomial valuation on the genuine polynomial coordinate ring.
```
def valuation (w : σ → ℝ≥0) : AddValuation (MvPolynomial σ k) ENNReal :=
…
```
lemma OAI.CartierSections.Monomial.valuation_apply line 160
def OAI.CartierSections.Monomial.combine line 169
Source documentation
Coordinatewise nonnegative linear combination of weight vectors.
```
def combine (s : Finset ι) (c : ι → ℝ≥0) (w : ι → σ → ℝ≥0) : σ → ℝ≥0 :=
…
```
lemma OAI.CartierSections.Monomial.weight_combine line 172
lemma OAI.CartierSections.Monomial.combine_dominates line 187
Source documentation
Nonnegative combinations dominate the corresponding combination of values. The homogeneous inequality needs no normalization of the coefficients.
```
lemma combine_dominates [IsDomain k] (s : Finset ι) (c : ι → ℝ≥0) (w : ι → σ → ℝ≥0)
    (p : MvPolynomial σ k) :
    ∑ i ∈ s, (c i : ENNReal) * valuation (w i) p ≤
      valuation (combine s c w) p := by
…
```
Mentions: OAI.CartierSections.Monomial.valuation, OAI.CartierSections.Monomial.combine

lemma OAI.CartierSections.Monomial.linear_equation_combine line 201

Source documentation

Equality of two monomial weights is preserved by nonnegative combinations.

lemma linear_equation_combine (s : Finset ι) (c : ι → ℝ≥0)
    (w : ι → σ → ℝ≥0) (a b : σ →₀ ℕ)
    (h : ∀ i ∈ s, Finsupp.weight (w i) a = Finsupp.weight (w i) b) :
    Finsupp.weight (combine s c w) a = Finsupp.weight (combine s c w) b := by
…

Mentions: OAI.CartierSections.Monomial.combine