Indexing the auxiliary Wronskian family

Enumerate the auxiliary family and its derivative orders, then transport determinant nonvanishing through that indexing.

theorem BGS.CorvajaZannier.auxiliaryFamily_index_card (h k : ℕ) : Fintype.card (Fin k ⊕ Fin (k + 1) × Fin h) = h * k + h + k

The source auxiliary family has exactly h*k+h+k members.

noncomputable def BGS.CorvajaZannier.auxiliaryFamilyIndexEquiv (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h ≃ Fin (h * k + h + k)

A fixed enumeration of the auxiliary family by consecutive derivative orders.

Equations

• BGS.CorvajaZannier.auxiliaryFamilyIndexEquiv h k = Fintype.equivFinOfCardEq ⋯

noncomputable def BGS.CorvajaZannier.auxiliaryFamilyDerivativeOrder (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h → ℕ

The derivative order assigned to an auxiliary-family row.

Equations

• BGS.CorvajaZannier.auxiliaryFamilyDerivativeOrder h k i = ↑((BGS.CorvajaZannier.auxiliaryFamilyIndexEquiv h k) i)

theorem BGS.CorvajaZannier.auxiliaryFamilyDerivativeOrder_injective (h k : ℕ) : Function.Injective (auxiliaryFamilyDerivativeOrder h k)

theorem BGS.CorvajaZannier.auxiliaryFamilyDerivativeOrder_le_pred (h k : ℕ) (hn : 0 < h * k + h + k) (i : Fin k ⊕ Fin (k + 1) × Fin h) : auxiliaryFamilyDerivativeOrder h k i ≤ h * k + h + k - 1

theorem BGS.CorvajaZannier.auxiliaryFamilyDerivativeOrder_sum (h k : ℕ) : ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, auxiliaryFamilyDerivativeOrder h k i = (h * k + h + k).choose 2

theorem BGS.CorvajaZannier.auxiliaryFamily_k_le_card (h k : ℕ) : k ≤ h * k + h + k

theorem BGS.CorvajaZannier.indexedAuxiliaryWronskian_det_eq_derivationWronskian_det {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (D : Derivation C L L) (h k : ℕ) (f : Fin k ⊕ Fin (k + 1) × Fin h → L) : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) f).det = (Algebra.derivationWronskian D fun (j : Fin (h * k + h + k)) => f ((auxiliaryFamilyIndexEquiv h k).symm j)).det

Reindexing both rows and columns identifies the indexed consecutive-order Wronskian with the ordinary Fin n Wronskian.

theorem BGS.CorvajaZannier.indexedAuxiliaryWronskian_det_ne_zero_of_linearIndependent {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (D : Derivation C L L) (hconstants : ∀ (x : L), D x = 0 → ∃ (c : C), (algebraMap C L) c = x) (h k : ℕ) (f : Fin k ⊕ Fin (k + 1) × Fin h → L) (hLI : LinearIndependent C f) : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) f).det ≠ 0

Exact constants and linear independence make the indexed global Wronskian nonzero.