Determinant nondegeneracy turns multiplication bounds on a hyperplane complement into the product inequality used to control the largest successive minimum. This file contains the algebraic product step.

def CCDN.hyperplaneComplement {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (ℓ μ : K →ₗ[F] F) : Submodule F K

The intersection of the kernels of two linear functionals ℓ and μ on K.

Equations

• CCDN.hyperplaneComplement ℓ μ = ℓ.ker ⊓ μ.ker

theorem CCDN.hyperplane_multiplication_minimum_product {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {ι : Type u_3} [Fintype ι] (ℓ μ : K →ₗ[F] F) (hℓ : ℓ ≠ 0) (hℓ1 : ℓ 1 = 0) (hμ1 : μ 1 = 1) (b : Module.Basis ι F ↥(hyperplaneComplement ℓ μ)) (w : ι → ℝ) {M : ℝ} (hM : 0 ≤ M) (hw : ∀ (i j : ι), ℓ (↑(b i) * ↑(b j)) ≠ 0 → M ≤ w i * w j) : M ^ (Fintype.card ι + 2) ≤ (M * ∏ i : ι, w i) ^ 2

Let ℓ ≠ 0 and μ be linear functionals on K with ℓ 1 = 0 and μ 1 = 1, and let b be a basis of hyperplaneComplement ℓ μ with weights w. If M ≤ w i * w j whenever ℓ (b i * b j) ≠ 0, then M ^ (d + 2) ≤ (M * ∏ i, w i) ^ 2, where d is the size of the basis.