Uniformizer-free Dedekind auxiliary cases

This module packages Corvaja--Zannier local cases (iii) and (iv) using only a DVR-preserving derivation. The uniformizer needed by the determinant estimate is chosen internally. In particular, callers do not need an algebra map from the derivation's constant field into the local DVR.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_auxiliaryFamily_caseIII_source_lower_bound_of_preserves {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra C L] [IsFractionRing R L] (vPlace : IsDedekindDomain.HeightOneSpectrum R) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (h k : ℕ) (epsilon : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finitePlaceOrder vPlace u + (h * k) • finitePlaceOrder vPlace v + k • finitePlaceOrder vPlace ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finitePlaceOrder vPlace (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ finitePlaceOrderTop vPlace (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Uniformizer-free form of source case (iii).

theorem BGS.CorvajaZannier.finitePlaceOrderTop_auxiliaryFamily_caseIV_source_lower_bound_of_preserves {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra C L] [IsFractionRing R L] (vPlace : IsDedekindDomain.HeightOneSpectrum R) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (h k : ℕ) (epsilon : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finitePlaceOrder vPlace u + k • finitePlaceOrder vPlace ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finitePlaceOrder vPlace (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ finitePlaceOrderTop vPlace (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Uniformizer-free form of source case (iv).