feat(Analysis/Normed/Algebra/GelfandMazur): new file (#29649)

This adds two versions of the *Gelfand-Mazur* *Theorem*:
```lean
NormedAlgebra.Complex.nonempty_algEquiv (F : Type*) [NormedRing F] [NormOneClass F]
    [NormMulClass F] [NormedAlgebra ℂ F] [Nontrivial F] :
    Nonempty (ℂ ≃ₐ[ℂ] F)

NormedAlgebra.Real.nonempty_algEquiv_or (F : Type*) [NormedField F] [NormedAlgebra ℝ F] :
    Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)
```
The version for complex algebras differs in its assumptions from the existing version [NormedRing.algEquivComplexOfComplete](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Algebra/Spectrum.html#NormedRing.algEquivComplexOfComplete) (nontrivial normed algebra with multiplicative norm vs. complete division ring with submultiplicative norm).
A version for real algebras is not yet in Mathlib; it is needed in the context of implementing (absolute) heights; see [Heights](https://github.com/MichaelStollBayreuth/Heights).

Following a suggestion by @j-loreaux, we also add some API for the `Bornology.cobounded` filter.

Author: MichaelStollBayreuth

Mathlib.lean

@@ -1809,6 +1809,7 @@ import Mathlib.Analysis.Normed.Algebra.Basic
 import Mathlib.Analysis.Normed.Algebra.DualNumber
 import Mathlib.Analysis.Normed.Algebra.Exponential
 import Mathlib.Analysis.Normed.Algebra.GelfandFormula
+import Mathlib.Analysis.Normed.Algebra.GelfandMazur
 import Mathlib.Analysis.Normed.Algebra.MatrixExponential
 import Mathlib.Analysis.Normed.Algebra.QuaternionExponential
 import Mathlib.Analysis.Normed.Algebra.Spectrum

Mathlib/Analysis/Calculus/TangentCone.lean

@@ -562,7 +562,7 @@ theorem tangentConeAt_mono_field : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜
     · intro β hβ
       rw [mem_map, mem_atTop_sets]
       obtain ⟨n, hn⟩ := mem_atTop_sets.1
-        (mem_map.1 (h₁ (algebraMap_cobounded_le_cobounded (𝕜 := 𝕜) (𝕜' := 𝕜') hβ)))
+        (mem_map.1 (h₁ (tendsto_algebraMap_cobounded (𝕜 := 𝕜) (𝕜' := 𝕜') hβ)))
       use n, fun _ _ ↦ by simp_all
     · simpa
 

Mathlib/Analysis/Complex/PhragmenLindelof.lean

@@ -516,7 +516,7 @@ theorem quadrant_III (hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0))
   · rcases hB with ⟨c, hc, B, hO⟩
     refine ⟨c, hc, B, ?_⟩
     simpa only [Function.comp_def, norm_neg]
-      using hO.comp_tendsto (tendsto_neg_cobounded.inf H.tendsto)
+      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)
   · rw [comp_apply, ← ofReal_neg]
     exact hre (-x) (neg_nonpos.2 hx)
   · rw [comp_apply, ← neg_mul, ← ofReal_neg]
@@ -580,7 +580,7 @@ theorem quadrant_IV (hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0))
   · rcases hB with ⟨c, hc, B, hO⟩
     refine ⟨c, hc, B, ?_⟩
     simpa only [Function.comp_def, norm_neg]
-      using hO.comp_tendsto (tendsto_neg_cobounded.inf H.tendsto)
+      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)
   · rw [comp_apply, ← ofReal_neg]
     exact hre (-x) (neg_nonneg.2 hx)
   · rw [comp_apply, ← neg_mul, ← ofReal_neg]

Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean

@@ -298,18 +298,20 @@ end NNReal
 
 variable (𝕜)
 
-/--
-Preimages of cobounded sets under the algebra map are cobounded.
--/
-theorem algebraMap_cobounded_le_cobounded [NormOneClass 𝕜'] :
-    Filter.map (algebraMap 𝕜 𝕜') (Bornology.cobounded 𝕜) ≤ Bornology.cobounded 𝕜' := by
+open Filter Bornology in
+/-- Preimages of cobounded sets under the algebra map are cobounded. -/
+@[simp]
+theorem tendsto_algebraMap_cobounded (𝕜 𝕜' : Type*) [NormedField 𝕜] [SeminormedRing 𝕜']
+    [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] :
+    Tendsto (algebraMap 𝕜 𝕜') (cobounded 𝕜) (cobounded 𝕜') := by
   intro c hc
-  rw [Filter.mem_map, ← Bornology.isCobounded_def, ← Bornology.isBounded_compl_iff,
-    isBounded_iff_forall_norm_le]
-  obtain ⟨s, hs⟩ := isBounded_iff_forall_norm_le.1
-    (Bornology.isBounded_compl_iff.2 (Bornology.isCobounded_def.1 hc))
-  use s
-  exact fun x hx ↦ by simpa [norm_algebraMap, norm_one] using hs ((algebraMap 𝕜 𝕜') x) hx
+  rw [mem_map]
+  rw [← isCobounded_def, ← isBounded_compl_iff, isBounded_iff_forall_norm_le] at hc ⊢
+  obtain ⟨s, hs⟩ := hc
+  exact ⟨s, fun x hx ↦ by simpa using hs (algebraMap 𝕜 𝕜' x) hx⟩
+
+@[deprecated (since := "2025-11-04")] alias
+  algebraMap_cobounded_le_cobounded := tendsto_algebraMap_cobounded
 
 /-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
 theorem algebraMap_isometry [NormOneClass 𝕜'] : Isometry (algebraMap 𝕜 𝕜') := by

Mathlib/Analysis/Normed/Module/Basic.lean

@@ -535,6 +535,20 @@ theorem Tendsto.prodMap_coprod {δ : Type*} {f : α → γ} {g : β → δ} {a :
     Tendsto (Prod.map f g) (a.coprod b) (c.coprod d) :=
   map_prodMap_coprod_le.trans (coprod_mono hf hg)
 
+lemma Tendsto.coprod_of_prod_top_right {f : α × β → γ} {la : Filter α} {lb : Filter β}
+    {lc : Filter γ} (h₁ : ∀ s : Set α, s ∈ la → Tendsto f (𝓟 sᶜ ×ˢ lb) lc)
+    (h₂ : Tendsto f (la ×ˢ ⊤) lc) :
+    Tendsto f (la.coprod lb) lc := by
+  simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
+  grind
+
+lemma Tendsto.coprod_of_prod_top_left {f : α × β → γ} {la : Filter α} {lb : Filter β}
+    {lc : Filter γ} (h₁ : ∀ s : Set β, s ∈ lb → Tendsto f (la ×ˢ 𝓟 sᶜ) lc)
+    (h₂ : Tendsto f (⊤ ×ˢ lb) lc) :
+    Tendsto f (la.coprod lb) lc := by
+  simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
+  grind
+
 end Coprod
 
 end Filter

Mathlib/Order/Filter/Prod.lean

@@ -66,7 +66,6 @@ lemma boundedSub_of_lipschitzWith_sub [PseudoMetricSpace R] [Sub R] {K : NNReal}
 
 end bounded_sub
 
-
 section bounded_mul
 /-!
 ### Bounded multiplication and addition
@@ -158,6 +157,46 @@ lemma SeminormedAddCommGroup.lipschitzWith_sub :
 
 instance : BoundedSub R := boundedSub_of_lipschitzWith_sub SeminormedAddCommGroup.lipschitzWith_sub
 
+open Filter Pointwise Bornology
+
+/-
+TODO:
+* Generalize the following to bornologies and `BoundedFoo` classes.
+* Add `BoundedNeg`, `BoundedInv` and `BoundedDiv` in the process.
+-/
+
+@[simp]
+lemma tendsto_add_const_cobounded (x : R) :
+    Tendsto (· + x) (cobounded R) (cobounded R) := by
+  intro s hs
+  rw [mem_map]
+  rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢
+  rw [← Set.preimage_compl]
+  convert isBounded_sub hs (t := {x}) isBounded_singleton using 1
+  ext y
+  simp [sub_eq_iff_eq_add]
+
+@[simp]
+lemma tendsto_const_add_cobounded (x : R) :
+    Tendsto (x + ·) (cobounded R) (cobounded R) := by
+  intro s hs
+  rw [mem_map]
+  rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢
+  rw [← Set.preimage_compl]
+  convert isBounded_add isBounded_singleton (s := {-x}) hs using 1
+  ext y
+  simp
+
+@[simp]
+theorem tendsto_sub_const_cobounded (x : R) :
+    Tendsto (· - x) (cobounded R) (cobounded R) := by
+  simpa only [sub_eq_add_neg] using tendsto_add_const_cobounded (-x)
+
+@[simp]
+theorem tendsto_const_sub_cobounded (x : R) :
+    Tendsto (x - ·) (cobounded R) (cobounded R) := by
+  simpa only [sub_eq_add_neg] using (tendsto_const_add_cobounded x).comp tendsto_neg_cobounded
+
 end SeminormedAddCommGroup
 
 section NonUnitalSeminormedRing

Mathlib/Topology/Bornology/BoundedOperation.lean

@@ -1997,6 +1997,13 @@ Q2226650:
 
 Q2226677:
   title: Gelfand–Mazur theorem
+  decls:
+    - NormedRing.algEquivComplexOfComplete
+    - NormedAlgebra.Complex.algEquivOfNormMul
+    - NormedAlgebra.Real.nonempty_algEquiv_or
+  authors: Jireh Loreaux, Michael Stoll
+  date: 2021, 2025
+  comment: "The first two are over the complex numbers (with different assumptions), the third is over the real numbers."
 
 Q2226682:
   title: Gelfand–Naimark theorem

docs/1000.yaml

@@ -3922,6 +3922,23 @@ @Article{         orzech1971
   url           = {https://doi.org/10.2307/2316897}
 }
 
+@Article{         ostrowski1916,
+  author        = {Ostrowski, Alexander},
+  title         = {\"Uber einige {L}\"osungen der {F}unktionalgleichung
+                  {$\psi(x)\cdot\psi(x)=\psi(xy)$}},
+  journal       = {Acta Math.},
+  fjournal      = {Acta Mathematica},
+  volume        = {41},
+  year          = {1916},
+  number        = {1},
+  pages         = {271--284},
+  issn          = {0001-5962,1871-2509},
+  mrclass       = {99-04},
+  mrnumber      = {1555153},
+  doi           = {10.1007/BF02422947},
+  url           = {https://doi.org/10.1007/BF02422947}
+}
+
 @Article{         oudom_guin_2008,
   author        = {Oudom, J.-M. and Guin, D.},
   title         = {On the {Lie} enveloping algebra of a pre-{Lie} algebra},