Canonical Wronskian sums over all places

Sum the local Wronskian inequalities with residue-degree weights, separating exceptional places from the outside pole height.

noncomputable def BGS.CorvajaZannier.finiteExtensionCanonicalSummationSupport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (S : Finset (FiniteExtensionPlace K L)) (canonical : FiniteExtensionPlace K L →₀ ℤ) (u v rho grid W : L) : Finset (FiniteExtensionPlace K L)

The finite set on which all terms in the canonical Wronskian summation can be nonzero.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.CorvajaZannier.finiteExtensionOutsideHeight (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (rho : L) (S : Finset (FiniteExtensionPlace K L)) : ℕ

The pole height of rho away from an exceptional set.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.CorvajaZannier.finiteExtensionOutsideHeight_negativeSum (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (rho : L) (S : Finset (FiniteExtensionPlace K L)) : ∑ P ∈ (finiteExtensionPrincipalDivisor K L rho).support with P ∉ S ∧ (finiteExtensionPrincipalDivisor K L rho) P < 0, (finiteExtensionPrincipalDivisor K L rho) P * ↑(finiteExtensionPlaceDegree K L P) = -↑(finiteExtensionOutsideHeight K L rho S)

theorem BGS.CorvajaZannier.globalWronskianInequality_of_finiteExtensionCanonicalPlacewiseBounds (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (S : Finset (FiniteExtensionPlace K L)) (canonical : FiniteExtensionPlace K L →₀ ℤ) (u v rho grid W : L) (h k n sigma chi : ℕ) (hu : u ≠ 0) (hgrid : grid ≠ 0) (hW : W ≠ 0) (hUOutside : ∀ P ∉ S, (finiteExtensionPrincipalDivisor K L u) P = 0) (hGridOutside : ∀ P ∉ S, (finiteExtensionPrincipalDivisor K L grid) P = 0) (hVPositiveSupport : ∀ (P : FiniteExtensionPlace K L), 0 < (finiteExtensionPrincipalDivisor K L v) P → P ∈ S) (hEuler : finiteExtensionDivisorDegree K L canonical + ∑ P ∈ S, ↑(finiteExtensionPlaceDegree K L P) ≤ ↑chi) (hRhoSupport : -(↑(finiteExtensionPositiveDegree K L u) + ↑(finiteExtensionPositiveDegree K L v)) ≤ ∑ P ∈ S, (finiteExtensionPrincipalDivisor K L rho) P * ↑(finiteExtensionPlaceDegree K L P)) (hCaseI : ∀ P ∉ S, (finiteExtensionPrincipalDivisor K L rho) P < 0 → ↑n * (finiteExtensionPrincipalDivisor K L rho) P ≤ ↑sigma * canonical P + (finiteExtensionPrincipalDivisor K L W) P) (hCaseII : ∀ P ∉ S, 0 ≤ (finiteExtensionPrincipalDivisor K L rho) P → 0 ≤ ↑sigma * canonical P + (finiteExtensionPrincipalDivisor K L W) P) (hCaseIII : ∀ P ∈ S, 0 < (finiteExtensionPrincipalDivisor K L v) P → ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) P + ↑(h * k) * (finiteExtensionPrincipalDivisor K L v) P + ↑k * (finiteExtensionPrincipalDivisor K L rho) P + (finiteExtensionPrincipalDivisor K L grid) P - ↑sigma ≤ ↑sigma * canonical P + (finiteExtensionPrincipalDivisor K L W) P) (hCaseIV : ∀ P ∈ S, (finiteExtensionPrincipalDivisor K L v) P ≤ 0 → ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) P + ↑k * (finiteExtensionPrincipalDivisor K L rho) P + (finiteExtensionPrincipalDivisor K L grid) P - ↑sigma ≤ ↑sigma * canonical P + (finiteExtensionPrincipalDivisor K L W) P) : ↑(h * k) * ↑(finiteExtensionPositiveDegree K L v) - ↑k * (↑(finiteExtensionPositiveDegree K L u) + ↑(finiteExtensionPositiveDegree K L v)) - ↑sigma * ↑chi ≤ ↑n * ↑(finiteExtensionOutsideHeight K L rho S)

Exhaustive residue-degree-weighted summation with a genuine canonical divisor and a nonzero global Wronskian.