The log-canonical degree budget for a plane curve

This module combines the canonical-different estimate with the weighted zero/pole boundary estimate. It is the exact geometric input chi = 2ab used by the exhaustive-place form of Corvaja--Zannier Proposition 2.

theorem BGS.CorvajaZannier.planeCurve_canonicalDifferent_add_propositionTwoExceptional_weightedDegree_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have hx := ⋯; finiteExtensionDivisorDegree K (PlaneCurveFunctionField f) (finiteExtensionCanonicalDifferentDivisor K (PlaneCurveFunctionField f) ⋯) + ∑ w ∈ propositionTwoExceptionalPlaces K (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n), ↑(finiteExtensionPlaceDegree K (PlaneCurveFunctionField f) w) ≤ ↑(2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)

The canonical divisor together with the actual weighted zero/pole boundary of positive coordinate powers has degree at most twice the product of the two coordinate degrees.