Corvaja--Zannier local case (i)

This file formalizes the column elimination and the sharp local Wronskian estimate in case (i) of Corvaja--Zannier's Proposition 2. Repeated negative Laurent orders are eliminated by an explicitly constructed product of transvections. Consequently the column matrix has determinant one; the finite-dimensional elimination is not assumed as a hypothesis.

The second part isolates the exact source inequalities. Pairwise-distinct negative column orders give the first triangular-number gain, and distinct derivative orders give the second. Under the source's cardinal inequalities this sharpens the ordinary Wronskian order to rhoOrder * (epsilon + 1), and hence to rhoOrder * q when epsilon + 1 ≤ q.

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

noncomputable def BGS.CorvajaZannier.laurentPoleDepth {K : Type u_1} [Field K] (f : LaurentSeries K) : ℕ

The depth of the negative part of a Laurent series.

Equations

• BGS.CorvajaZannier.laurentPoleDepth f = (-HahnSeries.order f).toNat

noncomputable def BGS.CorvajaZannier.laurentPoleWeight {K : Type u_1} [Field K] {k : ℕ} (f : Fin k → LaurentSeries K) : ℕ

A terminating measure for repeated leading-term cancellation.

Equations

• BGS.CorvajaZannier.laurentPoleWeight f = ∑ i : Fin k, BGS.CorvajaZannier.laurentPoleDepth (f i)

def BGS.CorvajaZannier.NegativeOrdersPairwiseDistinct {K : Type u_1} [Field K] {ι : Type u_2} (f : ι → LaurentSeries K) : Prop

All negative orders in a finite family are pairwise distinct.

Equations

• BGS.CorvajaZannier.NegativeOrdersPairwiseDistinct f = ∀ ⦃i j : ι⦄, HahnSeries.order (f i) < 0 → HahnSeries.order (f j) < 0 → HahnSeries.order (f i) = HahnSeries.order (f j) → i = j

noncomputable def BGS.CorvajaZannier.cancelLaurentLeadingTerm {K : Type u_1} [Field K] (x y : LaurentSeries K) : LaurentSeries K

Cancel the leading term of x using a series y of the same order.

Equations

• BGS.CorvajaZannier.cancelLaurentLeadingTerm x y = x - (HahnSeries.leadingCoeff x / HahnSeries.leadingCoeff y) • y

@[simp]

theorem BGS.CorvajaZannier.laurentPoleDepth_pos_iff {K : Type u_1} [Field K] (f : LaurentSeries K) : 0 < laurentPoleDepth f ↔ HahnSeries.order f < 0

@[simp]

theorem BGS.CorvajaZannier.laurentPoleDepth_eq_zero_iff {K : Type u_1} [Field K] (f : LaurentSeries K) : laurentPoleDepth f = 0 ↔ 0 ≤ HahnSeries.order f

theorem BGS.CorvajaZannier.order_lt_orderTop_cancelLaurentLeadingTerm {K : Type u_1} [Field K] (x y : LaurentSeries K) (hx : x ≠ 0) (hy : y ≠ 0) (horder : HahnSeries.order x = HahnSeries.order y) : ↑(HahnSeries.order x) < HahnSeries.orderTop (cancelLaurentLeadingTerm x y)

Cancellation of equal leading terms strictly raises Laurent order.

theorem BGS.CorvajaZannier.laurentPoleDepth_cancelLaurentLeadingTerm_lt {K : Type u_1} [Field K] (x y : LaurentSeries K) (hxneg : HahnSeries.order x < 0) (hyneg : HahnSeries.order y < 0) (horder : HahnSeries.order x = HahnSeries.order y) : laurentPoleDepth (cancelLaurentLeadingTerm x y) < laurentPoleDepth x

Leading-term cancellation strictly decreases pole depth.

theorem BGS.CorvajaZannier.indexedLaurentSeriesColumnCombination_mul {K : Type u_1} [Field K] {k : ℕ} (f : Fin k → LaurentSeries K) (A B : Matrix (Fin k) (Fin k) K) : indexedLaurentSeriesColumnCombination (indexedLaurentSeriesColumnCombination f A) B = indexedLaurentSeriesColumnCombination f (A * B)

Successive constant column combinations compose by matrix multiplication.

theorem BGS.CorvajaZannier.exists_det_one_columnMatrix_negativeOrdersPairwiseDistinct {K : Type u_1} [Field K] {k : ℕ} (a : ℤ) (ha : a ≤ 0) (f : Fin k → LaurentSeries K) (hf : ∀ (i : Fin k), a ≤ HahnSeries.order (f i)) : ∃ (A : Matrix (Fin k) (Fin k) K), A.det = 1 ∧ NegativeOrdersPairwiseDistinct (indexedLaurentSeriesColumnCombination f A) ∧ ∀ (i : Fin k), a ≤ HahnSeries.order (indexedLaurentSeriesColumnCombination f A i)

Explicit finite-dimensional elimination of repeated negative orders. The resulting matrix is a product of transvections and therefore has determinant one.

theorem BGS.CorvajaZannier.sum_range_add_le_sum_of_injOn {ι : Type u_2} (s : Finset ι) (w : ι → ℤ) (a : ℤ) (hinj : Set.InjOn w ↑s) (hlower : ∀ i ∈ s, a ≤ w i) : ∑ n ∈ Finset.range s.card, (a + ↑n) ≤ ∑ i ∈ s, w i

Sharp lower sum bound for distinct integers bounded below.

theorem BGS.CorvajaZannier.sum_le_sum_range_sub_of_injOn {ι : Type u_2} (s : Finset ι) (e : ι → ℕ) (epsilon : ℕ) (hinj : Set.InjOn e ↑s) (hupper : ∀ i ∈ s, e i ≤ epsilon) : ∑ i ∈ s, ↑(e i) ≤ ∑ n ∈ Finset.range s.card, (↑epsilon - ↑n)

Sharp upper sum bound for distinct natural numbers bounded above.

theorem BGS.CorvajaZannier.orderTop_indexedWronskian_det_lower_bound_of_poles {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (epsilonOrder : ι → ℕ) (g : ι → LaurentSeries K) (poles : Finset ι) (E : ℤ) (hregular : ∀ i ∉ poles, 0 ≤ HahnSeries.order (g i)) (hselected : ∀ (σ : Equiv.Perm ι), ∑ i ∈ poles, ↑(epsilonOrder (σ i)) ≤ E) : ↑(∑ i ∈ poles, HahnSeries.order (g i) - E) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian epsilonOrder g).det

The determinant bound in which only pole columns pay a derivative-order cost; regular columns contribute a nonnegative order.

theorem BGS.CorvajaZannier.orderTop_indexedWronskian_det_caseI_epsilon_plus_one_lower_bound {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (epsilonOrder : ι → ℕ) (g : ι → LaurentSeries K) (rhoOrder : ℤ) (epsilon : ℕ) (hgdistinct : NegativeOrdersPairwiseDistinct g) (hglower : ∀ (i : ι), rhoOrder ≤ HahnSeries.order (g i)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : ι), epsilonOrder i ≤ epsilon) (hcardRho : rhoOrder ≤ -↑{i : ι | HahnSeries.order (g i) < 0}.card) (hcardEpsilon : {i : ι | HahnSeries.order (g i) < 0}.card ≤ epsilon + 1) : ↑(rhoOrder * ↑(epsilon + 1)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian epsilonOrder g).det

The exact intermediate bound in source case (i).

theorem BGS.CorvajaZannier.orderTop_indexedWronskian_det_caseI_q_lower_bound {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (epsilonOrder : ι → ℕ) (g : ι → LaurentSeries K) (rhoOrder : ℤ) (epsilon q : ℕ) (hgdistinct : NegativeOrdersPairwiseDistinct g) (hglower : ∀ (i : ι), rhoOrder ≤ HahnSeries.order (g i)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : ι), epsilonOrder i ≤ epsilon) (hcardRho : rhoOrder ≤ -↑{i : ι | HahnSeries.order (g i) < 0}.card) (hcardEpsilon : {i : ι | HahnSeries.order (g i) < 0}.card ≤ epsilon + 1) (hrho : rhoOrder ≤ 0) (hepsilonQ : epsilon + 1 ≤ q) : ↑(↑q * rhoOrder) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian epsilonOrder g).det

Source case (i), in the final q * rhoOrder form.

theorem BGS.CorvajaZannier.card_negativeOrders_le_neg {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (g : ι → LaurentSeries K) (a : ℤ) (ha : a ≤ 0) (hgdistinct : NegativeOrdersPairwiseDistinct g) (hglower : ∀ (i : ι), a ≤ HahnSeries.order (g i)) : a ≤ -↑{i : ι | HahnSeries.order (g i) < 0}.card

Pairwise-distinct negative integers bounded below by a nonpositive integer are no more numerous than its pole depth.

theorem BGS.CorvajaZannier.exists_caseI_columnMatrix_and_q_wronskian_bound {K : Type u_1} [Field K] {k : ℕ} (epsilonOrder : Fin k → ℕ) (f : Fin k → LaurentSeries K) (a : ℤ) (epsilon q : ℕ) (ha : a ≤ 0) (hf : ∀ (i : Fin k), a ≤ HahnSeries.order (f i)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ q) : ∃ (A : Matrix (Fin k) (Fin k) K), A.det = 1 ∧ (indexedLaurentSeriesWronskian epsilonOrder (indexedLaurentSeriesColumnCombination f A)).det = (indexedLaurentSeriesWronskian epsilonOrder f).det ∧ ↑(↑q * a) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian epsilonOrder f).det

Complete local case (i) for an arbitrary Fin k family. The theorem constructs the determinant-one elimination matrix, preserves the original Wronskian determinant, and proves the final q * a order bound.

def BGS.CorvajaZannier.caseIColumnMatrix {K : Type u_1} [Field K] (h k : ℕ) (A : Matrix (Fin k) (Fin k) K) : Matrix (Fin k ⊕ Fin (k + 1) × Fin h) (Fin k ⊕ Fin (k + 1) × Fin h) K

Extend a first-block column operation by the identity on the grid columns of the source auxiliary family.

Equations

• BGS.CorvajaZannier.caseIColumnMatrix h k A = Matrix.fromBlocks A 0 0 1

theorem BGS.CorvajaZannier.caseIColumnMatrix_det {K : Type u_1} [Field K] (h k : ℕ) (A : Matrix (Fin k) (Fin k) K) : (caseIColumnMatrix h k A).det = A.det

theorem BGS.CorvajaZannier.indexedColumnCombination_caseIColumnMatrix_inl {K : Type u_1} [Field K] (h k : ℕ) (f : Fin k ⊕ Fin (k + 1) × Fin h → LaurentSeries K) (A : Matrix (Fin k) (Fin k) K) (i : Fin k) : indexedLaurentSeriesColumnCombination f (caseIColumnMatrix h k A) (Sum.inl i) = indexedLaurentSeriesColumnCombination (fun (j : Fin k) => f (Sum.inl j)) A i

theorem BGS.CorvajaZannier.indexedColumnCombination_caseIColumnMatrix_inr {K : Type u_1} [Field K] (h k : ℕ) (f : Fin k ⊕ Fin (k + 1) × Fin h → LaurentSeries K) (A : Matrix (Fin k) (Fin k) K) (rs : Fin (k + 1) × Fin h) : indexedLaurentSeriesColumnCombination f (caseIColumnMatrix h k A) (Sum.inr rs) = f (Sum.inr rs)

noncomputable def BGS.CorvajaZannier.caseITransformedLocalAuxiliaryFamily {K : Type u_1} [Field K] (u v rho : LaurentSeries K) (h k : ℕ) (A : Matrix (Fin k) (Fin k) K) : Fin k ⊕ Fin (k + 1) × Fin h → LaurentSeries K

The full auxiliary family after a case-(i) operation on its first block.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.caseITransformedLocalAuxiliaryFamily_inl {K : Type u_1} [Field K] (u v rho : LaurentSeries K) (h k : ℕ) (A : Matrix (Fin k) (Fin k) K) (i : Fin k) : caseITransformedLocalAuxiliaryFamily u v rho h k A (Sum.inl i) = indexedLaurentSeriesColumnCombination (fun (j : Fin k) => localAuxiliaryFamily u v rho h k (Sum.inl j)) A i

@[simp]

theorem BGS.CorvajaZannier.caseITransformedLocalAuxiliaryFamily_inr {K : Type u_1} [Field K] (u v rho : LaurentSeries K) (h k : ℕ) (A : Matrix (Fin k) (Fin k) K) (rs : Fin (k + 1) × Fin h) : caseITransformedLocalAuxiliaryFamily u v rho h k A (Sum.inr rs) = localAuxiliaryFamily u v rho h k (Sum.inr rs)

theorem BGS.CorvajaZannier.exists_localAuxiliaryFamily_caseI_columnMatrix {K : Type u_1} [Field K] (u v rho : LaurentSeries K) (h k : ℕ) (hu : u ≠ 0) (hrhoNe : rho ≠ 0) (huOrder : HahnSeries.order u = 0) (hrhoOrder : HahnSeries.order rho ≤ 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2)) : ∃ (A : Matrix (Fin k) (Fin k) K), A.det = 1 ∧ NegativeOrdersPairwiseDistinct (caseITransformedLocalAuxiliaryFamily u v rho h k A) ∧ (∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), HahnSeries.order rho ≤ HahnSeries.order (caseITransformedLocalAuxiliaryFamily u v rho h k A i)) ∧ ∀ (rs : Fin (k + 1) × Fin h), caseITransformedLocalAuxiliaryFamily u v rho h k A (Sum.inr rs) = localAuxiliaryFamily u v rho h k (Sum.inr rs)

The exact source-facing case-(i) result for localAuxiliaryFamily. Only the first k columns can have poles; the constructed block matrix eliminates their repeated negative orders and fixes every grid column.

theorem BGS.CorvajaZannier.exists_localAuxiliaryFamily_caseI_q_wronskian_bound {K : Type u_1} [Field K] (u v rho : LaurentSeries K) (h k : ℕ) (epsilonOrder : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (epsilon q : ℕ) (hu : u ≠ 0) (hrhoNe : rho ≠ 0) (huOrder : HahnSeries.order u = 0) (hrhoOrder : HahnSeries.order rho ≤ 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ q) : ∃ (A : Matrix (Fin k) (Fin k) K), A.det = 1 ∧ (indexedLaurentSeriesWronskian epsilonOrder (caseITransformedLocalAuxiliaryFamily u v rho h k A)).det = (indexedLaurentSeriesWronskian epsilonOrder (localAuxiliaryFamily u v rho h k)).det ∧ ↑(↑q * HahnSeries.order rho) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian epsilonOrder (localAuxiliaryFamily u v rho h k)).det

Full source case (i) for the exact Sum-indexed auxiliary family: the first-block elimination preserves the original Wronskian determinant and gives the q * order rho lower bound.

theorem BGS.CorvajaZannier.exists_auxiliaryFamily_caseI_q_wronskian_bound {K : Type u_1} [Field K] (u v : LaurentSeries K) (h k : ℕ) (epsilonOrder : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (epsilon q : ℕ) (hu : u ≠ 0) (hrhoNe : (1 - u) / (1 - v) ≠ 0) (huOrder : HahnSeries.order u = 0) (hrhoOrder : HahnSeries.order ((1 - u) / (1 - v)) ≤ 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ q) : ∃ (A : Matrix (Fin k) (Fin k) K), A.det = 1 ∧ (indexedLaurentSeriesWronskian epsilonOrder (indexedLaurentSeriesColumnCombination (auxiliaryFamily u v h k) (caseIColumnMatrix h k A))).det = (indexedLaurentSeriesWronskian epsilonOrder (auxiliaryFamily u v h k)).det ∧ ↑(↑q * HahnSeries.order ((1 - u) / (1 - v))) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian epsilonOrder (auxiliaryFamily u v h k)).det

The same case-(i) endpoint for the source auxiliaryFamily, obtained by specializing rho = (1-u)/(1-v).