Supports.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Supporting functionals

Supports are continuous real linear functionals of norm at most one which attain the norm at the specified vector. Hahn–Banach supplies supports and extends them from any subspace. Restriction and extension relate assertions about every ambient support to assertions about every support on a finite span.

The results here hold in arbitrary real normed spaces, including the zero space.

def OAI.Tingley.SupportAt line 24
Source documentation
A norm-bounded real functional attaining the norm at a vector.
```
def SupportAt (φ : X →L[ℝ] ℝ) (a : X) : Prop :=
…
```
theorem OAI.Tingley.exists_support line 28
Source documentation
The norm-at-most-one formulation also supplies a support at zero.
```
theorem exists_support (a : X) : ∃ φ : X →L[ℝ] ℝ, SupportAt φ a :=
…
```
Mentions: OAI.Tingley.SupportAt
theorem OAI.Tingley.abs_apply_le_norm line 31
theorem OAI.Tingley.apply_le_norm line 35
theorem OAI.Tingley.supportAt_zero_iff line 39
theorem OAI.Tingley.SupportAt.smul_nonneg line 43
theorem OAI.Tingley.supportAt_pos_smul_iff line 48
theorem OAI.Tingley.supportAt_neg_iff line 59
theorem OAI.Tingley.SupportAt.neg line 63
theorem OAI.Tingley.SupportAt.subgradient line 67

theorem OAI.Tingley.extension_norm_eq line 73

Source documentation

Hahn–Banach extends from any real subspace without changing the norm.

theorem extension_norm_eq (U : Submodule ℝ X) (φ : U →L[ℝ] ℝ) :
    ∃ Φ : X →L[ℝ] ℝ, (∀ u : U, Φ (u : X) = φ u) ∧ ‖Φ‖ = ‖φ‖ :=
…

theorem OAI.Tingley.supportAt_extension line 77
theorem OAI.Tingley.norm_restrict_le line 84
theorem OAI.Tingley.SupportAt.restrict line 88

theorem OAI.Tingley.exists_extension_norm_eq_of_le line 94

Source documentation

Extending to an enlargement retains even the exact operator norm.

theorem exists_extension_norm_eq_of_le {U V : Submodule ℝ X}
    (hUV : U ≤ V) (φ : U →L[ℝ] ℝ) :
    ∃ ψ : V →L[ℝ] ℝ,
      (∀ u : U, ψ ⟨(u : X), hUV u.property⟩ = φ u) ∧ ‖ψ‖ = ‖φ‖ := by
…

theorem OAI.Tingley.supportAt_finite_enlargement line 110

Source documentation

In particular, a support extends to every specified finite enlargement. The stronger statement does not need either subspace to be finite-dimensional.

theorem supportAt_finite_enlargement (U V : Submodule ℝ X) (hUV : U ≤ V)
    (a : U) (φ : U →L[ℝ] ℝ) (h : SupportAt φ a) :
    ∃ ψ : V →L[ℝ] ℝ,
      (∀ u : U, ψ ⟨(u : X), hUV u.property⟩ = φ u) ∧
      SupportAt ψ ⟨(a : X), hUV a.property⟩ := by
…

Mentions: OAI.Tingley.SupportAt

theorem OAI.Tingley.forall_supportAt_apply_iff_submodule line 120
Source documentation
Universal assertions about support evaluations can be made on any subspace containing the two vectors. This permits using the dual of their finite span.
```
theorem forall_supportAt_apply_iff_submodule (U : Submodule ℝ X)
    (a b : U) (P : ℝ → Prop) :
    (∀ φ : X →L[ℝ] ℝ, SupportAt φ (a : X) → P (φ (b : X))) ↔
    (∀ ψ : U →L[ℝ] ℝ, SupportAt ψ a → P (ψ b)) := by
…
```
Mentions: OAI.Tingley.SupportAt
theorem OAI.Tingley.norm_add_eq_iff_exists_common_supportAt line 132
Source documentation
Triangle equality is equivalent to the existence of a common support.
```
theorem norm_add_eq_iff_exists_common_supportAt (x y : X) :
    ‖x + y‖ = ‖x‖ + ‖y‖ ↔
      ∃ φ : X →L[ℝ] ℝ, SupportAt φ x ∧ SupportAt φ y := by
…
```
Mentions: OAI.Tingley.SupportAt

theorem OAI.Tingley.common_support_of_norm_add_eq line 155

Source documentation

Positive weighted triangle equality for unit vectors gives one functional taking value one at both vectors. No strict convexity is required.

theorem common_support_of_norm_add_eq {v w : X}
    (hv : ‖v‖ = 1) (hw : ‖w‖ = 1) {α β : ℝ}
    (hα : 0 < α) (hβ : 0 < β)
    (heq : ‖α • v + β • w‖ = α + β) :
    ∃ φ : X →L[ℝ] ℝ, ‖φ‖ ≤ 1 ∧ φ v = 1 ∧ φ w = 1 := by
…