ValuationBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Valuation bounds for isolated jets

The boundary monomial ideal controls valuations of remainders. In particular, the valuation of an isolated jet equals its least weight, and initial weights bound every valuation with the prescribed boundary-coordinate values below.

theorem OAI.CartierSections.valuation_unit_zero line 21
theorem OAI.CartierSections.valuation_prod line 26
def OAI.CartierSections.strictValuationIdeal line 34
Source documentation
The strict positive-threshold ideal of a nonnegative additive valuation.
```
def strictValuationIdeal (v : AddValuation A ENNReal) (t : ℝ) : Ideal A where
…
```

theorem OAI.CartierSections.valuation_boundary_monomial line 51

Source documentation

Only the boundary-coordinate values are used; the transverse weights are allowed to vanish even when the original valuation is positive on them.

theorem valuation_boundary_monomial (v : AddValuation A ENNReal)
    (B : Finset ι) (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hz : ∀ i ∈ B, v (algebraMap (MvPolynomial ι k) A (MvPolynomial.X i)) = ENNReal.ofReal (w i))
    (d : ι →₀ ℕ) (hd : ∀ i ∉ B, d i = 0) :
    v (algebraMap (MvPolynomial ι k) A (MvPolynomial.monomial d 1)) =
      ENNReal.ofReal (realWeight w d) := by
…

Mentions: OAI.CartierSections.realWeight

theorem OAI.CartierSections.valuation_gt_of_mem_boundaryWeightIdeal line 73

Source documentation

Elements of the higher-boundary-weight ideal have strictly higher valuation.

theorem valuation_gt_of_mem_boundaryWeightIdeal (v : AddValuation A ENNReal)
    (B : Finset ι) (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hz : ∀ i ∈ B, v (algebraMap (MvPolynomial ι k) A (MvPolynomial.X i)) = ENNReal.ofReal (w i))
    (L : ℝ) (hL : 0 ≤ L) {q : A}
    (hq : q ∈ chartBoundaryWeightIdeal (k := k) B w L) :
…

Mentions: OAI.CartierSections.chartBoundaryWeightIdeal

theorem OAI.CartierSections.valuation_isolated_jet line 88

Source documentation

The isolated-jet congruence determines the valuation.

theorem valuation_isolated_jet (v : AddValuation A ENNReal)
    (B : Finset ι) (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hz : ∀ i ∈ B, v (algebraMap (MvPolynomial ι k) A (MvPolynomial.X i)) = ENNReal.ofReal (w i))
    (α : ι →₀ ℕ) (hα : ∀ i ∉ B, α i = 0) {u q g : A} (hu : IsUnit u)
    (hq : q ∈ chartBoundaryWeightIdeal (k := k) B w (realWeight w α))
…

Mentions: OAI.CartierSections.chartBoundaryWeightIdeal, OAI.CartierSections.realWeight

theorem OAI.CartierSections.valuation_ge_initial_weight line 113

Source documentation

The initial weight bounds the valuation below by faithful flatness of expansion.

theorem valuation_ge_initial_weight
    (θ : A →ₐ[k] MvPowerSeries ι k)
    (hcoord : ∀ i, θ (algebraMap (MvPolynomial ι k) A (MvPolynomial.X i)) = MvPowerSeries.X i)
    (hθ : θ.toRingHom = algebraMap A (MvPowerSeries ι k))
    (v : AddValuation A ENNReal) (B : Finset ι) (w : ι → ℝ)
    (hw : ∀ i, 0 ≤ w i) (hwzero : ∀ i ∉ B, w i = 0)
    (hz : ∀ i ∈ B, v (algebraMap (MvPolynomial ι k) A (MvPolynomial.X i)) = ENNReal.ofReal (w i))
    (f : A) (L : ℝ)
    (hL : ∀ d, MvPowerSeries.coeff d (θ f) ≠ 0 → L ≤ realWeight w d) :
    ENNReal.ofReal L ≤ v f := by
…

Mentions: OAI.CartierSections.realWeight