Translation-invariant Hahn–Banach extensions by finite averaging

Background for Lemma 3.2 (lem:exotic-mean). Let R be an action of the additive group ℝ on a real normed space E by linear contractions (no continuity in the translation parameter is assumed). Let e ∈ E be fixed by R and V an R-invariant subspace such that |c| ≤ ‖c • e + v‖ for all c ∈ ℝ and v ∈ V. Then exists_invariant_extension provides m ∈ E* with ‖m‖ ≤ 1, m e = 1, m = 0 on V and m ∘ R a = m for all a.

Proof: finite Cesàro averages of translations make every coboundary R a x - x arbitrarily small without moving e nor leaving V (difference_annihilable), so the separation of e from V persists from V to V ⊔ coboundaries (separation_sup_coboundaries); then apply the Hahn–Banach theorem to the coefficient of e (extend_from_separation).

structure AbstractLinearControl.ExoticMean.HahnBanach.Action (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_2

A contractive real-translation action, with no continuity assumption in a.

• T : ℝ → E →ₗ[ℝ] E

  Translation by the real parameter.

• zero_apply (x : E) : (self.T 0) x = x
• add_apply (a b : ℝ) (x : E) : (self.T (a + b)) x = (self.T a) ((self.T b) x)
• bound (a : ℝ) (x : E) : ‖(self.T a) x‖ ≤ ‖x‖

theorem AbstractLinearControl.ExoticMean.HahnBanach.Action.commute {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (a b : ℝ) (x : E) : (R.T a) ((R.T b) x) = (R.T b) ((R.T a) x)

structure AbstractLinearControl.ExoticMean.HahnBanach.Averager {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) : Type u_1

An averaging operator preserves e and V, is contractive, and belongs algebraically to the bicommutant of the translation action. The last field lets us compose averaging operators without introducing a finite-product API. Every finite Cesàro average of translations has this property.

• op : E →ₗ[ℝ] E

  The contractive averaging operator.

• fixes : self.op e = e
• preserves (x : E) : x ∈ V → self.op x ∈ V
• bound (x : E) : ‖self.op x‖ ≤ ‖x‖
• bicommutes (L : E →ₗ[ℝ] E) : (∀ (a : ℝ) (x : E), L ((R.T a) x) = (R.T a) (L x)) → ∀ (x : E), self.op (L x) = L (self.op x)

def AbstractLinearControl.ExoticMean.HahnBanach.Averager.identity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) : Averager R e V

The identity averaging operator.

Equations

• AbstractLinearControl.ExoticMean.HahnBanach.Averager.identity R e V = { op := LinearMap.id, fixes := ⋯, preserves := ⋯, bound := ⋯, bicommutes := ⋯ }

theorem AbstractLinearControl.ExoticMean.HahnBanach.Averager.commute_translation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : Action E} {e : E} {V : Submodule ℝ E} (Q : Averager R e V) (a : ℝ) (x : E) : Q.op ((R.T a) x) = (R.T a) (Q.op x)

theorem AbstractLinearControl.ExoticMean.HahnBanach.Averager.commute {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : Action E} {e : E} {V : Submodule ℝ E} (Q P : Averager R e V) (x : E) : Q.op (P.op x) = P.op (Q.op x)

def AbstractLinearControl.ExoticMean.HahnBanach.Averager.comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : Action E} {e : E} {V : Submodule ℝ E} (Q P : Averager R e V) : Averager R e V

Composition of two averaging operators.

Equations

• Q.comp P = { op := Q.op ∘ₗ P.op, fixes := ⋯, preserves := ⋯, bound := ⋯, bicommutes := ⋯ }

noncomputable def AbstractLinearControl.ExoticMean.HahnBanach.Averager.cesaro {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) (a : ℝ) (N : ℕ) (hN : 0 < N) : Averager R e V

The ordinary finite Cesàro average. N must be strictly positive.

Equations

• AbstractLinearControl.ExoticMean.HahnBanach.Averager.cesaro R e V he hV a N hN = { op := (↑N)⁻¹ • ∑ k ∈ Finset.range N, R.T (↑k * a), fixes := ⋯, preserves := ⋯, bound := ⋯, bicommutes := ⋯ }

theorem AbstractLinearControl.ExoticMean.HahnBanach.Averager.cesaro_difference {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) (a : ℝ) (N : ℕ) (hN : 0 < N) (x : E) : (cesaro R e V he hV a N hN).op ((R.T a) x - x) = (↑N)⁻¹ • ((R.T (↑N * a)) x - x)

theorem AbstractLinearControl.ExoticMean.HahnBanach.Averager.cesaro_difference_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) (a : ℝ) (N : ℕ) (hN : 0 < N) (x : E) : ‖(cesaro R e V he hV a N hN).op ((R.T a) x - x)‖ ≤ 2 * ‖x‖ / ↑N

def AbstractLinearControl.ExoticMean.HahnBanach.annihilable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) : Submodule ℝ E

Vectors made arbitrarily small by finite contractive averaging.

Equations

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

def AbstractLinearControl.ExoticMean.HahnBanach.coboundaries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) : Submodule ℝ E

All finite real linear combinations of translation differences.

Equations

• AbstractLinearControl.ExoticMean.HahnBanach.coboundaries R = Submodule.span ℝ {d : E | ∃ (a : ℝ) (x : E), d = (R.T a) x - x}

theorem AbstractLinearControl.ExoticMean.HahnBanach.difference_annihilable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) (a : ℝ) (x : E) : (R.T a) x - x ∈ annihilable R e V

theorem AbstractLinearControl.ExoticMean.HahnBanach.coboundaries_le_annihilable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) : coboundaries R ≤ annihilable R e V

theorem AbstractLinearControl.ExoticMean.HahnBanach.separation_sup_coboundaries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) (hsep : ∀ (c : ℝ), ∀ v ∈ V, |c| ≤ ‖c • e + v‖) (c : ℝ) (w : E) : w ∈ V ⊔ coboundaries R → |c| ≤ ‖c • e + w‖

The key estimate: adjoining all translation differences preserves the norm separation of the constants.

theorem AbstractLinearControl.ExoticMean.HahnBanach.extend_from_separation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E) (W : Submodule ℝ E) (hsep : ∀ (c : ℝ), ∀ w ∈ W, |c| ≤ ‖c • e + w‖) : ∃ (m : E →L[ℝ] ℝ), ‖m‖ ≤ 1 ∧ m e = 1 ∧ ∀ w ∈ W, m w = 0

Hahn--Banach applied to the coefficient of e, without presupposing a choice of direct-sum decomposition. The separation estimate itself proves that the coefficient is well-defined.

theorem AbstractLinearControl.ExoticMean.HahnBanach.exists_invariant_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : Action E) (e : E) (V : Submodule ℝ E) (he : ∀ (a : ℝ), (R.T a) e = e) (hV : ∀ (a : ℝ), ∀ x ∈ V, (R.T a) x ∈ V) (hsep : ∀ (c : ℝ), ∀ v ∈ V, |c| ≤ ‖c • e + v‖) : ∃ (m : E →L[ℝ] ℝ), ‖m‖ ≤ 1 ∧ m e = 1 ∧ (∀ v ∈ V, m v = 0) ∧ ∀ (a : ℝ) (x : E), m ((R.T a) x) = m x

Translation-invariant Hahn–Banach extension: the main result of this file.