MathlibAnnex/Analysis/CStarAlgebra/DirectSum/C0DirectSum.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-/6module7public import Mathlib.Analysis.CStarAlgebra.lpSpace8public import Mathlib.Topology.Algebra.NonUnitalStarAlgebra9public import Mathlib.Topology.Sequences10public import Mathlib.Tactic1112@[expose] public section1314/-!15# Dependent c₀-direct sums1617Mathlib already supplies the dependent bounded product `lp A ∞`, with its18pointwise nonunital C-star structure.  This file defines the actual dependent19c₀-direct sum as the norm-closed star subalgebra of families vanishing at20infinity.  No countability or separability assumption is imposed on the index21set or on the fibres.2223The file also supplies coordinate evaluations, coordinate embeddings, finite24truncations, and the exact supremum norm formula.  The algebraic direct sum,25the bounded product, and the c₀-direct sum remain separate objects throughout.26-/2728set_option autoImplicit false29noncomputable section3031open Filter Set Topology32open scoped BigOperators CStarAlgebra ENNReal3334namespace MathlibAnnex.Analysis.CStarAlgebra3536universe uι uA uH3738namespace C0DirectSum3940variable {ι : Type uι} (A : ι → Type uA)41variable [∀ i, NonUnitalCStarAlgebra (A i)]4243/-- A bounded dependent family vanishes at infinity when every positive44superlevel set of coordinate norms is finite. -/45def VanishesAtInfinity (x : lp A ∞) : Prop :=46  ∀ ε : ℝ, 0 < ε → Set.Finite {i : ι | ε ≤ ‖x i‖}4748@[simp]49theorem vanishesAtInfinity_zero : VanishesAtInfinity A 0 := by50  intro ε hε51  simpa [VanishesAtInfinity, not_le_of_gt hε] using52    (Set.finite_empty : Set.Finite (∅ : Set ι))5354theorem VanishesAtInfinity.neg {x : lp A ∞} (hx : VanishesAtInfinity A x) :55    VanishesAtInfinity A (-x) := by56  simpa [VanishesAtInfinity] using hx5758@[simp]59theorem vanishesAtInfinity_neg_iff {x : lp A ∞} :60    VanishesAtInfinity A (-x) ↔ VanishesAtInfinity A x :=61  ⟨fun h => by simpa only [neg_neg] using h.neg (A := A), fun h => h.neg (A := A)⟩6263theorem VanishesAtInfinity.add {x y : lp A ∞}64    (hx : VanishesAtInfinity A x) (hy : VanishesAtInfinity A y) :65    VanishesAtInfinity A (x + y) := by66  intro ε hε67  have hx' := hx (ε / 2) (half_pos hε)68  have hy' := hy (ε / 2) (half_pos hε)69  refine (hx'.union hy').subset ?_70  intro i hi71  simp only [Set.mem_union, Set.mem_setOf_eq]72  by_contra hsmall73  push_neg at hsmall74  change ε ≤ ‖x i + y i‖ at hi75  have htri : ‖x i + y i‖ ≤ ‖x i‖ + ‖y i‖ := norm_add_le _ _76  linarith7778theorem VanishesAtInfinity.sub {x y : lp A ∞}79    (hx : VanishesAtInfinity A x) (hy : VanishesAtInfinity A y) :80    VanishesAtInfinity A (x - y) := by81  simpa only [sub_eq_add_neg] using hx.add (A := A) (hy.neg (A := A))8283theorem VanishesAtInfinity.smul (c : ℂ) {x : lp A ∞}84    (hx : VanishesAtInfinity A x) : VanishesAtInfinity A (c • x) := by85  by_cases hc : c = 086  · subst c87    simpa using vanishesAtInfinity_zero (A := A)88  intro ε hε89  have hcpos : 0 < ‖c‖ := norm_pos_iff.mpr hc90  have hfinite := hx (ε / ‖c‖) (div_pos hε hcpos)91  refine hfinite.subset ?_92  intro i hi93  change ε / ‖c‖ ≤ ‖x i‖94  change ε ≤ ‖c • x i‖ at hi95  rw [norm_smul] at hi96  exact (div_le_iff₀ hcpos).2 (by simpa [mul_comm] using hi)9798theorem VanishesAtInfinity.mul {x y : lp A ∞}99    (hx : VanishesAtInfinity A x) (hy : VanishesAtInfinity A y) :100    VanishesAtInfinity A (x * y) := by101  intro ε hε102  let δ : ℝ := Real.sqrt ε103  have hδ : 0 < δ := Real.sqrt_pos.2 hε104  have hδsq : δ * δ = ε := by105    dsimp [δ]106    exact Real.mul_self_sqrt hε.le107  have hx' := hx δ hδ108  have hy' := hy δ hδ109  refine (hx'.union hy').subset ?_110  intro i hi111  simp only [Set.mem_union, Set.mem_setOf_eq]112  by_contra hsmall113  push_neg at hsmall114  change ε ≤ ‖x i * y i‖ at hi115  have hmul : ‖x i * y i‖ ≤ ‖x i‖ * ‖y i‖ := norm_mul_le _ _116  have hprod : ‖x i‖ * ‖y i‖ < δ * δ := calc117    ‖x i‖ * ‖y i‖ ≤ ‖x i‖ * δ :=118      mul_le_mul_of_nonneg_left hsmall.2.le (norm_nonneg _)119    _ < δ * δ := mul_lt_mul_of_pos_right hsmall.1 hδ120  linarith121122theorem VanishesAtInfinity.star {x : lp A ∞}123    (hx : VanishesAtInfinity A x) : VanishesAtInfinity A (star x) := by124  simpa [VanishesAtInfinity] using hx125126@[simp]127theorem vanishesAtInfinity_star_iff {x : lp A ∞} :128    VanishesAtInfinity A (star x) ↔ VanishesAtInfinity A x :=129  ⟨fun h => by simpa only [star_star] using h.star (A := A), fun h => h.star (A := A)⟩130131/-- Finitely supported bounded families, before norm closure. -/132def finiteSupportStarSubalgebra : NonUnitalStarSubalgebra ℂ (lp A ∞) where133  carrier := {x | Set.Finite {i : ι | x i ≠ 0}}134  zero_mem' := by simp135  add_mem' := by136    intro x y hx hy137    refine (hx.union hy).subset ?_138    intro i hi139    change x i + y i ≠ 0 at hi140    simp only [Set.mem_union, Set.mem_setOf_eq]141    by_contra h142    push_neg at h143    exact hi (by simp [h.1, h.2])144  mul_mem' := by145    intro x y hx hy146    refine hx.subset ?_147    intro i hi148    change x i ≠ 0149    intro hxi150    apply hi151    simp [hxi]152  smul_mem' := by153    intro c x hx154    refine hx.subset ?_155    intro i hi156    change x i ≠ 0157    intro hxi158    apply hi159    simp [hxi]160  star_mem' := by161    intro x hx162    refine hx.subset ?_163    intro i hi164    change x i ≠ 0165    intro hxi166    apply hi167    simp [hxi]168169@[simp]170theorem mem_finiteSupportStarSubalgebra (x : lp A ∞) :171    x ∈ finiteSupportStarSubalgebra A ↔ Set.Finite {i : ι | x i ≠ 0} :=172  Iff.rfl173174/-- The dependent c₀-direct sum as a concrete star subalgebra of the bounded175product. -/176def starSubalgebra : NonUnitalStarSubalgebra ℂ (lp A ∞) where177  carrier := {x | VanishesAtInfinity A x}178  zero_mem' := vanishesAtInfinity_zero A179  add_mem' := fun hx hy => hx.add (A := A) hy180  mul_mem' := fun hx hy => hx.mul (A := A) hy181  smul_mem' := fun c _ hx => hx.smul (A := A) c182  star_mem' := fun hx => hx.star (A := A)183184@[simp]185theorem mem_starSubalgebra (x : lp A ∞) :186    x ∈ starSubalgebra A ↔ VanishesAtInfinity A x := Iff.rfl187188/-- Vanishing at infinity is closed in the supremum norm. -/189theorem isClosed_setOf_vanishesAtInfinity :190    IsClosed {x : lp A ∞ | VanishesAtInfinity A x} := by191  rw [← isOpen_compl_iff]192  refine Metric.isOpen_iff.mpr ?_193  intro x hx194  change ¬ VanishesAtInfinity A x at hx195  unfold VanishesAtInfinity at hx196  push_neg at hx197  obtain ⟨ε, hε, hinfinite⟩ := hx198  refine ⟨ε / 2, half_pos hε, ?_⟩199  intro y hy200  change ¬ VanishesAtInfinity A y201  intro hy0202  have hfinite := hy0 (ε / 2) (half_pos hε)203  apply hinfinite204  refine hfinite.subset ?_205  intro i hi206  change ε / 2 ≤ ‖y i‖207  change ε ≤ ‖x i‖ at hi208  have hcoord : ‖x i - y i‖ ≤ ‖x - y‖ := by209    simpa only [lp.coeFn_sub, Pi.sub_apply] using210      lp.norm_apply_le_norm (by simp) (x - y) i211  have hdist : ‖x - y‖ < ε / 2 := by212    simpa only [Metric.mem_ball, dist_eq_norm, norm_sub_rev] using hy213  have hreverse : ‖x i‖ - ‖y i‖ ≤ ‖x i - y i‖ := by214    exact norm_sub_norm_le (x i) (y i)215  linarith216217/-- The c₀-direct sum is norm closed in the bounded product. -/218theorem isClosed_starSubalgebra : IsClosed (starSubalgebra A : Set (lp A ∞)) :=219  isClosed_setOf_vanishesAtInfinity A220221end C0DirectSum222223/-- The actual dependent c₀-direct sum.  It is a subtype of `lp A ∞`, not an224unrestricted product and not an algebraic direct sum. -/225abbrev C0DirectSum {ι : Type uι} (A : ι → Type uA)226    [∀ i, NonUnitalCStarAlgebra (A i)] :=227  C0DirectSum.starSubalgebra A228229namespace C0DirectSum230231variable {ι : Type uι} (A : ι → Type uA)232variable [∀ i, NonUnitalCStarAlgebra (A i)]233234instance nonUnitalCStarAlgebra : NonUnitalCStarAlgebra (C0DirectSum A) :=235  NonUnitalStarSubalgebra.nonUnitalCStarAlgebra _236    (h_closed := isClosed_starSubalgebra A)237238/-- Coordinate evaluation on the dependent c₀-direct sum. -/239def eval (i : ι) : C0DirectSum A →⋆ₙₐ[ℂ] A i where240  toFun := fun x => x.1 i241  map_zero' := rfl242  map_add' := fun _ _ => rfl243  map_mul' := fun _ _ => rfl244  map_smul' := fun _ _ => rfl245  map_star' := fun _ => rfl246247@[simp]248theorem eval_apply (i : ι) (x : C0DirectSum A) : eval A i x = x.1 i := rfl249250open scoped Classical251252/-- A single nonzero coordinate is a c₀-family. -/253theorem vanishesAtInfinity_single (i : ι) (a : A i) :254    VanishesAtInfinity A (lp.single ∞ i a) := by255  intro ε hε256  refine (Set.finite_singleton i).subset ?_257  intro j hj258  simp only [Set.mem_singleton_iff]259  by_contra hji260  have hz : (lp.single ∞ i a : lp A ∞) j = 0 := by261    simp [lp.single_apply, hji, Ne.symm hji]262  change ε ≤ ‖(lp.single ∞ i a : lp A ∞) j‖ at hj263  rw [hz, norm_zero] at hj264  exact (not_lt_of_ge hj) hε265266/-- The coordinate embedding into the dependent c₀-direct sum. -/267def single (i : ι) : A i →⋆ₙₐ[ℂ] C0DirectSum A where268  toFun := fun a => ⟨lp.single ∞ i a, vanishesAtInfinity_single A i a⟩269  map_zero' := by270    apply Subtype.ext271    ext j272    simp [lp.single_apply]273  map_add' := by274    intro a b275    apply Subtype.ext276    ext j277    simp [lp.single_apply]278  map_mul' := by279    intro a b280    apply Subtype.ext281    ext j282    by_cases hji : j = i283    · subst j284      simp [lp.single_apply]285    · simp [lp.single_apply, hji, Ne.symm hji]286  map_smul' := by287    intro c a288    apply Subtype.ext289    ext j290    simp [lp.single_apply]291  map_star' := by292    intro a293    apply Subtype.ext294    ext j295    by_cases hji : j = i296    · subst j297      simp [lp.single_apply]298    · simp [lp.single_apply, hji, Ne.symm hji]299300@[simp]301theorem eval_single_same (i : ι) (a : A i) : eval A i (single A i a) = a := by302  change (lp.single ∞ i a : lp A ∞) i = a303  simp [lp.single_apply]304305@[simp]306theorem eval_single_of_ne {i j : ι} (h : j ≠ i) (a : A i) :307    eval A j (single A i a) = 0 := by308  change (lp.single ∞ i a : lp A ∞) j = 0309  simp [lp.single_apply, h, Ne.symm h]310311/-- Every coordinate evaluation is onto. -/312theorem eval_surjective (i : ι) : Function.Surjective (eval A i) := by313  intro a314  exact ⟨single A i a, eval_single_same A i a⟩315316/-- Every coordinate embedding is injective. -/317theorem single_injective (i : ι) : Function.Injective (single A i) := by318  intro a b h319  have := congrArg (fun x : C0DirectSum A => eval A i x) h320  simpa only [eval_single_same] using this321322/-- Coordinate evaluation is contractive for the inherited supremum norm. -/323theorem norm_eval_le (i : ι) (x : C0DirectSum A) : ‖eval A i x‖ ≤ ‖x‖ := by324  change ‖x.1 i‖ ≤ ‖x.1‖325  exact lp.norm_apply_le_norm (by simp) x.1 i326327/-- A coordinate embedding is an isometry. -/328@[simp]329theorem norm_single (i : ι) (a : A i) : ‖single A i a‖ = ‖a‖ := by330  change ‖(lp.single ∞ i a : lp A ∞)‖ = ‖a‖331  exact lp.norm_single (by simp) i a332333/-- The c₀ norm is literally the supremum of the coordinate norms. -/334theorem norm_eq_ciSup (x : C0DirectSum A) : ‖x‖ = ⨆ i, ‖eval A i x‖ := by335  change ‖x.1‖ = ⨆ i, ‖x.1 i‖336  exact lp.norm_eq_ciSup x.1337338/-- Finite coordinate truncation inside the actual c₀-direct sum. -/339def truncate (s : Finset ι) (x : C0DirectSum A) : C0DirectSum A :=340  ∑ i ∈ s, single A i (eval A i x)341342@[simp]343theorem eval_truncate (s : Finset ι) (x : C0DirectSum A) (j : ι) :344    eval A j (truncate A s x) = if j ∈ s then eval A j x else 0 := by345  classical346  simp only [truncate, map_sum, Finset.sum_apply]347  by_cases hj : j ∈ s348  · rw [Finset.sum_eq_single j]349    · simpa only [if_pos hj] using eval_single_same A j (eval A j x)350    · intro i hi hij351      exact eval_single_of_ne A (Ne.symm hij) (eval A i x)352    · exact fun h => (h hj).elim353  · have hne : ∀ i ∈ s, j ≠ i := by354      intro i hi hji355      exact hj (hji ▸ hi)356    rw [if_neg hj]357    apply Finset.sum_eq_zero358    intro i hi359    exact eval_single_of_ne A (hne i hi) (eval A i x)360361/-- A finite truncation has finite support, independently of the support of the362original element. -/363theorem finite_support_truncate (s : Finset ι) (x : C0DirectSum A) :364    Set.Finite {j : ι | eval A j (truncate A s x) ≠ 0} := by365  classical366  refine s.finite_toSet.subset ?_367  intro j hj368  by_contra hjs369  change j ∉ s at hjs370  have heval := eval_truncate A s x j371  rw [if_neg hjs] at heval372  exact hj heval373374/-- A uniform coordinate estimate off `s` controls the norm of the truncation375remainder. -/376theorem norm_sub_truncate_le (s : Finset ι) (x : C0DirectSum A) {ε : ℝ}377    (hε : 0 ≤ ε) (h : ∀ i, i ∉ s → ‖eval A i x‖ ≤ ε) :378    ‖x - truncate A s x‖ ≤ ε := by379  change ‖(x - truncate A s x).1‖ ≤ ε380  refine lp.norm_le_of_forall_le hε ?_381  intro i382  change ‖eval A i x - eval A i (truncate A s x)‖ ≤ ε383  rw [eval_truncate]384  by_cases hi : i ∈ s385  · simpa [hi] using hε386  · simpa [hi] using h i hi387388/-- Finite truncations converge in norm to every c₀-family. -/389theorem exists_finset_norm_sub_truncate_lt (x : C0DirectSum A) {ε : ℝ} (hε : 0 < ε) :390    ∃ s : Finset ι, ‖x - truncate A s x‖ < ε := by391  classical392  let δ : ℝ := ε / 2393  have hδ : 0 < δ := half_pos hε394  have hfinite : Set.Finite {i : ι | δ ≤ ‖eval A i x‖} := by395    simpa only [eval_apply] using x.2 δ hδ396  let s : Finset ι := hfinite.toFinset397  refine ⟨s, (norm_sub_truncate_le A s x hδ.le ?_).trans_lt (half_lt_self hε)⟩398  intro i hi399  have hnot : ¬ δ ≤ ‖eval A i x‖ := by400    intro hlarge401    apply hi402    exact hfinite.mem_toFinset.2 hlarge403  exact le_of_lt (lt_of_not_ge hnot)404405406end C0DirectSum407408end MathlibAnnex.Analysis.CStarAlgebra