Degree-weighted Corvaja--Zannier Wronskian summation #
The published proof sums local orders with the residue degree of each place.
This module derives the weighted version of the four-case global inequality by
replacing a place of weight e by e identical copies and applying
globalWronskianInequality_of_placewiseBounds.
This is the finite combinatorial form of the weighted divisor summation in Corvaja--Zannier, Proposition 2 (published reconstruction, pp. 15--16).
theorem
BGS.CorvajaZannier.globalWronskianInequality_of_weightedPlacewiseBounds
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(weight : ι → ℕ)
(S : Finset ι)
(ordU ordV ordRho ordGrid ordW : ι → ℤ)
(h k n sigma degreeU degreeV chi heightOutside : ℕ)
(canonicalDegree : ℤ)
(hUOutside : ∀ i ∉ S, ordU i = 0)
(hGridOutside : ∀ i ∉ S, ordGrid i = 0)
(hUSum : ∑ i : ι, ordU i * ↑(weight i) = 0)
(hGridSum : ∑ i : ι, ordGrid i * ↑(weight i) = 0)
(hDegreeV : ∑ i ∈ S with 0 < ordV i, ordV i * ↑(weight i) = ↑degreeV)
(hOutsideHeight : ∑ i : ι with i ∉ S ∧ ordRho i < 0, ordRho i * ↑(weight i) = -↑heightOutside)
(hCanonical : ∑ i : ι, ordW i * ↑(weight i) = ↑sigma * canonicalDegree)
(hEuler : canonicalDegree + ↑(∑ i ∈ S, weight i) ≤ ↑chi)
(hRhoSupport : -(↑degreeU + ↑degreeV) ≤ ∑ i ∈ S, ordRho i * ↑(weight i))
(hCaseI : ∀ i ∉ S, ordRho i < 0 → ↑n * ordRho i ≤ ordW i)
(hCaseII : ∀ i ∉ S, 0 ≤ ordRho i → 0 ≤ ordW i)
(hCaseIII :
∀ i ∈ S, 0 < ordV i → ↑(k * (k - 1) / 2) * ordU i + ↑(h * k) * ordV i + ↑k * ordRho i + ordGrid i - ↑sigma ≤ ordW i)
(hCaseIV : ∀ i ∈ S, ordV i ≤ 0 → ↑(k * (k - 1) / 2) * ordU i + ↑k * ordRho i + ordGrid i - ↑sigma ≤ ordW i)
:
Residue-degree-weighted finite-support form of the global summation step in the proof of Corvaja--Zannier Proposition 2.