Auxiliary-family Wronskian estimates at a Dedekind place

This file transports the algebraic local cases (ii)--(iv) in Corvaja--Zannier's Proposition 2 from Laurent series to an arbitrary height-one DVR place. The derivation is only required to preserve the DVR; no choice of a normalized local parameter is used.

The case-(iii) column operation is exactly the lower-unitriangular matrix caseIIIColumnMatrix. Consequently the resulting estimates retain the source terms: the triangular u contribution, the h * k contribution of v, the k copies of the ratio rho, the full grid sum, and the loss given by the sum of the selected derivative orders.

Source provenance: published pages 1935--1936; checked semantic reconstruction Papers/CorvajaZannier2013/CorvajaZannier2013.tex, lines 636--732.

def BGS.CorvajaZannier.dedekindLocalAuxiliaryFamily {L : Type u_3} [Field L] (u v rho : L) (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h → L

The auxiliary family with the ratio column written using an explicit parameter rho.

Equations

• BGS.CorvajaZannier.dedekindLocalAuxiliaryFamily u v rho h k (Sum.inl i) = u ^ ↑i * rho
• BGS.CorvajaZannier.dedekindLocalAuxiliaryFamily u v rho h k (Sum.inr rs) = u ^ ↑rs.1 * v ^ ↑rs.2

@[simp]

theorem BGS.CorvajaZannier.dedekindLocalAuxiliaryFamily_div_eq_auxiliaryFamily {L : Type u_3} [Field L] (u v : L) (h k : ℕ) : dedekindLocalAuxiliaryFamily u v ((1 - u) / (1 - v)) h k = auxiliaryFamily u v h k

def BGS.CorvajaZannier.dedekindCaseIIIImprovedAuxiliaryFamily {L : Type u_3} [Field L] (u v rho : L) (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h → L

The case-(iii) family after replacing each first-block column u ^ i * rho by u ^ i * v ^ h * rho.

Equations

• BGS.CorvajaZannier.dedekindCaseIIIImprovedAuxiliaryFamily u v rho h k (Sum.inl i) = u ^ ↑i * v ^ h * rho
• BGS.CorvajaZannier.dedekindCaseIIIImprovedAuxiliaryFamily u v rho h k (Sum.inr rs) = u ^ ↑rs.1 * v ^ ↑rs.2

theorem BGS.CorvajaZannier.indexedDedekindLocalColumnCombination_caseIIIColumnMatrix {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] (u v rho : L) (h k : ℕ) (hrho : (1 - v) * rho = 1 - u) : indexedDedekindLocalColumnCombination (dedekindLocalAuxiliaryFamily u v rho h k) (caseIIIColumnMatrix h k) = dedekindCaseIIIImprovedAuxiliaryFamily u v rho h k

The determinant-one source column operation performs the case-(iii) replacement over an arbitrary fraction field.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_auxiliaryFamily_caseII_nonnegative_of_integral {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain 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) (huIntegral : ∃ (u0 : R), u = (algebraMap R L) u0) (hvIntegral : ∃ (v0 : R), v = (algebraMap R L) v0) (hratioIntegral : ∃ (rho0 : R), (1 - u) / (1 - v) = (algebraMap R L) rho0) : 0 ≤ finitePlaceOrderTop vPlace (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Case (ii): if u, v, and the ratio are all represented by elements of the DVR, then the auxiliary Wronskian is regular.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_caseIII_source_lower_bound {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) (pi : R) (hpi : Irreducible pi) (hpiIdeal : vPlace.asIdeal = Ideal.span {pi}) (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 rho : L) (hrhoIdentity : (1 - v) * rho = 1 - u) (hu : u ≠ 0) (hv : v ≠ 0) (hrho : rho ≠ 0) : ↑((k * (k - 1) / 2) • finitePlaceOrder vPlace u + (h * k) • finitePlaceOrder vPlace v + k • finitePlaceOrder vPlace rho + ∑ 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 (dedekindLocalAuxiliaryFamily u v rho h k)).det

Case (iii) at a Dedekind DVR place, in the displayed source form. The grid contribution is retained as the exact sum that cancels under the global product formula.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_caseIV_source_lower_bound {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) (pi : R) (hpi : Irreducible pi) (hpiIdeal : vPlace.asIdeal = Ideal.span {pi}) (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 rho : L) (hu : u ≠ 0) (hv : v ≠ 0) (hrho : rho ≠ 0) : ↑((k * (k - 1) / 2) • finitePlaceOrder vPlace u + k • finitePlaceOrder vPlace rho + ∑ 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 (dedekindLocalAuxiliaryFamily u v rho h k)).det

Case (iv) at a Dedekind DVR place, in the displayed source form.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_auxiliaryFamily_caseIII_source_lower_bound {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) (pi : R) (hpi : Irreducible pi) (hpiIdeal : vPlace.asIdeal = Ideal.span {pi}) (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

Case (iii) connected to the exact Corvaja--Zannier auxiliary family.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_auxiliaryFamily_caseIV_source_lower_bound {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) (pi : R) (hpi : Irreducible pi) (hpiIdeal : vPlace.asIdeal = Ideal.span {pi}) (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

Case (iv) connected to the exact Corvaja--Zannier auxiliary family.