Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.PlaneCurveCanonicalGcdBound

The canonical Corvaja--Zannier bound for powered plane coordinates #

This module composes the automatic canonical placewise estimate with the first-coordinate model of a plane function field. Linear independence of the auxiliary family supplies the Wronskian nonvanishing, while the two powered-coordinate height theorems replace abstract positive divisor degrees by the actual bidegree budgets.

source
theorem BGS.CorvajaZannier.finiteExtensionGcdBound_planeCurvePowers_of_auxiliaryFamily_linearIndependent {K : Type u_1} [Field K] [Finite K] [DecidableEq K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (h k : ℕ) (hcard : 0 < h * k + h + k) (chi : ℕ) :
have hx := ⋯; LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n) h k) → finiteExtensionDivisorDegree K (PlaneCurveFunctionField f) (finiteExtensionCanonicalDifferentDivisor K (PlaneCurveFunctionField f) ⋯) + ∑ P ∈ propositionTwoExceptionalPlaces K (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n), ↑(finiteExtensionPlaceDegree K (PlaneCurveFunctionField f) P) ≤ ↑chi → ↑(finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 0 ^ m) (1 - planeCurveFunction f 1 ^ n)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(n * MvPolynomial.degreeOf 0 f) + ↑k / ↑(h * k + h + k) * ↑(m * MvPolynomial.degreeOf 1 f) + (↑(h * k + h + k) - 1) / 2 * ↑chi

The automatic canonical placewise estimate, specialized to u = x^m, v = y^n on a plane curve and expressed using the actual coordinate degrees.

source
theorem BGS.CorvajaZannier.finiteExtensionGcdBound_planeCurvePowers_swapped_of_auxiliaryFamily_linearIndependent {K : Type u_1} [Field K] [Finite K] [DecidableEq K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (h k : ℕ) (hcard : 0 < h * k + h + k) (chi : ℕ) :
have hx := ⋯; LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 1 ^ n) (planeCurveFunction f 0 ^ m) h k) → finiteExtensionDivisorDegree K (PlaneCurveFunctionField f) (finiteExtensionCanonicalDifferentDivisor K (PlaneCurveFunctionField f) ⋯) + ∑ P ∈ propositionTwoExceptionalPlaces K (PlaneCurveFunctionField f) (planeCurveFunction f 1 ^ n) (planeCurveFunction f 0 ^ m), ↑(finiteExtensionPlaceDegree K (PlaneCurveFunctionField f) P) ≤ ↑chi → ↑(finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 1 ^ n) (1 - planeCurveFunction f 0 ^ m)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(m * MvPolynomial.degreeOf 1 f) + ↑k / ↑(h * k + h + k) * ↑(n * MvPolynomial.degreeOf 0 f) + (↑(h * k + h + k) - 1) / 2 * ↑chi

The companion specialization with the powered coordinates exchanged. Here the leading coefficient multiplies the exact height of x^m, while the second coefficient multiplies the degree budget for y^n.