Lattice transference via reduced bases

This file was automatically generated by Codex.

The classical transference principle compares complementary successive minima of a full lattice and its Euclidean dual, with respect to a symmetric convex body and its polar. successiveMinimaProduct proves the lower bound one and an explicit nonsharp upper bound d * 16^d, hence (100*d)^(10*d), for every positive dimension. The formulation covers arbitrary finite-dimensional real inner-product spaces and compact symmetric convex bodies with nonempty interior. Its types, hypotheses, conclusions and local definitions use only Mathlib.

The proof develops integer basis extension, shortest-projection size reduction, primal and dual basis estimates, attainment of minima, and a maximum-determinant ellipsoid comparison, and the quantitative coefficient-box application.

Verified source: blueprint/formalization_blueprint.tex, lem:integer-basis (lines 257–263), lem:reduced-basis (lines 267–292), and lem:transference (lines 296–314). Background library references: pinned Mathlib.MeasureTheory.Group.GeometryOfNumbers (Blichfeldt and Minkowski's first theorem), and Mathlib.LinearAlgebra.BilinearForm.DualLattice (dual lattice and dual basis identities). The successive-minima product estimate is proved here, rather than imported from those modules.

def TrilinearHT.Auto.PrimitiveIntegerVector {d : ℕ} (v : Fin d → ℤ) : Prop

A primitive vector is one whose coordinates have gcd one.

Equations

• TrilinearHT.Auto.PrimitiveIntegerVector v = (Finset.univ.gcd v = 1)

theorem TrilinearHT.Auto.primitiveIntegerVector_isUnimodular {d : ℕ} (v : Fin d → ℤ) (hv : PrimitiveIntegerVector v) : Module.IsUnimodular ℤ v

noncomputable def TrilinearHT.Auto.integerFunctionalSplit {d : ℕ} (v : Fin d → ℤ) (f : (Fin d → ℤ) →ₗ[ℤ] ℤ) (hf : f v = 1) : (ℤ × ↥f.ker) ≃ₗ[ℤ] Fin d → ℤ

Splitting off a vector on which an integral linear functional takes value one.

Equations

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

theorem TrilinearHT.Auto.primitiveIntegerVector_extends_basis {d : ℕ} (v : Fin d → ℤ) (hv : PrimitiveIntegerVector v) : ∃ (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (i : Fin d), b i = v

Blueprint lem:integer-basis, primitive-vector assertion: every primitive vector belongs to an integer basis of ℤ^d.

def TrilinearHT.Auto.IntegerSaturated {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : Prop

Saturation in the integer lattice, as in lem:integer-basis.

Equations

• TrilinearHT.Auto.IntegerSaturated L = ∀ (n : ℤ), n ≠ 0 → ∀ (v : Fin d → ℤ), n • v ∈ L → v ∈ L

theorem TrilinearHT.Auto.integerSaturated_quotient_torsionFree {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) : Module.IsTorsionFree ℤ ((Fin d → ℤ) ⧸ L)

theorem TrilinearHT.Auto.integerSaturated_quotient_free {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) : Module.Free ℤ ((Fin d → ℤ) ⧸ L)

The quotient of a saturated integer subgroup is free.

noncomputable def TrilinearHT.Auto.integerQuotientSplit {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (s : (Fin d → ℤ) ⧸ L →ₗ[ℤ] Fin d → ℤ) (hs : L.mkQ ∘ₗ s = LinearMap.id) : (↥L × (Fin d → ℤ) ⧸ L) ≃ₗ[ℤ] Fin d → ℤ

A section of the quotient map splits an integer submodule from its quotient.

Equations

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

theorem TrilinearHT.Auto.saturatedAdaptedBasis {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) : ∃ r ≤ d, ∃ (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)), Submodule.span ℤ (⇑b '' {i : Fin d | ↑i < r}) = L

Blueprint lem:integer-basis: a saturated subgroup is spanned by an initial part of an integer basis.

def TrilinearHT.Auto.integerRationalMap (d : ℕ) : (Fin d → ℤ) →ₗ[ℤ] Fin d → ℚ

The coordinate inclusion of the integer lattice in its rational vector space.

Equations

• TrilinearHT.Auto.integerRationalMap d = { toFun := fun (v : Fin d → ℤ) (i : Fin d) => ↑(v i), map_add' := ⋯, map_smul' := ⋯ }

def TrilinearHT.Auto.rationalIntegerIntersection {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) : Submodule ℤ (Fin d → ℤ)

Integer points of a rational subspace.

Equations

• TrilinearHT.Auto.rationalIntegerIntersection V = Submodule.comap (TrilinearHT.Auto.integerRationalMap d) (Submodule.restrictScalars ℤ V)

theorem TrilinearHT.Auto.rationalIntegerIntersection_saturated {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) : IntegerSaturated (rationalIntegerIntersection V)

Blueprint lem:integer-basis, last assertion: integer points in a rational subspace form a saturated subgroup.

theorem TrilinearHT.Auto.lattice_bounded_inter_finite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {S : Set E} (hS : Bornology.IsBounded S) : (S ∩ ↑L).Finite

Blueprint lem:reduced-basis: bounded sets meet a discrete integer lattice in finitely many points.

theorem TrilinearHT.Auto.lattice_exists_shortest {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (hL : L ≠ ⊥) : ∃ v ∈ L, v ≠ 0 ∧ ∀ w ∈ L, w ≠ 0 → ‖v‖ ≤ ‖w‖

Blueprint lem:reduced-basis: every nonzero discrete lattice has a shortest nonzero vector.

theorem TrilinearHT.Auto.lattice_shortest_coordinates_primitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {d : ℕ} (b : Module.Basis (Fin d) ℤ ↥L) (v : ↥L) (hv : v ≠ 0) (hshort : ∀ (w : ↥L), w ≠ 0 → ‖↑v‖ ≤ ‖↑w‖) : PrimitiveIntegerVector (b.equivFun v)

A shortest nonzero lattice vector has primitive coordinates in every integer basis (lem:reduced-basis, first proof paragraph).

theorem TrilinearHT.Auto.lattice_shortest_extends_basis {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {d : ℕ} (b : Module.Basis (Fin d) ℤ ↥L) (v : ↥L) (hv : v ≠ 0) (hshort : ∀ (w : ↥L), w ≠ 0 → ‖↑v‖ ≤ ‖↑w‖) : ∃ (c : Module.Basis (Fin d) ℤ ↥L) (i : Fin d), c i = v

A shortest nonzero lattice vector belongs to an integer basis.

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.basisTailSpan {E : Type u_1} [AddCommGroup E] [Module ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : Submodule ℝ E

The span of all but the first vector of a finite basis.

Equations

• TrilinearHT.Auto.basisTailSpan b = Submodule.span ℝ (Set.range fun (i : Fin n) => b i.succ)

theorem TrilinearHT.Auto.basisTailSpan_isCompl {E : Type u_1} [AddCommGroup E] [Module ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : IsCompl (ℝ ∙ b 0) (basisTailSpan b)

noncomputable def TrilinearHT.Auto.basisTailOrthogonalEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : ↥(basisTailSpan b) ≃ₗ[ℝ] ↥(ℝ ∙ b 0)ᗮ

The tail-span complement is linearly equivalent to the perpendicular space by orthogonal projection.

Equations

• TrilinearHT.Auto.basisTailOrthogonalEquiv b = ((ℝ ∙ b 0).quotientEquivOfIsCompl (TrilinearHT.Auto.basisTailSpan b) ⋯).symm.trans (ℝ ∙ b 0).quotientEquivOrthogonal.toLinearEquiv

theorem TrilinearHT.Auto.basisTailOrthogonalEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (x : ↥(basisTailSpan b)) : (basisTailOrthogonalEquiv b) x = (ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto ↑x

noncomputable def TrilinearHT.Auto.projectedTailBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : Module.Basis (Fin n) ℝ ↥(ℝ ∙ b 0)ᗮ

The projected tail of a real basis is a basis of the perpendicular space.

Equations

• TrilinearHT.Auto.projectedTailBasis b = (Module.Basis.span ⋯).map (TrilinearHT.Auto.basisTailOrthogonalEquiv b)

theorem TrilinearHT.Auto.projectedTailBasis_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (i : Fin n) : (projectedTailBasis b) i = (ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto (b i.succ)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.projectedLattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : Submodule ℤ ↥(ℝ ∙ b 0)ᗮ

The full lattice generated by the projected tail basis.

Equations

• TrilinearHT.Auto.projectedLattice b = Submodule.span ℤ (Set.range ⇑(TrilinearHT.Auto.projectedTailBasis b))

theorem TrilinearHT.Auto.projectedLattice_eq_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : Submodule.map (↑ℤ ↑(ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto) (Submodule.span ℤ (Set.range ⇑b)) = projectedLattice b

Blueprint lem:reduced-basis: projecting off the first basis vector gives exactly the full lattice generated by the projected remaining vectors.

noncomputable def TrilinearHT.Auto.latticeLiftEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : (ℤ × ↥(projectedLattice b)) ≃ₗ[ℤ] ↥(Submodule.span ℤ (Set.range ⇑b))

Integer coordinates split into the first coordinate and the projected lattice.

Equations

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

theorem TrilinearHT.Auto.latticeLiftEquiv_coe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (a : ℤ) (x : ↥(projectedLattice b)) : ↑((latticeLiftEquiv b) (a, x)) = a • b 0 + ∑ i : Fin n, ((Module.Basis.restrictScalars ℤ (projectedTailBasis b)).repr x) i • b i.succ

theorem TrilinearHT.Auto.latticeLiftEquiv_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (a : ℤ) (x : ↥(projectedLattice b)) : (ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto ↑((latticeLiftEquiv b) (a, x)) = ↑x

def TrilinearHT.Auto.headTailIndex (n : ℕ) : Fin 1 ⊕ Fin n ≃ Fin (n + 1)

Identify a distinguished first coordinate and the remaining coordinates with Fin (n+1).

Equations

• TrilinearHT.Auto.headTailIndex n = finSumFinEquiv.trans (finCongr ⋯)

theorem TrilinearHT.Auto.headTailIndex_zero (n : ℕ) : (headTailIndex n) (Sum.inl 0) = 0

theorem TrilinearHT.Auto.headTailIndex_succ {n : ℕ} (i : Fin n) : (headTailIndex n) (Sum.inr i) = i.succ

noncomputable def TrilinearHT.Auto.liftedIntegerBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) : Module.Basis (Fin (n + 1)) ℤ ↥(Submodule.span ℤ (Set.range ⇑b))

Lift any integer basis of the projected lattice, keeping the original first vector.

Equations

• TrilinearHT.Auto.liftedIntegerBasis b c = (((Module.Basis.singleton (Fin 1) ℤ).prod c).map (TrilinearHT.Auto.latticeLiftEquiv b)).reindex (TrilinearHT.Auto.headTailIndex n)

theorem TrilinearHT.Auto.liftedIntegerBasis_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) : ↑((liftedIntegerBasis b c) 0) = b 0

theorem TrilinearHT.Auto.liftedIntegerBasis_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (i : Fin n) : (ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto ↑((liftedIntegerBasis b c) i.succ) = ↑(c i)

theorem TrilinearHT.Auto.exists_shortest_first_basis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) : ∃ (c : Module.Basis (Fin (n + 1)) ℝ E), Submodule.span ℤ (Set.range ⇑c) = Submodule.span ℤ (Set.range ⇑b) ∧ ∀ w ∈ Submodule.span ℤ (Set.range ⇑b), w ≠ 0 → ‖c 0‖ ≤ ‖w‖

Choose a lattice basis whose first vector is shortest nonzero.

@[reducible, inline]

abbrev TrilinearHT.Auto.basisPrefixSpan {E : Type u_1} [AddCommGroup E] [Module ℝ E] {n : ℕ} (f : Fin n → E) (i : Fin n) : Submodule ℝ E

The real span of the vectors preceding an index.

Equations

• TrilinearHT.Auto.basisPrefixSpan f i = Submodule.span ℝ (f '' Set.Iio i)

noncomputable def TrilinearHT.Auto.basisRemainder {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin n → E) (i : Fin n) : E →L[ℝ] E

Orthogonal projection off the preceding vectors.

Equations

• TrilinearHT.Auto.basisRemainder f i = (TrilinearHT.Auto.basisPrefixSpan f i)ᗮ.starProjection

theorem TrilinearHT.Auto.gramSchmidt_eq_basisRemainder {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin n → E) (i : Fin n) : InnerProductSpace.gramSchmidt ℝ f i = (basisRemainder f i) (f i)

def TrilinearHT.Auto.IsShortestProjectionBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : Prop

Every Gram–Schmidt vector is shortest nonzero in its projected lattice.

Equations

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

theorem TrilinearHT.Auto.starProjection_sup_subtype {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (P : Submodule ℝ E) (S : Submodule ℝ ↥Pᗮ) (x : E) : (P ⊔ Submodule.map Pᗮ.subtype S)ᗮ.starProjection x = ↑(Sᗮ.starProjection (Pᗮ.orthogonalProjectionOnto x))

Projecting off a subspace and then off a subspace of its perpendicular space agrees with the corresponding single orthogonal projection.

theorem TrilinearHT.Auto.basisPrefixSpan_succ {E : Type u_1} [AddCommGroup E] [Module ℝ E] {n : ℕ} (f : Fin (n + 1) → E) (i : Fin n) : basisPrefixSpan f i.succ = ℝ ∙ f 0 ⊔ basisPrefixSpan (fun (j : Fin n) => f j.succ) i

theorem TrilinearHT.Auto.sup_eq_sup_projected {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (P R : Submodule ℝ E) : P ⊔ R = P ⊔ Submodule.map Pᗮ.subtype (Submodule.map (↑Pᗮ.orthogonalProjectionOnto) R)

theorem TrilinearHT.Auto.basisRemainder_succ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin (n + 1) → E) (P : Submodule ℝ E) (hP : ℝ ∙ f 0 = P) (i : Fin n) (x : E) : (basisRemainder f i.succ) x = ↑((basisRemainder (fun (j : Fin n) => Pᗮ.orthogonalProjectionOnto (f j.succ)) i) (Pᗮ.orthogonalProjectionOnto x))

@[simp]

theorem TrilinearHT.Auto.basisRemainder_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin (n + 1) → E) (x : E) : (basisRemainder f 0) x = x

theorem TrilinearHT.Auto.exists_shortestProjectionBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : ∃ (c : Module.Basis (Fin n) ℝ E), Submodule.span ℤ (Set.range ⇑c) = Submodule.span ℤ (Set.range ⇑b) ∧ IsShortestProjectionBasis c

Blueprint lem:reduced-basis, shortest-projection construction before size reduction: every full lattice admits a basis shortest at every projection stage.

def TrilinearHT.Auto.integerUpperShear {M : Type u_1} [AddCommGroup M] (f : M →ₗ[ℤ] ℤ) : (ℤ × M) ≃ₗ[ℤ] ℤ × M

An integral shear subtracting a linear functional from the first coordinate.

Equations

• TrilinearHT.Auto.integerUpperShear f = LinearEquiv.prodComm ℤ ℤ M ≪≫ₗ (LinearEquiv.refl ℤ M).skewProd (LinearEquiv.refl ℤ ℤ) (-f) ≪≫ₗ LinearEquiv.prodComm ℤ M ℤ

@[simp]

theorem TrilinearHT.Auto.integerUpperShear_apply {M : Type u_1} [AddCommGroup M] (f : M →ₗ[ℤ] ℤ) (a : ℤ) (x : M) : (integerUpperShear f) (a, x) = (a - f x, x)

noncomputable def TrilinearHT.Auto.shiftedLatticeLiftEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (k : Fin n → ℤ) : (ℤ × ↥(projectedLattice b)) ≃ₗ[ℤ] ↥(Submodule.span ℤ (Set.range ⇑b))

Integer lattice-lift equivalence after an integral upper shear.

Equations

• TrilinearHT.Auto.shiftedLatticeLiftEquiv b c k = TrilinearHT.Auto.integerUpperShear ((c.constr ℤ) k) ≪≫ₗ TrilinearHT.Auto.latticeLiftEquiv b

noncomputable def TrilinearHT.Auto.shiftedIntegerBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (k : Fin n → ℤ) : Module.Basis (Fin (n + 1)) ℤ ↥(Submodule.span ℤ (Set.range ⇑b))

Integral changes of the first coefficients of the lifted basis.

Equations

• TrilinearHT.Auto.shiftedIntegerBasis b c k = (((Module.Basis.singleton (Fin 1) ℤ).prod c).map (TrilinearHT.Auto.shiftedLatticeLiftEquiv b c k)).reindex (TrilinearHT.Auto.headTailIndex n)

theorem TrilinearHT.Auto.shiftedIntegerBasis_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (k : Fin n → ℤ) : ↑((shiftedIntegerBasis b c k) 0) = b 0

theorem TrilinearHT.Auto.shiftedIntegerBasis_succ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (k : Fin n → ℤ) (i : Fin n) : ↑((shiftedIntegerBasis b c k) i.succ) = ↑((liftedIntegerBasis b c) i.succ) - k i • b 0

theorem TrilinearHT.Auto.shiftedIntegerBasis_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (k : Fin n → ℤ) (i : Fin n) : (ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto ↑((shiftedIntegerBasis b c k) i.succ) = ↑(c i)

noncomputable def TrilinearHT.Auto.gramCoefficient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (f : Fin n → E) (i j : Fin n) : ℝ

The Gram–Schmidt coefficient used in the size-reduction step.

Equations

• TrilinearHT.Auto.gramCoefficient f i j = inner ℝ (InnerProductSpace.gramSchmidt ℝ f i) (f j) / ‖InnerProductSpace.gramSchmidt ℝ f i‖ ^ 2

def TrilinearHT.Auto.IsSizeReducedBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : Prop

A basis whose earlier Gram–Schmidt coefficients have absolute value at most one half.

Equations

• TrilinearHT.Auto.IsSizeReducedBasis b = ∀ (i j : Fin n), i < j → |TrilinearHT.Auto.gramCoefficient (⇑b) i j| ≤ 1 / 2

theorem TrilinearHT.Auto.gramSchmidt_succ_of_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin (n + 1) → E) (P : Submodule ℝ E) (hP : ℝ ∙ f 0 = P) (g : Fin n → ↥Pᗮ) (hg : ∀ (j : Fin n), Pᗮ.orthogonalProjectionOnto (f j.succ) = g j) (i : Fin n) : InnerProductSpace.gramSchmidt ℝ f i.succ = ↑(InnerProductSpace.gramSchmidt ℝ g i)

theorem TrilinearHT.Auto.gramCoefficient_succ_of_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin (n + 1) → E) (P : Submodule ℝ E) (hP : ℝ ∙ f 0 = P) (g : Fin n → ↥Pᗮ) (hg : ∀ (j : Fin n), Pᗮ.orthogonalProjectionOnto (f j.succ) = g j) (i j : Fin n) : gramCoefficient f i.succ j.succ = gramCoefficient g i j

noncomputable def TrilinearHT.Auto.roundedLiftShift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (i : Fin n) : ℤ

Nearest integer coefficient used to reduce a lifted basis vector along the first vector.

Equations

• TrilinearHT.Auto.roundedLiftShift b c i = round (inner ℝ (b 0) ↑((TrilinearHT.Auto.liftedIntegerBasis b c) i.succ) / ‖b 0‖ ^ 2)

noncomputable def TrilinearHT.Auto.roundedLiftBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) : Module.Basis (Fin (n + 1)) ℝ E

Lift a projected lattice basis and reduce its first Gram–Schmidt coefficients by subtracting nearest integer multiples of the first vector.

Equations

• TrilinearHT.Auto.roundedLiftBasis b c = Module.Basis.ofZLatticeBasis ℝ (Submodule.span ℤ (Set.range ⇑b)) (TrilinearHT.Auto.shiftedIntegerBasis b c (TrilinearHT.Auto.roundedLiftShift b c))

theorem TrilinearHT.Auto.roundedLiftBasis_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) : Submodule.span ℤ (Set.range ⇑(roundedLiftBasis b c)) = Submodule.span ℤ (Set.range ⇑b)

theorem TrilinearHT.Auto.roundedLiftBasis_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) : (roundedLiftBasis b c) 0 = b 0

theorem TrilinearHT.Auto.roundedLiftBasis_projection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (i : Fin n) : (ℝ ∙ b 0)ᗮ.orthogonalProjectionOnto ((roundedLiftBasis b c) i.succ) = ↑(c i)

theorem TrilinearHT.Auto.roundedLiftBasis_coefficient_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (c : Module.Basis (Fin n) ℤ ↥(projectedLattice b)) (i : Fin n) : |gramCoefficient (⇑(roundedLiftBasis b c)) 0 i.succ| ≤ 1 / 2

theorem TrilinearHT.Auto.projectedTailBasis_isShortest {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (hb : IsShortestProjectionBasis b) : IsShortestProjectionBasis (projectedTailBasis b)

theorem TrilinearHT.Auto.exists_sizeReducedShortestBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) : ∃ (c : Module.Basis (Fin n) ℝ E), Submodule.span ℤ (Set.range ⇑c) = Submodule.span ℤ (Set.range ⇑b) ∧ IsShortestProjectionBasis c ∧ IsSizeReducedBasis c

Recursive integer size reduction retains shortestness in every projected lattice and places all earlier Gram–Schmidt coefficients in [-1/2,1/2].

theorem TrilinearHT.Auto.exists_reducedShortestProjectionBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : ∃ (c : Module.Basis (Fin n) ℝ E), Submodule.span ℤ (Set.range ⇑c) = Submodule.span ℤ (Set.range ⇑b) ∧ IsShortestProjectionBasis c ∧ IsSizeReducedBasis c

Blueprint lem:reduced-basis: existence of a size-reduced shortest-projection basis, before the quantitative primal and dual norm estimates.

theorem TrilinearHT.Auto.basisRemainder_gramSchmidt_of_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin n → E) {i k : Fin n} (hki : k < i) : (basisRemainder f i) (InnerProductSpace.gramSchmidt ℝ f k) = 0

theorem TrilinearHT.Auto.basisRemainder_gramSchmidt_of_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin n → E) {i k : Fin n} (hik : i ≤ k) : (basisRemainder f i) (InnerProductSpace.gramSchmidt ℝ f k) = InnerProductSpace.gramSchmidt ℝ f k

theorem TrilinearHT.Auto.basisRemainder_next {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin (n + 1) → E) (i : Fin n) : (basisRemainder f i.castSucc) (f i.succ) = InnerProductSpace.gramSchmidt ℝ f i.succ + gramCoefficient f i.castSucc i.succ • InnerProductSpace.gramSchmidt ℝ f i.castSucc

theorem TrilinearHT.Auto.reducedBasis_adjacent_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (i : Fin n) : 3 / 4 * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i.castSucc‖ ^ 2 ≤ ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i.succ‖ ^ 2

Blueprint lem:reduced-basis: shortness in the projected lattice and size reduction imply the squared adjacent Gram–Schmidt length bound.

theorem TrilinearHT.Auto.norm_sq_sum_of_pairwise_orthogonal {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Finset ι) (f : ι → E) (hf : Pairwise fun (i j : ι) => inner ℝ (f i) (f j) = 0) : ‖∑ i ∈ s, f i‖ ^ 2 = ∑ i ∈ s, ‖f i‖ ^ 2

theorem TrilinearHT.Auto.basis_norm_sq_gramSchmidt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (f : Fin n → E) (j : Fin n) : ‖f j‖ ^ 2 = ‖InnerProductSpace.gramSchmidt ℝ f j‖ ^ 2 + ∑ i < j, gramCoefficient f i j ^ 2 * ‖InnerProductSpace.gramSchmidt ℝ f i‖ ^ 2

theorem TrilinearHT.Auto.adjacent_prefix_sum_bound {n : ℕ} (a : Fin (n + 1) → ℝ) (hadj : ∀ (i : Fin n), 3 / 4 * a i.castSucc ≤ a i.succ) (j : Fin (n + 1)) : ∑ i < j, a i ≤ 4 * ((4 / 3) ^ ↑j - 1) * a j

The finite geometric majorant for squared Gram–Schmidt lengths in the primal norm estimate of lem:reduced-basis.

theorem TrilinearHT.Auto.reducedBasis_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (j : Fin n) : ‖b j‖ ^ 2 ≤ (4 / 3) ^ ↑j * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖ ^ 2

Blueprint lem:reduced-basis: the squared primal norm estimate.

theorem TrilinearHT.Auto.reducedBasis_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (j : Fin n) : ‖b j‖ ≤ (2 / √3) ^ ↑j * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖

Blueprint lem:reduced-basis: with zero-based indices, ‖bⱼ‖ ≤ (2 / √3)^j ‖bⱼ*‖.

noncomputable def TrilinearHT.Auto.inverseGramCoefficient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i j : Fin n) : ℝ

Coordinates of the Gram–Schmidt vectors in the original basis: these are the entries of the inverse unit upper triangular matrix in lem:reduced-basis.

Equations

• TrilinearHT.Auto.inverseGramCoefficient b i j = (b.repr (InnerProductSpace.gramSchmidt ℝ (⇑b) j)) i

theorem TrilinearHT.Auto.inverseGramCoefficient_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {i j : Fin n} (hji : j < i) : inverseGramCoefficient b i j = 0

theorem TrilinearHT.Auto.inverseGramCoefficient_recurrence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i j : Fin n) : inverseGramCoefficient b i j = (if i = j then 1 else 0) - ∑ k < j, gramCoefficient (⇑b) k j * inverseGramCoefficient b i k

theorem TrilinearHT.Auto.inverseGramCoefficient_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i : Fin n) : inverseGramCoefficient b i i = 1

theorem TrilinearHT.Auto.inverseGramCoefficient_abs_recurrence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsSizeReducedBasis b) {i j : Fin n} (hij : i < j) : |inverseGramCoefficient b i j| ≤ 1 / 2 * ∑ k < j, |inverseGramCoefficient b i k|

theorem TrilinearHT.Auto.triangular_prefix_bound {n : ℕ} (a : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (hzero : ∀ k < i, a k = 0) (hself : a i = 1) (hrec : ∀ (j : Fin (n + 1)), i < j → a j ≤ 1 / 2 * ∑ k < j, a k) (j : Fin (n + 1)) (hij : i ≤ j) : ∑ k ≤ j, a k ≤ (3 / 2) ^ (↑j - ↑i)

A triangular recurrence with off-diagonal coefficients bounded by one half has geometric prefix sums bounded by powers of three halves.

theorem TrilinearHT.Auto.inverseGramCoefficient_abs_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsSizeReducedBasis b) {i j : Fin n} (hij : i < j) : |inverseGramCoefficient b i j| ≤ 1 / 2 * (3 / 2) ^ (↑j - ↑i - 1)

The upper triangular inverse bound in lem:reduced-basis, obtained by the equivalent forward substitution recurrence.

theorem TrilinearHT.Auto.adjacent_chain_bound {n : ℕ} (a : Fin (n + 1) → ℝ) (r : ℝ) (hr : 0 ≤ r) (ha : ∀ (k : Fin n), a k.castSucc ≤ r * a k.succ) (i j : Fin (n + 1)) (hij : i ≤ j) : a i ≤ r ^ (↑j - ↑i) * a j

theorem TrilinearHT.Auto.reducedBasis_length_ratio_coarse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) {i j : Fin n} (hij : i ≤ j) : ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i‖ ≤ (4 / 3) ^ (↑j - ↑i) * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖

theorem TrilinearHT.Auto.inverseGramCoefficient_abs_coarse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsSizeReducedBasis b) {i j : Fin n} (hij : i ≤ j) : |inverseGramCoefficient b i j| ≤ (3 / 2) ^ (↑j - ↑i)

theorem TrilinearHT.Auto.reducedBasis_weighted_inverse_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (i j : Fin n) : ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i‖ * |inverseGramCoefficient b i j| ≤ 2 ^ n * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖

noncomputable def TrilinearHT.Auto.euclideanDualBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : Module.Basis (Fin n) ℝ E

Euclidean dual basis, obtained from the algebraic dual basis by Riesz duality.

Equations

• TrilinearHT.Auto.euclideanDualBasis b = b.dualBasis.map (LinearMap.toContinuousLinearMap.trans (InnerProductSpace.toDual ℝ E).symm.toLinearEquiv)

theorem TrilinearHT.Auto.euclideanDualBasis_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i : Fin n) (x : E) : inner ℝ ((euclideanDualBasis b) i) x = (b.repr x) i

theorem TrilinearHT.Auto.gramSchmidtBasis_coordinate_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (x : E) (j : Fin n) : |((InnerProductSpace.gramSchmidtBasis b).repr x) j| * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖ ≤ ‖x‖

theorem TrilinearHT.Auto.reducedBasis_coordinate_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (i : Fin n) (x : E) : ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i‖ * |(b.repr x) i| ≤ 4 ^ n * ‖x‖

The coordinate functional bound implying the dual-vector estimate in lem:reduced-basis.

theorem TrilinearHT.Auto.reducedBasis_dual_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (i : Fin n) : ‖(euclideanDualBasis b) i‖ ≤ 4 ^ n / ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i‖

Blueprint lem:reduced-basis: the Euclidean dual basis satisfies ‖qᵢ‖ ≤ 4^d / aᵢ.

theorem TrilinearHT.Auto.euclideanDualBasis_inner_basis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i j : Fin n) : inner ℝ ((euclideanDualBasis b) i) (b j) = if i = j then 1 else 0

noncomputable def TrilinearHT.Auto.euclideanDualLattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : Submodule ℤ E

The integer dual with respect to the Euclidean inner product.

Equations

• TrilinearHT.Auto.euclideanDualLattice L = LinearMap.BilinForm.dualSubmodule (innerₗ E) L

theorem TrilinearHT.Auto.mem_euclideanDualLattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (x : E) : x ∈ euclideanDualLattice L ↔ ∀ y ∈ L, ∃ (m : ℤ), ↑m = inner ℝ x y

theorem TrilinearHT.Auto.euclideanInner_nondegenerate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : (innerₗ E).Nondegenerate

theorem TrilinearHT.Auto.euclideanDualBasis_eq_bilinDual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : LinearMap.BilinForm.dualBasis (innerₗ E) ⋯ b = euclideanDualBasis b

theorem TrilinearHT.Auto.euclideanDualLattice_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : euclideanDualLattice (Submodule.span ℤ (Set.range ⇑b)) = Submodule.span ℤ (Set.range ⇑(euclideanDualBasis b))

Blueprint lem:transference: the integer dual lattice is generated by the Euclidean dual basis, hence is again a full lattice.

structure TrilinearHT.Auto.IsSymmetricConvexBody {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) : Prop

The compact, origin-symmetric convex bodies used in blueprint lem:transference; the interior is required to be nonempty.

• compact : IsCompact K
• convex : Convex ℝ K
• neg_mem (x : E) : x ∈ K → -x ∈ K
• interior_nonempty : (interior K).Nonempty

theorem TrilinearHT.Auto.symmetricConvexBody_zero_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) : 0 ∈ interior K

theorem TrilinearHT.Auto.symmetricConvexBody_gauge_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {x : E} (hx : x ≠ 0) : 0 < gauge K x

theorem TrilinearHT.Auto.symmetricConvexBody_gauge_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (x : E) : gauge K x ≤ 1 ↔ x ∈ K

theorem TrilinearHT.Auto.symmetricConvexBody_gauge_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (x : E) {t : ℝ} (ht : 0 < t) : gauge K x ≤ t ↔ x ∈ t • K

Positive gauge sublevel sets are exactly dilates of the original body.

theorem TrilinearHT.Auto.symmetricConvexBody_gauge_sublevel_compact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {t : ℝ} (ht : 0 < t) : IsCompact {x : E | gauge K x ≤ t}

noncomputable def TrilinearHT.Auto.euclideanPolar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) : Set E

The absolute Euclidean polar from blueprint lem:transference.

Equations

• TrilinearHT.Auto.euclideanPolar K = (innerₗ E).polar K

theorem TrilinearHT.Auto.mem_euclideanPolar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) (y : E) : y ∈ euclideanPolar K ↔ ∀ x ∈ K, |inner ℝ x y| ≤ 1

theorem TrilinearHT.Auto.euclideanPolar_closed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) : IsClosed (euclideanPolar K)

theorem TrilinearHT.Auto.euclideanPolar_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) : Convex ℝ (euclideanPolar K)

theorem TrilinearHT.Auto.euclideanPolar_bounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : K ∈ nhds 0) : Bornology.IsBounded (euclideanPolar K)

theorem TrilinearHT.Auto.euclideanPolar_zero_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : Bornology.IsBounded K) : 0 ∈ interior (euclideanPolar K)

theorem TrilinearHT.Auto.symmetricConvexBody_polar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) : IsSymmetricConvexBody (euclideanPolar K)

The polar again satisfies all convex-body hypotheses needed to define and attain its successive minima.

noncomputable def TrilinearHT.Auto.latticeTupleRadius {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {j : ℕ} (K : Set E) (v : Fin j → E) : ℝ

The least nonnegative gauge radius containing a finite tuple.

Equations

• TrilinearHT.Auto.latticeTupleRadius K v = ↑(Finset.univ.sup fun (i : Fin j) => ⟨gauge K (v i), ⋯⟩)

theorem TrilinearHT.Auto.latticeTupleRadius_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {j : ℕ} (K : Set E) (v : Fin j → E) : 0 ≤ latticeTupleRadius K v

theorem TrilinearHT.Auto.gauge_le_latticeTupleRadius {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {j : ℕ} (K : Set E) (v : Fin j → E) (i : Fin j) : gauge K (v i) ≤ latticeTupleRadius K v

theorem TrilinearHT.Auto.latticeTupleRadius_le_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {j : ℕ} (K : Set E) (v : Fin j → E) {r : ℝ} (hr : 0 ≤ r) : latticeTupleRadius K v ≤ r ↔ ∀ (i : Fin j), gauge K (v i) ≤ r

def TrilinearHT.Auto.IndependentLatticeTuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {j : ℕ} (v : Fin j → E) : Prop

Independent lattice tuples are the witnesses in the successive-minimum definition.

Equations

• TrilinearHT.Auto.IndependentLatticeTuple L v = (LinearIndependent ℝ v ∧ ∀ (i : Fin j), v i ∈ L)

theorem TrilinearHT.Auto.exists_minimal_lattice_tuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (L : Submodule ℤ E) [DiscreteTopology ↥L] {j : ℕ} (v : Fin j → E) (hv : IndependentLatticeTuple L v) : ∃ (w : Fin j → E), IndependentLatticeTuple L w ∧ ∀ (u : Fin j → E), IndependentLatticeTuple L u → latticeTupleRadius K w ≤ latticeTupleRadius K u

Blueprint lem:transference, line 305: among independent tuples of a fixed length, a tuple of least gauge radius exists as soon as one tuple exists.

def TrilinearHT.Auto.successiveDilationSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) (L : Submodule ℤ E) (j : ℕ) : Set ℝ

The dilation parameters containing j real-linearly independent lattice vectors, exactly as in blueprint lem:transference.

Equations

• TrilinearHT.Auto.successiveDilationSet K L j = {t : ℝ | 0 < t ∧ ∃ (v : Fin j → E), TrilinearHT.Auto.IndependentLatticeTuple L v ∧ ∀ (i : Fin j), v i ∈ t • K}

noncomputable def TrilinearHT.Auto.successiveMinimum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) (L : Submodule ℤ E) (j : ℕ) : ℝ

The jth successive minimum of the body K and lattice L.

Equations

• TrilinearHT.Auto.successiveMinimum K L j = sInf (TrilinearHT.Auto.successiveDilationSet K L j)

theorem TrilinearHT.Auto.successiveDilationSet_bddBelow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) (L : Submodule ℤ E) (j : ℕ) : BddBelow (successiveDilationSet K L j)

theorem TrilinearHT.Auto.successiveMinimum_le_of_tuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {L : Submodule ℤ E} {j : ℕ} {t : ℝ} (ht : 0 < t) (v : Fin j → E) (hv : IndependentLatticeTuple L v) (hmem : ∀ (i : Fin j), v i ∈ t • K) : successiveMinimum K L j ≤ t

theorem TrilinearHT.Auto.successiveMinimum_attained_of_tuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (L : Submodule ℤ E) [DiscreteTopology ↥L] {j : ℕ} (hj : 0 < j) (v : Fin j → E) (hv : IndependentLatticeTuple L v) : 0 < successiveMinimum K L j ∧ ∃ (w : Fin j → E), IndependentLatticeTuple L w ∧ ∀ (i : Fin j), w i ∈ successiveMinimum K L j • K

Blueprint lem:transference, line 305: the positive successive minimum is attained by an independent tuple whenever a tuple of that length exists.

theorem TrilinearHT.Auto.successiveMinimum_attained {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {j : ℕ} (hj : 0 < j) (hjn : j ≤ n) : 0 < successiveMinimum K (Submodule.span ℤ (Set.range ⇑b)) j ∧ ∃ (w : Fin j → E), IndependentLatticeTuple (Submodule.span ℤ (Set.range ⇑b)) w ∧ ∀ (i : Fin j), w i ∈ successiveMinimum K (Submodule.span ℤ (Set.range ⇑b)) j • K

Every admissible initial segment of a lattice basis supplies an independent tuple, so all successive minima from one through the dimension are attained.

theorem TrilinearHT.Auto.inner_le_of_mem_dilate_polar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) {x y : E} (hx : x ∈ a • K) (hy : y ∈ b • euclideanPolar K) : |inner ℝ x y| ≤ a * b

theorem TrilinearHT.Auto.unitBall_symmetricConvexBody {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : IsSymmetricConvexBody (Metric.closedBall 0 1)

theorem TrilinearHT.Auto.reducedBasis_length_ratio_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) {i j : Fin n} (hij : i ≤ j) : ‖InnerProductSpace.gramSchmidt ℝ (⇑b) i‖ ≤ 2 ^ (↑j - ↑i) * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖

theorem TrilinearHT.Auto.reducedBasis_primal_prefix_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) {i j : Fin n} (hij : i ≤ j) : ‖b i‖ ≤ 2 ^ n * ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖

theorem TrilinearHT.Auto.reducedBasis_dual_suffix_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) {i j : Fin n} (hij : j ≤ i) : ‖(euclideanDualBasis b) i‖ ≤ 8 ^ n / ‖InnerProductSpace.gramSchmidt ℝ (⇑b) j‖

theorem TrilinearHT.Auto.successiveMinimum_ball_product_upper {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {j : ℕ} (hj : 0 < j) (hjn : j ≤ n) : successiveMinimum (Metric.closedBall 0 1) (Submodule.span ℤ (Set.range ⇑b)) j * successiveMinimum (Metric.closedBall 0 1) (euclideanDualLattice (Submodule.span ℤ (Set.range ⇑b))) (n + 1 - j) ≤ 16 ^ n

Blueprint lem:transference, line 307: for the Euclidean unit ball the product of complementary successive minima is bounded by 16^d.

theorem TrilinearHT.Auto.symmetricConvexBody_exists_basis_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : ∃ (c : Module.Basis (Fin n) ℝ E), ∀ (i : Fin n), c i ∈ K

theorem TrilinearHT.Auto.symmetricConvexBody_maxDetBasis {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : ∃ (c : Module.Basis (Fin n) ℝ E), (∀ (i : Fin n), c i ∈ K) ∧ (∀ (v : Fin n → E), (∀ (i : Fin n), v i ∈ K) → |b.det v| ≤ |b.det ⇑c|) ∧ ∀ x ∈ K, ∀ (i : Fin n), |(c.repr x) i| ≤ 1

Blueprint lem:transference, line 309: a maximum-determinant basis has all its vectors in the body and all coordinates of body points bounded by one.

theorem TrilinearHT.Auto.symmetricConvexBody_gauge_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {x : E} (hx : x ∈ K) (r : ℝ) : gauge K (r • x) ≤ |r|

theorem TrilinearHT.Auto.symmetricConvexBody_sum_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (v : Fin n → E) (hv : ∀ (i : Fin n), v i ∈ K) (u : Fin n → ℝ) (hu : ∑ i : Fin n, |u i| ≤ 1) : ∑ i : Fin n, u i • v i ∈ K

The image of the coefficient ℓ1 unit ball lies in the body whenever the basis vectors lie in the body (blueprint lem:transference, line 309).

noncomputable def TrilinearHT.Auto.basisEuclideanEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : E ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n)

Coordinates in a basis, with the Euclidean rather than supremum norm.

Equations

• TrilinearHT.Auto.basisEuclideanEquiv b = b.equivFun ≪≫ₗ (WithLp.linearEquiv 2 ℝ (Fin n → ℝ)).symm

@[simp]

theorem TrilinearHT.Auto.basisEuclideanEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (x : E) (i : Fin n) : ((basisEuclideanEquiv b) x).ofLp i = (b.repr x) i

theorem TrilinearHT.Auto.euclidean_sum_abs_le {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ∑ i : Fin n, |x.ofLp i| ≤ √↑n * ‖x‖

theorem TrilinearHT.Auto.basisEuclideanEquiv_norm_le_sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (x : E) (hx : ∀ (i : Fin n), |(b.repr x) i| ≤ 1) : ‖(basisEuclideanEquiv b) x‖ ≤ √↑n

theorem TrilinearHT.Auto.symmetricConvexBody_mem_of_coordinate_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) (hb : ∀ (i : Fin n), b i ∈ K) (x : E) (hx : ‖(basisEuclideanEquiv b) x‖ ≤ (√↑n)⁻¹) : x ∈ K

def TrilinearHT.Auto.basisEllipsoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : Set E

The ellipsoid obtained by mapping the Euclidean unit ball through a basis.

Equations

• TrilinearHT.Auto.basisEllipsoid b = {x : E | ‖(TrilinearHT.Auto.basisEuclideanEquiv b) x‖ ≤ 1}

theorem TrilinearHT.Auto.mem_smul_basisEllipsoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (x : E) {t : ℝ} (ht : 0 < t) : x ∈ t • basisEllipsoid b ↔ ‖(basisEuclideanEquiv b) x‖ ≤ t

theorem TrilinearHT.Auto.euclideanPolar_antitone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K H : Set E} (h : K ⊆ H) : euclideanPolar H ⊆ euclideanPolar K

theorem TrilinearHT.Auto.euclideanPolar_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) {t : ℝ} (ht : 0 < t) : euclideanPolar (t • K) = t⁻¹ • euclideanPolar K

theorem TrilinearHT.Auto.symmetricConvexBody_ellipsoidComparison {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) : ∃ (c : Module.Basis (Fin n) ℝ E), (√↑n)⁻¹ • basisEllipsoid c ⊆ K ∧ K ⊆ √↑n • basisEllipsoid c ∧ (√↑n)⁻¹ • euclideanPolar (basisEllipsoid c) ⊆ euclideanPolar K ∧ euclideanPolar K ⊆ √↑n • euclideanPolar (basisEllipsoid c)

Blueprint lem:transference, lines 309–313: a maximum-determinant ellipsoid and its polar approximate the body and its polar within √d.

noncomputable def TrilinearHT.Auto.euclideanAdjointEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (A : E ≃ₗ[ℝ] F) : F ≃ₗ[ℝ] E

The transpose of an invertible real map, bundled as an equivalence.

Equations

• TrilinearHT.Auto.euclideanAdjointEquiv A = { toLinearMap := LinearMap.adjoint ↑A, invFun := ⇑(LinearMap.adjoint ↑A.symm), left_inv := ⋯, right_inv := ⋯ }

theorem TrilinearHT.Auto.euclideanAdjointEquiv_inner {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (A : E ≃ₗ[ℝ] F) (x : E) (y : F) : inner ℝ x ((euclideanAdjointEquiv A) y) = inner ℝ (A x) y

theorem TrilinearHT.Auto.basis_map_span_mem_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (A : E ≃ₗ[ℝ] F) (x : F) : x ∈ Submodule.span ℤ (Set.range ⇑(b.map A)) ↔ A.symm x ∈ Submodule.span ℤ (Set.range ⇑b)

theorem TrilinearHT.Auto.adjoint_mem_dual_lattice {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (A : E ≃ₗ[ℝ] F) {y : F} (hy : y ∈ euclideanDualLattice (Submodule.span ℤ (Set.range ⇑(b.map A)))) : (euclideanAdjointEquiv A) y ∈ euclideanDualLattice (Submodule.span ℤ (Set.range ⇑b))

theorem TrilinearHT.Auto.successiveMinimum_le_transport {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {K : Set E} {H : Set F} (hH : IsSymmetricConvexBody H) {n : ℕ} (b : Module.Basis (Fin n) ℝ F) (T : F ≃ₗ[ℝ] E) (L : Submodule ℤ E) (hL : ∀ x ∈ Submodule.span ℤ (Set.range ⇑b), T x ∈ L) {c : ℝ} (hc : 0 < c) (hcover : ∀ x ∈ H, T x ∈ c • K) {j : ℕ} (hj : 0 < j) (hjn : j ≤ n) : successiveMinimum K L j ≤ c * successiveMinimum H (Submodule.span ℤ (Set.range ⇑b)) j

Transport an attained minimum through an invertible linear map when the image of the source body lies in a fixed dilation of the target body.

theorem TrilinearHT.Auto.mem_smul_of_inv_smul_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K H : Set E} {r : ℝ} (hr : r ≠ 0) (h : r⁻¹ • H ⊆ K) {x : E} (hx : x ∈ H) : x ∈ r • K

theorem TrilinearHT.Auto.adjoint_unitBall_mem_polar_ellipsoid {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ Metric.closedBall 0 1) : (euclideanAdjointEquiv (basisEuclideanEquiv b)) y ∈ euclideanPolar (basisEllipsoid b)

A unit vector, transported by the transpose coordinate map, belongs to the polar of the corresponding ellipsoid.

theorem TrilinearHT.Auto.successiveMinimum_product_upper {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {j : ℕ} (hj : 0 < j) (hjn : j ≤ n) : successiveMinimum K (Submodule.span ℤ (Set.range ⇑b)) j * successiveMinimum (euclideanPolar K) (euclideanDualLattice (Submodule.span ℤ (Set.range ⇑b))) (n + 1 - j) ≤ ↑n * 16 ^ n

Blueprint lem:transference, line 314: general symmetric convex bodies satisfy the upper complementary-minima bound d * 16^d.

theorem TrilinearHT.Auto.transference_constant_bound {n : ℕ} (hn : 0 < n) : ↑n * 16 ^ n ≤ (100 * ↑n) ^ (10 * n)