feat(Normed/Field): completeSpace_iff_isComplete_closedBall (#15777)

On the way to locally complete K iff complete O(K) 
Also add some helper lemmas about uniform continuity of multiplication by a constant with a variant for rings (via smul) instead of UniformGroup (which fields are not).




Co-authored-by: Yakov Pechersky <[email protected]>
Co-authored-by: Yakov Pechersky <[email protected]>

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -14,6 +14,9 @@ import Mathlib.Data.Set.Pointwise.Interval
 
 In this file we define (semi)normed rings and fields. We also prove some theorems about these
 definitions.
+
+Some useful results that relate the topology of the normed field to the discrete topology include:
+* `norm_eq_one_iff_ne_zero_of_discrete`
 -/
 
 -- Guard against import creep.
@@ -669,6 +672,46 @@ theorem nndist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :
     nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊) :=
   NNReal.eq <| dist_inv_inv₀ hz hw
 
+namespace NormedDivisionRing
+
+section Discrete
+
+variable {𝕜 : Type*} [NormedDivisionRing 𝕜] [DiscreteTopology 𝕜]
+
+lemma norm_eq_one_iff_ne_zero_of_discrete {x : 𝕜} : ‖x‖ = 1 ↔ x ≠ 0 := by
+  constructor <;> intro hx
+  · contrapose! hx
+    simp [hx]
+  · have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}
+    simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this
+    obtain ⟨ε, εpos, h'⟩ := this
+    wlog h : ‖x‖ < 1 generalizing 𝕜 with H
+    · push_neg at h
+      rcases h.eq_or_lt with h|h
+      · rw [h]
+      replace h := norm_inv x ▸ inv_lt_one h
+      rw [← inv_inj, inv_one, ← norm_inv]
+      exact H (by simpa) h' h
+    obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h
+    rw [← norm_pow] at hk
+    specialize h' _ hk
+    simp [hx] at h'
+
+@[simp]
+lemma norm_le_one_of_discrete
+    (x : 𝕜) : ‖x‖ ≤ 1 := by
+  rcases eq_or_ne x 0 with rfl|hx
+  · simp
+  · simp [norm_eq_one_iff_ne_zero_of_discrete.mpr hx]
+
+lemma discreteTopology_unit_closedBall_eq_univ : (Metric.closedBall 0 1 : Set 𝕜) = Set.univ := by
+  ext
+  simp
+
+end Discrete
+
+end NormedDivisionRing
+
 end NormedDivisionRing
 
 /-- A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖. -/

Mathlib/Analysis/Normed/Field/Lemmas.lean

@@ -17,6 +17,11 @@ import Mathlib.Topology.MetricSpace.DilationEquiv
 # Normed fields
 
 In this file we continue building the theory of (semi)normed rings and fields.
+
+Some useful results that relate the topology of the normed field to the discrete topology include:
+* `discreteTopology_or_nontriviallyNormedField`
+* `discreteTopology_of_bddAbove_range_norm`
+
 -/
 
 -- Guard against import creep.
@@ -291,6 +296,32 @@ end NormedDivisionRing
 
 namespace NormedField
 
+/-- A normed field is either nontrivially normed or has a discrete topology.
+In the discrete topology case, all the norms are 1, by `norm_eq_one_iff_ne_zero_of_discrete`.
+The nontrivially normed field instance is provided by a subtype with a proof that the
+forgetful inheritance to the existing `NormedField` instance is definitionally true.
+This allows one to have the new `NontriviallyNormedField` instance without data clashes. -/
+lemma discreteTopology_or_nontriviallyNormedField (𝕜 : Type*) [h : NormedField 𝕜] :
+    DiscreteTopology 𝕜 ∨ Nonempty ({h' : NontriviallyNormedField 𝕜 // h'.toNormedField = h}) := by
+  by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
+  · exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩
+  · simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
+             sub_zero]
+    refine Or.inl ⟨1, zero_lt_one, ?_⟩
+    contrapose! H
+    refine H.imp ?_
+    -- contextual to reuse the `a ≠ 0` hypothesis in the proof of `a ≠ 0 ∧ ‖a‖ ≠ 1`
+    simp (config := {contextual := true}) [add_comm, ne_of_lt]
+
+lemma discreteTopology_of_bddAbove_range_norm {𝕜 : Type*} [NormedField 𝕜]
+    (h : BddAbove (Set.range fun k : 𝕜 ↦ ‖k‖)) :
+    DiscreteTopology 𝕜 := by
+  refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_
+  rintro ⟨_, rfl⟩
+  obtain ⟨x, h⟩ := h
+  obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x
+  exact hk.not_le (h (Set.mem_range_self k))
+
 section Densely
 
 variable (α) [DenselyNormedField α]
@@ -333,3 +364,31 @@ instance Rat.instDenselyNormedField : DenselyNormedField ℚ where
   lt_norm_lt r₁ r₂ h₀ hr :=
     let ⟨q, h⟩ := exists_rat_btwn hr
     ⟨q, by rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]⟩
+
+section Complete
+
+lemma NormedField.completeSpace_iff_isComplete_closedBall {K : Type*} [NormedField K] :
+    CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1 : Set K) := by
+  constructor <;> intro h
+  · exact Metric.isClosed_ball.isComplete
+  rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _|⟨_, rfl⟩
+  · rwa [completeSpace_iff_isComplete_univ,
+         ← NormedDivisionRing.discreteTopology_unit_closedBall_eq_univ]
+  refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
+  obtain ⟨k, hk⟩ := hu.norm_bddAbove
+  have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
+  obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k
+  have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
+  have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 := by
+    intro
+    simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
+    rw [div_le_one (kpos.trans_lt hx)]
+    exact hx.le.trans' (hk (by simp))
+  obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
+  refine ⟨a * x, (((continuous_mul_right x).tendsto a).comp ha').congr ?_⟩
+  have hx' : x ≠ 0 := by
+    contrapose! hx
+    simp [hx, kpos]
+  simp [div_mul_cancel₀ _ hx']
+
+end Complete

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -379,4 +379,17 @@ theorem cauchySeq_prod_of_eventually_eq {u v : ℕ → E} {N : ℕ} (huv : ∀ n
   intro m hm
   simp [huv m (le_of_lt hm)]
 
+@[to_additive CauchySeq.norm_bddAbove]
+lemma CauchySeq.mul_norm_bddAbove {G : Type*} [SeminormedGroup G] {u : ℕ → G}
+    (hu : CauchySeq u) : BddAbove (Set.range (fun n ↦ ‖u n‖)) := by
+  obtain ⟨C, -, hC⟩ := cauchySeq_bdd hu
+  simp_rw [SeminormedGroup.dist_eq] at hC
+  have : ∀ n, ‖u n‖ ≤ C + ‖u 0‖ := by
+    intro n
+    rw [add_comm]
+    refine (norm_le_norm_add_norm_div' (u n) (u 0)).trans ?_
+    simp [(hC _ _).le]
+  rw [bddAbove_def]
+  exact ⟨C + ‖u 0‖, by simpa using this⟩
+
 end SeminormedCommGroup

Mathlib/Topology/Algebra/UniformGroup.lean

@@ -93,6 +93,33 @@ theorem UniformContinuous.mul [UniformSpace β] {f : β → α} {g : β → α}
 theorem uniformContinuous_mul : UniformContinuous fun p : α × α => p.1 * p.2 :=
   uniformContinuous_fst.mul uniformContinuous_snd
 
+@[to_additive]
+theorem UniformContinuous.mul_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
+    (a : α) : UniformContinuous fun x ↦ f x * a :=
+  hf.mul uniformContinuous_const
+
+@[to_additive]
+theorem UniformContinuous.const_mul [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
+    (a : α) : UniformContinuous fun x ↦ a * f x :=
+  uniformContinuous_const.mul hf
+
+@[to_additive]
+theorem uniformContinuous_mul_left (a : α) : UniformContinuous fun b : α => a * b :=
+  uniformContinuous_id.const_mul _
+
+@[to_additive]
+theorem uniformContinuous_mul_right (a : α) : UniformContinuous fun b : α => b * a :=
+  uniformContinuous_id.mul_const _
+
+@[to_additive]
+theorem UniformContinuous.div_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
+    (a : α) : UniformContinuous fun x ↦ f x / a :=
+  hf.div uniformContinuous_const
+
+@[to_additive]
+theorem uniformContinuous_div_const (a : α) : UniformContinuous fun b : α => b / a :=
+  uniformContinuous_id.div_const _
+
 @[to_additive UniformContinuous.const_nsmul]
 theorem UniformContinuous.pow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
     ∀ n : ℕ, UniformContinuous fun x => f x ^ n

Mathlib/Topology/Algebra/UniformMulAction.lean

@@ -116,6 +116,39 @@ instance UniformGroup.to_uniformContinuousConstSMul {G : Type u} [Group G] [Unif
     [UniformGroup G] : UniformContinuousConstSMul G G :=
   ⟨fun _ => uniformContinuous_const.mul uniformContinuous_id⟩
 
+section Ring
+
+variable {R β : Type*} [Ring R] [UniformSpace R] [UniformSpace β]
+
+theorem UniformContinuous.const_mul' [UniformContinuousConstSMul R R] {f : β → R}
+    (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ a * f x :=
+  hf.const_smul a
+
+theorem UniformContinuous.mul_const' [UniformContinuousConstSMul Rᵐᵒᵖ R] {f : β → R}
+    (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ f x * a :=
+  hf.const_smul (MulOpposite.op a)
+
+theorem uniformContinuous_mul_left' [UniformContinuousConstSMul R R] (a : R) :
+    UniformContinuous fun b : R => a * b :=
+  uniformContinuous_id.const_mul' _
+
+theorem uniformContinuous_mul_right' [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) :
+    UniformContinuous fun b : R => b * a :=
+  uniformContinuous_id.mul_const' _
+
+theorem UniformContinuous.div_const' {R β : Type*} [DivisionRing R] [UniformSpace R]
+    [UniformContinuousConstSMul Rᵐᵒᵖ R] [UniformSpace β] {f : β → R}
+    (hf : UniformContinuous f) (a : R) :
+    UniformContinuous fun x ↦ f x / a := by
+  simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹
+
+theorem uniformContinuous_div_const' {R : Type*} [DivisionRing R] [UniformSpace R]
+    [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) :
+    UniformContinuous fun b : R => b / a :=
+  uniformContinuous_id.div_const' _
+
+end Ring
+
 namespace UniformSpace
 
 namespace Completion