Maximal independent thin directions

Fibre-constant affine functionals form a submodule containing all constants. A greedy extension by thin functionals therefore stops after at most d steps. The selected directions have the prescribed stage-dependent widths, and every direction outside the final submodule is thick at the next stage.

def EGZ.FpRepresentation.fiberConstantSubmodule {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)

Affine functionals constant on every fibre inside the represented space.

Equations

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

theorem EGZ.FpRepresentation.mem_fiberConstantSubmodule_iff {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) : ξ ∈ R.fiberConstantSubmodule x ↔ ¬R.NonconstantOnFibers x ξ

theorem EGZ.FpRepresentation.const_mem_fiberConstantSubmodule {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) (c : ZMod p) : AffineMap.const (ZMod p) (FpCoord p d) c ∈ R.fiberConstantSubmodule x

theorem EGZ.FpRepresentation.finrank_affineFunctionals {p d : ℕ} [Fact (Nat.Prime p)] : Module.finrank (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p) = d + 1

theorem EGZ.FpRepresentation.finrank_fiberConstantSubmodule_pos {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : 0 < Module.finrank (ZMod p) ↥(R.fiberConstantSubmodule x)

Constants account for at least one dimension of the fibre-constant space.

theorem EGZ.FpRepresentation.finrank_quotient_fiberConstantSubmodule_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : Module.finrank (ZMod p) ((FpCoord p d →ᵃ[ZMod p] ZMod p) ⧸ R.fiberConstantSubmodule x) ≤ d

At most d independent directions can be added to the fibre-constant space.

structure EGZ.DirectionChain {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Submodule K V) (P : ℕ → V → Prop) (length : ℕ) : Type u_2

A finite prefix of independent extensions of an initial submodule. Only indices below length carry conditions; the remaining values are irrelevant.

• space : ℕ → Submodule K V

  The successive subspaces generated by adjoining the chosen directions to the initial space.

• direction : ℕ → V

  The direction adjoined at each step of the chain.

• initial : self.space 0 = W
• step (i : ℕ) : i < length → self.space (i + 1) = self.space i ⊔ K ∙ self.direction i
• independent (i : ℕ) : i < length → self.direction i ∉ self.space i
• selected (i : ℕ) : i < length → P i (self.direction i)

def EGZ.DirectionChain.empty {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Submodule K V) (P : ℕ → V → Prop) : DirectionChain W P 0

The chain of length zero that stays at the initial subspace.

Equations

• EGZ.DirectionChain.empty W P = { space := fun (x : ℕ) => W, direction := fun (x : ℕ) => 0, initial := ⋯, step := ⋯, independent := ⋯, selected := ⋯ }

noncomputable def EGZ.DirectionChain.append {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K V} {P : ℕ → V → Prop} {k : ℕ} (D : DirectionChain W P k) (ξ : V) (hξ : ξ ∉ D.space k) (hP : P k ξ) : DirectionChain W P (k + 1)

Add one selected direction outside the final submodule.

Equations

• D.append ξ hξ hP = { space := Function.update D.space (k + 1) (D.space k ⊔ K ∙ ξ), direction := Function.update D.direction k ξ, initial := ⋯, step := ⋯, independent := ⋯, selected := ⋯ }

theorem EGZ.DirectionChain.finrank_space {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Submodule K V} {P : ℕ → V → Prop} {k : ℕ} (D : DirectionChain W P k) (i : ℕ) (hi : i ≤ k) : Module.finrank K ↥(D.space i) = Module.finrank K ↥W + i

Each independent singleton extension adds exactly one dimension.

theorem EGZ.DirectionChain.length_le_finrank_quotient {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Submodule K V} {P : ℕ → V → Prop} {k : ℕ} (D : DirectionChain W P k) : k ≤ Module.finrank K (V ⧸ W)

theorem EGZ.DirectionChain.space_le_of_mem {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K V} {P : ℕ → V → Prop} {k : ℕ} (D : DirectionChain W P k) (U : Submodule K V) (hW : W ≤ U) (hdir : ∀ j < k, D.direction j ∈ U) (i : ℕ) (hi : i ≤ k) : D.space i ≤ U

The enlarged space lies in every submodule containing the initial space and all the selected directions.

theorem EGZ.DirectionChain.length_pos_of_exists {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K V} {P : ℕ → V → Prop} {k : ℕ} (D : DirectionChain W P k) (hmax : ∀ ξ ∉ D.space k, ¬P k ξ) (hex : ∃ ξ ∉ W, P 0 ξ) : 0 < k

If a first-stage direction exists, a maximal chain has positive length.

theorem EGZ.exists_maximal_directionChain {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Submodule K V) (P : ℕ → V → Prop) : ∃ k ≤ Module.finrank K (V ⧸ W), ∃ (D : DirectionChain W P k), ∀ ξ ∉ D.space k, ¬P k ξ

A maximal chain exists for arbitrary predicates assigned to its stages. Maximality is tested using the predicate for the next stage.

theorem EGZ.exists_maximal_thinDirections {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) (w : FpCoord p d → ℕ) (t : ℕ → ℕ) (δ : ℝ) : ∃ k ≤ d, ∃ (D : DirectionChain (R.fiberConstantSubmodule x) (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k), ∀ ξ ∉ D.space k, IsThickAlong w ξ (t (k + 1)) (3 ^ (k + 1) * δ)

Maximal independent thin functionals with the paper's stage-dependent width and error parameters. The first selected direction uses stage one.