Seshadri constants of points in the plane

AbbreviationPolynomials in two complex variables#✓fully proved

A plane polynomial is a polynomial \(f \in \mathbb{C}[X_0, X_1]\) in two variables \(X_0, X_1\) with complex coefficients.

Such polynomials are used to represent affine plane curves.

abbrev PlanePolynomial : Type := MvPolynomial (Fin 2) ℂ

Used by 5

Used byThe affine Seshadri constant is at most one · Multiplicity of a plane polynomial at a point · The first-coordinate line through a point has multiplicity one there · Seshadri ratios of ten points · Translate of a plane polynomial

AbbreviationPoints of the complex affine plane#✓fully proved

A point of the complex affine plane is a pair \(a = (a_0, a_1)\) of complex numbers, that is, an element of \(\mathbb{C}^2\), with coordinates indexed by \(0\) and \(1\).

abbrev AffinePoint : Type := Fin 2 → ℂ

Used by 7

Used bySeshadri constant of ten affine points · The affine Seshadri constant is at most one · Generic ten-point Seshadri constant · Multiplicity of a plane polynomial at a point · The first-coordinate line through a point has multiplicity one there · Seshadri ratios of ten points · Translate of a plane polynomial

DefinitionTranslate of a plane polynomial#✓fully proved

For a polynomial \(f \in \mathbb{C}[x_1, x_2]\) and a point \(a = (a_1, a_2) \in \mathbb{C}^2\), the translate of \(f\) by \(a\) is the polynomial \(f(x_1 + a_1, x_2 + a_2)\), obtained by substituting \(x_i + a_i\) for \(x_i\). It moves the point \(a\) to the origin.

noncomputable def shifted (f : PlanePolynomial) (a : AffinePoint) : PlanePolynomial :=
  MvPolynomial.aeval (fun i => MvPolynomial.X i + MvPolynomial.C (a i)) f

Uses 2 · Used by 3

Statement usesPoints of the complex affine plane · Polynomials in two complex variables

Used byThe affine Seshadri constant is at most one · Multiplicity of a plane polynomial at a point · The first-coordinate line through a point has multiplicity one there

DefinitionTotal degree of a monomial#✓fully proved

The total degree of the exponent vector \(m = (m_0, m_1)\) of a monomial \(X_0^{m_0} X_1^{m_1}\) in two variables is \(m_0 + m_1\).

def monomialDegree (m : Fin 2 →₀ ℕ) : ℕ :=
  ∑ i, m i

Used by 3

Used byThe affine Seshadri constant is at most one · Multiplicity of a plane polynomial at a point · The first-coordinate line through a point has multiplicity one there

DefinitionMultiplicity of a plane polynomial at a point#✓fully proved

For a polynomial \(f \in \mathbb{C}[X_0, X_1]\) and a point \(a = (a_0, a_1) \in \mathbb{C}^2\), the multiplicity of \(f\) at \(a\) is the least total degree of a monomial occurring with nonzero coefficient in the translated polynomial \(f(X_0 + a_0, X_1 + a_1)\). For the zero polynomial it is \(0\).

noncomputable def multiplicity (f : PlanePolynomial) (a : AffinePoint) : ℕ :=
  if h : (shifted f a).support.Nonempty then
    ((shifted f a).support.image monomialDegree).min'
      (Finset.image_nonempty.mpr h)
  else 0

Uses 4 · Used by 3

Statement usesPoints of the complex affine plane · Polynomials in two complex variables · Total degree of a monomial · Translate of a plane polynomial

Used byThe affine Seshadri constant is at most one · The first-coordinate line through a point has multiplicity one there · Seshadri ratios of ten points

TheoremThe first-coordinate line through a point has multiplicity one there#✓fully proved

For every point \(a = (a_0, a_1) \in \mathbb{C}^2\), the polynomial \(X_0 - a_0 \in \mathbb{C}[X_0, X_1]\), which defines the line through \(a\) on which the first coordinate is constant, has multiplicity \(1\) at \(a\).

theorem multiplicity_X_sub_C (a : AffinePoint) :
    multiplicity (MvPolynomial.X 0 - MvPolynomial.C (a 0)) a = 1

Uses 5 · Used by 1

Statement usesPoints of the complex affine plane · Polynomials in two complex variables · Multiplicity of a plane polynomial at a point

Proof usesTotal degree of a monomial · Translate of a plane polynomial

Used byThe affine Seshadri constant is at most one

DefinitionSeshadri ratios of ten points#✓fully proved

For a configuration \(x = (x_0, \dots, x_9)\) of ten points of \(\mathbb{C}^2\), not necessarily distinct, the Seshadri ratios of \(x\) are the real numbers \(\deg f / \sum_{i=0}^{9} \operatorname{mult}_{x_i} f\), where \(f\) ranges over the nonzero polynomials in \(\mathbb{C}[X_0, X_1]\) with \(\sum_{i=0}^{9} \operatorname{mult}_{x_i} f > 0\), \(\deg f\) is the total degree of \(f\), and \(\operatorname{mult}_{x_i} f\) is the multiplicity of \(f\) at \(x_i\).

def seshadriRatios (x : Fin 10 → AffinePoint) : Set ℝ :=
  {r | ∃ f : PlanePolynomial, f ≠ 0 ∧
    0 < ∑ i, multiplicity f (x i) ∧
    r = (f.totalDegree : ℝ) / ((∑ i, multiplicity f (x i) : ℕ) : ℝ)}

Uses 3 · Used by 2

Statement usesPoints of the complex affine plane · Polynomials in two complex variables · Multiplicity of a plane polynomial at a point

Used bySeshadri constant of ten affine points · The affine Seshadri constant is at most one

DefinitionSeshadri constant of ten affine points#✓fully proved

For a configuration \(x = (x_0, \dots, x_9)\) of ten points of \(\mathbb{C}^2\), not necessarily distinct, the affine Seshadri constant of \(x\) is the infimum of the ratios \(\deg f / \sum_{i=0}^{9} \operatorname{mult}_{x_i} f\) over all nonzero polynomials \(f \in \mathbb{C}[X_0, X_1]\) with \(\sum_{i=0}^{9} \operatorname{mult}_{x_i} f > 0\), where \(\deg f\) is the total degree of \(f\) and \(\operatorname{mult}_{x_i} f\) is the multiplicity of \(f\) at \(x_i\).

The set of these ratios is nonempty and bounded below by \(0\).

noncomputable def affineSeshadriConstant (x : Fin 10 → AffinePoint) : ℝ :=
  sInf (seshadriRatios x)

Uses 2 · Used by 2

Statement usesPoints of the complex affine plane · Seshadri ratios of ten points

Used byThe affine Seshadri constant is at most one · Generic ten-point Seshadri constant

TheoremThe affine Seshadri constant is at most one#✓fully proved

For every configuration \(x = (x_0, \dots, x_9)\) of ten points of \(\mathbb{C}^2\), not necessarily distinct, the affine Seshadri constant of \(x\) is at most \(1\).

The bound comes from the polynomial \(X_0 - c \in \mathbb{C}[X_0, X_1]\), where \(c\) is the first coordinate of \(x_0\): it has total degree \(1\) and multiplicity \(1\) at \(x_0\).

theorem affineSeshadriConstant_le_one (x : Fin 10 → AffinePoint) :
    affineSeshadriConstant x ≤ 1

Uses 8

Statement usesPoints of the complex affine plane · Seshadri constant of ten affine points

Proof usesPolynomials in two complex variables · Total degree of a monomial · Multiplicity of a plane polynomial at a point · The first-coordinate line through a point has multiplicity one there · Seshadri ratios of ten points · Translate of a plane polynomial

DefinitionGeneric ten-point Seshadri constant#✓fully proved

The generic ten-point Seshadri constant is the supremum, over all configurations \(x = (x_0, \dots, x_9)\) of ten pairwise distinct points of \(\mathbb{C}^2\), of the affine Seshadri constant of \(x\).

This models the Seshadri constant of ten very general points of \(\mathbb{P}^2\) in one affine chart.

noncomputable def genericSeshadriConstant : ℝ :=
  sSup {r | ∃ x : Fin 10 → AffinePoint, Function.Injective x ∧
    r = affineSeshadriConstant x}

Uses 2 · Used by 1

Statement usesPoints of the complex affine plane · Seshadri constant of ten affine points

Used byTen-point Seshadri constant

DefinitionTen-point Seshadri constant#✓fully proved

The ten-point Seshadri constant is the generic ten-point Seshadri constant: the supremum, over all configurations of ten pairwise distinct points of \(\mathbb{C}^2\), of their affine Seshadri constants.

It models the catalogue constant \(C_{74}\), the Seshadri constant of \(\mathbb{P}^2\) at ten very general points, in one affine chart.

noncomputable def seshadriConstant10 : ℝ :=
  genericSeshadriConstant

Uses 1 · Used by 6

Statement usesGeneric ten-point Seshadri constant

Used byCiliberto–Miranda lower bound for the ten-point Seshadri constant · Eckl's 2008 lower bound for the ten-point Seshadri constant · Eckl's 2011 lower bound for the ten-point Seshadri constant · Harbourne–Roé lower bound for the ten-point Seshadri constant · Nagata's conjecture for ten points · Submaximal upper bound for the ten-point Seshadri constant

DefinitionNagata's conjecture for ten points#✓fully proved

The proposition that the generic ten-point Seshadri constant of \(\mathbb{P}^2\), in the affine-chart model, equals \(1/\sqrt{10}\).

It is recorded as a proposition only and is not asserted.

def nagataConjecture10 : Prop :=
  seshadriConstant10 = 1 / Real.sqrt 10

Uses 1

Statement usesTen-point Seshadri constant

TheoremEckl's 2008 lower bound for the ten-point Seshadri constant#●ready to prove

The generic ten-point Seshadri constant of \(\mathbb{P}^2\), in the affine-chart model, is at least \(4/13\).

theorem_wanted eckl2008LowerBound_wanted :
    (4 / 13 : ℝ) ≤ seshadriConstant10

Sources

• Eckl (2008), asymptotic Dumnicki method, catalogue lower bound 4/13.

Uses 1

Statement usesTen-point Seshadri constant

TheoremHarbourne–Roé lower bound for the ten-point Seshadri constant#●ready to prove

The generic ten-point Seshadri constant of \(\mathbb{P}^2\), in the affine-chart model, is at least \(177/560\).

theorem_wanted harbourneRoe2009LowerBound_wanted :
    (177 / 560 : ℝ) ≤ seshadriConstant10

Sources

• Harbourne--Roé (2009), nef divisor bound 177/560.

Uses 1

Statement usesTen-point Seshadri constant

TheoremCiliberto–Miranda lower bound for the ten-point Seshadri constant#●ready to prove

The generic ten-point Seshadri constant of \(\mathbb{P}^2\), in the affine-chart model, is at least \(55/174\).

theorem_wanted cilibertoMiranda2011LowerBound_wanted :
    (55 / 174 : ℝ) ≤ seshadriConstant10

Sources

• Ciliberto--Miranda (2011), degeneration bound 55/174.

Uses 1

Statement usesTen-point Seshadri constant

TheoremEckl's 2011 lower bound for the ten-point Seshadri constant#●ready to prove

The generic ten-point Seshadri constant of \(\mathbb{P}^2\), in the affine-chart model, is at least \(117/370\).

theorem_wanted eckl2011LowerBound_wanted :
    (117 / 370 : ℝ) ≤ seshadriConstant10

Sources

• Eckl (2011), improved catalogue lower bound 117/370.

Uses 1

Statement usesTen-point Seshadri constant

TheoremSubmaximal upper bound for the ten-point Seshadri constant#●ready to prove

The generic ten-point Seshadri constant of \(\mathbb{P}^2\), in the affine-chart model, is at most \(1/\sqrt{10}\).

theorem_wanted submaximalUpperBound_wanted :
    seshadriConstant10 ≤ 1 / Real.sqrt 10

Sources

• the general submaximal upper bound ε ≤ √(D²/r) for D = 𝒪_{ℙ²}(1) and r = 10.

Uses 1

Statement usesTen-point Seshadri constant

12 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.