MathlibAnnex/Analysis/Normed/GeometricStructure/Support.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6module78public import Mathlib.Analysis.Normed.Module.Dual910/-!11# Supporting functionals and unions of kernels1213The scalar field may be real or complex. The continuous dual is Mathlib's14`StrongDual`. A union of kernels is a `Set`, not a submodule or an ideal.15No nonemptiness of the supporting family is built into its definition.16-/1718@[expose] public section1920set_option autoImplicit false2122universe u v2324namespace NormedSpace2526variable (𝕜 : Type v) [RCLike 𝕜]27variable {E : Type u} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]2829/-- The closed-dual-ball functionals taking the norm value at a vector. -/30def normingFunctionals (x : E) : Set (StrongDual 𝕜 E) :=31  {f | ‖f‖ ≤ 1 ∧ f x = (‖x‖ : 𝕜)}3233@[simp]34theorem mem_normingFunctionals (x : E) (f : StrongDual 𝕜 E) :35    f ∈ normingFunctionals 𝕜 x ↔ ‖f‖ ≤ 1 ∧ f x = (‖x‖ : 𝕜) := Iff.rfl3637/-- Hahn-Banach supplies norming functionals, including at zero in the zero space. -/38theorem nonempty_normingFunctionals (x : E) : (normingFunctionals 𝕜 x).Nonempty :=39  exists_dual_vector'' 𝕜 x4041/-- The closed-dual-ball functionals taking value one at every point of a set. -/42def supportFunctionals (F : Set E) : Set (StrongDual 𝕜 E) :=43  {f | ‖f‖ ≤ 1 ∧ ∀ x ∈ F, f x = 1}4445@[simp]46theorem mem_supportFunctionals (F : Set E) (f : StrongDual 𝕜 E) :47    f ∈ supportFunctionals 𝕜 F ↔ ‖f‖ ≤ 1 ∧ ∀ x ∈ F, f x = 1 := Iff.rfl4849/-- The norm bound is exactly membership in the closed dual unit ball. -/50theorem supportFunctionals_eq_setOf_mem_closedBall (F : Set E) :51    supportFunctionals 𝕜 F =52      {f : StrongDual 𝕜 E | f ∈ Metric.closedBall 0 1 ∧ ∀ x ∈ F, f x = 1} := by53  apply Set.ext54  intro f55  simp only [mem_supportFunctionals, Set.mem_setOf_eq, mem_closedBall_zero_iff]5657/-- For a nonempty set, the pointwise support condition is the paper's image equality.58Nonemptiness is essential for the converse from a constant-value condition to that equality. -/59theorem mem_supportFunctionals_iff_image_eq (F : Set E) (hF : F.Nonempty)60    (f : StrongDual 𝕜 E) :61    f ∈ supportFunctionals 𝕜 F ↔ ‖f‖ ≤ 1 ∧ (f : E → 𝕜) '' F = {1} := by62  constructor63  · intro hf64    refine ⟨hf.1, ?_⟩65    apply Set.ext66    intro a67    constructor68    · rintro ⟨x, hx, rfl⟩69      exact Set.mem_singleton_iff.2 (hf.2 x hx)70    · intro ha71      obtain ⟨x, hx⟩ := hF72      exact ⟨x, hx, (hf.2 x hx).trans (Set.mem_singleton_iff.1 ha).symm⟩73  · rintro ⟨hf, himage⟩74    refine ⟨hf, ?_⟩75    intro x hx76    apply Set.mem_singleton_iff.177    rw [← himage]78    exact ⟨x, hx, rfl⟩7980/-- A supporting functional of a nonempty subset of the closed unit ball has norm one.81This does not assert existence of such a functional. -/82theorem norm_eq_one_of_mem_supportFunctionals {F : Set E} (hF : F.Nonempty)83    (hball : ∀ x ∈ F, ‖x‖ ≤ 1) {f : StrongDual 𝕜 E}84    (hf : f ∈ supportFunctionals 𝕜 F) : ‖f‖ = 1 := by85  apply le_antisymm hf.186  obtain ⟨x, hx⟩ := hF87  calc88    1 = ‖f x‖ := by rw [hf.2 x hx, norm_one]89    _ ≤ ‖f‖ * ‖x‖ := f.le_opNorm x90    _ ≤ ‖f‖ * 1 := mul_le_mul_of_nonneg_left (hball x hx) (norm_nonneg f)91    _ = ‖f‖ := mul_one _9293theorem supportFunctionals_antitone {F G : Set E} (hFG : F ⊆ G) :94    supportFunctionals 𝕜 G ⊆ supportFunctionals 𝕜 F :=95  fun _ hf => ⟨hf.1, fun x hx => hf.2 x (hFG hx)⟩9697/-- A unit vector is supported by at least one closed-dual-ball functional. -/98theorem nonempty_supportFunctionals_singleton (x : E) (hx : ‖x‖ = 1) :99    (supportFunctionals 𝕜 {x}).Nonempty := by100  obtain ⟨f, hf, hfx⟩ := exists_dual_vector'' 𝕜 x101  refine ⟨f, hf, ?_⟩102  intro y hy103  have hyx : y = x := Set.mem_singleton_iff.1 hy104  subst y105  simpa [hx] using hfx106107/-- The set-theoretic union of the kernels of all supporting functionals. -/108def supportKernelUnion (F : Set E) : Set E :=109  {x | ∃ f ∈ supportFunctionals 𝕜 F, f x = 0}110111@[simp]112theorem mem_supportKernelUnion (F : Set E) (x : E) :113    x ∈ supportKernelUnion 𝕜 F ↔ ∃ f ∈ supportFunctionals 𝕜 F, f x = 0 := Iff.rfl114115/-- The defining union, written using ordinary inverse images of zero. -/116theorem supportKernelUnion_eq_iUnion (F : Set E) :117    supportKernelUnion 𝕜 F =118      ⋃ f ∈ supportFunctionals 𝕜 F, (f : E → 𝕜) ⁻¹' {0} := by119  apply Set.ext120  intro x121  simp only [mem_supportKernelUnion, Set.mem_iUnion, Set.mem_preimage,122    Set.mem_singleton_iff, exists_prop]123124theorem supportKernelUnion_antitone {F G : Set E} (hFG : F ⊆ G) :125    supportKernelUnion 𝕜 G ⊆ supportKernelUnion 𝕜 F := by126  rintro x ⟨f, hf, hfx⟩127  exact ⟨f, supportFunctionals_antitone 𝕜 hFG hf, hfx⟩128129/-- Every point of a nonempty supporting set lies outside the union of kernels. -/130theorem notMem_supportKernelUnion_of_mem {F : Set E} {x : E} (hx : x ∈ F) :131    x ∉ supportKernelUnion 𝕜 F := by132  rintro ⟨f, hf, hfx⟩133  exact one_ne_zero ((hf.2 x hx).symm.trans hfx)134135/-- The hull-kernel admissibility condition needs no existence theorem for support. -/136theorem supportKernelUnion_ne_univ {F : Set E} (hF : F.Nonempty) :137    supportKernelUnion 𝕜 F ≠ Set.univ := by138  intro h139  obtain ⟨x, hx⟩ := hF140  apply notMem_supportKernelUnion_of_mem 𝕜 hx141  rw [h]142  exact Set.mem_univ x143144/-- At zero, membership detects whether the supporting family is nonempty. -/145theorem zero_mem_supportKernelUnion_iff (F : Set E) :146    (0 : E) ∈ supportKernelUnion 𝕜 F ↔ (supportFunctionals 𝕜 F).Nonempty := by147  constructor148  · rintro ⟨f, hf, _⟩149    exact ⟨f, hf⟩150  · rintro ⟨f, hf⟩151    exact ⟨f, hf, f.map_zero⟩152153/-- Nonemptiness in `supportKernelUnion_ne_univ` cannot simply be dropped. -/154@[simp]155theorem supportKernelUnion_empty : supportKernelUnion 𝕜 (∅ : Set E) = Set.univ := by156  apply Set.Subset.antisymm (Set.subset_univ _)157  intro x _158  refine ⟨0, ⟨by simp, ?_⟩, ?_⟩159  · intro y hy160    exact False.elim hy161  · rfl162163/-- A singleton-support identity converts the union into one kernel.164This theorem does not assert that the supporting family is a singleton. -/165theorem supportKernelUnion_eq_preimage_zero_of_supportFunctionals_eq_singleton166    (F : Set E) (f : StrongDual 𝕜 E) (hF : supportFunctionals 𝕜 F = {f}) :167    supportKernelUnion 𝕜 F = (f : E → 𝕜) ⁻¹' {0} := by168  apply Set.ext169  intro x170  constructor171  · rintro ⟨g, hg, hgx⟩172    rw [hF] at hg173    have hgf : g = f := Set.mem_singleton_iff.1 hg174    subst g175    exact hgx176  · intro hx177    refine ⟨f, ?_, hx⟩178    rw [hF]179    exact Set.mem_singleton f180181end NormedSpace