Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(NormedSpace/Basic): move some theorems to
NormedSpace.Real (#…
…10206) This way we don't switch between general normed spaces and real normed spaces back and forth throughout the file.
- Loading branch information
Showing
14 changed files
with
176 additions
and
145 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,168 @@ | ||
| /- | ||
| Copyright (c) 2020 Yury Kudryashov. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Yury Kudryashov, Patrick Massot, Eric Wieser, Yaël Dillies | ||
| -/ | ||
| import Mathlib.Analysis.NormedSpace.Basic | ||
| import Mathlib.Topology.Algebra.Module.Basic | ||
|
|
||
| #align_import analysis.normed_space.basic from "leanprover-community/mathlib"@"bc91ed7093bf098d253401e69df601fc33dde156" | ||
|
|
||
| /-! | ||
| # Basic facts about real (semi)normed spaces | ||
| In this file we prove some theorems about (semi)normed spaces over real numberes. | ||
| ## Main results | ||
| - `closure_ball`, `frontier_ball`, `interior_closedBall`, `frontier_closedBall`, `interior_sphere`, | ||
| `frontier_sphere`: formulas for the closure/interior/frontier | ||
| of nontrivial balls and spheres in a real seminormed space; | ||
| - `interior_closedBall'`, `frontier_closedBall'`, `interior_sphere'`, `frontier_sphere'`: | ||
| similar lemmas assuming that the ambient space is separated and nontrivial instead of `r ≠ 0`. | ||
| -/ | ||
|
|
||
| open Metric Set Function Filter | ||
| open scoped NNReal Topology | ||
|
|
||
| /-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points. | ||
| This is a particular case of `Module.punctured_nhds_neBot`. -/ | ||
| instance Real.punctured_nhds_module_neBot {E : Type*} [AddCommGroup E] [TopologicalSpace E] | ||
| [ContinuousAdd E] [Nontrivial E] [Module ℝ E] [ContinuousSMul ℝ E] (x : E) : NeBot (𝓝[≠] x) := | ||
| Module.punctured_nhds_neBot ℝ E x | ||
| #align real.punctured_nhds_module_ne_bot Real.punctured_nhds_module_neBot | ||
|
|
||
| section Seminormed | ||
|
|
||
| variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E] | ||
|
|
||
| theorem inv_norm_smul_mem_closed_unit_ball (x : E) : | ||
| ‖x‖⁻¹ • x ∈ closedBall (0 : E) 1 := by | ||
| simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul, | ||
| div_self_le_one] | ||
| #align inv_norm_smul_mem_closed_unit_ball inv_norm_smul_mem_closed_unit_ball | ||
|
|
||
| theorem norm_smul_of_nonneg {t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖ := by | ||
| rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht] | ||
| #align norm_smul_of_nonneg norm_smul_of_nonneg | ||
|
|
||
| theorem dist_smul_add_one_sub_smul_le {r : ℝ} {x y : E} (h : r ∈ Icc 0 1) : | ||
| dist (r • x + (1 - r) • y) x ≤ dist y x := | ||
| calc | ||
| dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖ := by | ||
| simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add, | ||
| sub_right_comm] | ||
| _ = (1 - r) * dist y x := by | ||
| rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm'] | ||
| _ ≤ (1 - 0) * dist y x := by gcongr; exact h.1 | ||
| _ = dist y x := by rw [sub_zero, one_mul] | ||
|
|
||
| theorem closure_ball (x : E) {r : ℝ} (hr : r ≠ 0) : closure (ball x r) = closedBall x r := by | ||
| refine' Subset.antisymm closure_ball_subset_closedBall fun y hy => _ | ||
| have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 := | ||
| ((continuous_id.smul continuous_const).add continuous_const).continuousWithinAt | ||
| convert this.mem_closure _ _ | ||
| · rw [one_smul, sub_add_cancel] | ||
| · simp [closure_Ico zero_ne_one, zero_le_one] | ||
| · rintro c ⟨hc0, hc1⟩ | ||
| rw [mem_ball, dist_eq_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, abs_of_nonneg hc0, | ||
| mul_comm, ← mul_one r] | ||
| rw [mem_closedBall, dist_eq_norm] at hy | ||
| replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm | ||
| apply mul_lt_mul' <;> assumption | ||
| #align closure_ball closure_ball | ||
|
|
||
| theorem frontier_ball (x : E) {r : ℝ} (hr : r ≠ 0) : | ||
| frontier (ball x r) = sphere x r := by | ||
| rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball] | ||
| #align frontier_ball frontier_ball | ||
|
|
||
| theorem interior_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) : | ||
| interior (closedBall x r) = ball x r := by | ||
| cases' hr.lt_or_lt with hr hr | ||
| · rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty] | ||
| refine' Subset.antisymm _ ball_subset_interior_closedBall | ||
| intro y hy | ||
| rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl) | ||
| · exact hr | ||
| set f : ℝ → E := fun c : ℝ => c • (y - x) + x | ||
| suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by | ||
| have hfc : Continuous f := (continuous_id.smul continuous_const).add continuous_const | ||
| have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa | ||
| have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) := | ||
| interior_mono this (preimage_interior_subset_interior_preimage hfc hf1) | ||
| contrapose h1 | ||
| simp | ||
| intro c hc | ||
| rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_right hr] | ||
| simpa [dist_eq_norm, norm_smul] using hc | ||
| #align interior_closed_ball interior_closedBall | ||
|
|
||
| theorem frontier_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) : | ||
| frontier (closedBall x r) = sphere x r := by | ||
| rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball] | ||
| #align frontier_closed_ball frontier_closedBall | ||
|
|
||
| theorem interior_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : interior (sphere x r) = ∅ := by | ||
| rw [← frontier_closedBall x hr, interior_frontier isClosed_ball] | ||
| #align interior_sphere interior_sphere | ||
|
|
||
| theorem frontier_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (sphere x r) = sphere x r := by | ||
| rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty] | ||
| #align frontier_sphere frontier_sphere | ||
|
|
||
| end Seminormed | ||
|
|
||
| section Normed | ||
|
|
||
| variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] | ||
|
|
||
| section Surj | ||
|
|
||
| variable (E) | ||
|
|
||
| theorem exists_norm_eq {c : ℝ} (hc : 0 ≤ c) : ∃ x : E, ‖x‖ = c := by | ||
| rcases exists_ne (0 : E) with ⟨x, hx⟩ | ||
| rw [← norm_ne_zero_iff] at hx | ||
| use c • ‖x‖⁻¹ • x | ||
| simp [norm_smul, Real.norm_of_nonneg hc, abs_of_nonneg hc, inv_mul_cancel hx] | ||
| #align exists_norm_eq exists_norm_eq | ||
|
|
||
| @[simp] | ||
| theorem range_norm : range (norm : E → ℝ) = Ici 0 := | ||
| Subset.antisymm (range_subset_iff.2 norm_nonneg) fun _ => exists_norm_eq E | ||
| #align range_norm range_norm | ||
|
|
||
| theorem nnnorm_surjective : Surjective (nnnorm : E → ℝ≥0) := fun c => | ||
| (exists_norm_eq E c.coe_nonneg).imp fun _ h => NNReal.eq h | ||
| #align nnnorm_surjective nnnorm_surjective | ||
|
|
||
| @[simp] | ||
| theorem range_nnnorm : range (nnnorm : E → ℝ≥0) = univ := | ||
| (nnnorm_surjective E).range_eq | ||
| #align range_nnnorm range_nnnorm | ||
|
|
||
| end Surj | ||
|
|
||
| theorem interior_closedBall' (x : E) (r : ℝ) : interior (closedBall x r) = ball x r := by | ||
| rcases eq_or_ne r 0 with (rfl | hr) | ||
| · rw [closedBall_zero, ball_zero, interior_singleton] | ||
| · exact interior_closedBall x hr | ||
| #align interior_closed_ball' interior_closedBall' | ||
|
|
||
| theorem frontier_closedBall' (x : E) (r : ℝ) : frontier (closedBall x r) = sphere x r := by | ||
| rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball] | ||
| #align frontier_closed_ball' frontier_closedBall' | ||
|
|
||
| @[simp] | ||
| theorem interior_sphere' (x : E) (r : ℝ) : interior (sphere x r) = ∅ := by | ||
| rw [← frontier_closedBall' x, interior_frontier isClosed_ball] | ||
| #align interior_sphere' interior_sphere' | ||
|
|
||
| @[simp] | ||
| theorem frontier_sphere' (x : E) (r : ℝ) : frontier (sphere x r) = sphere x r := by | ||
| rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty] | ||
| #align frontier_sphere' frontier_sphere' | ||
|
|
||
| end Normed |
Oops, something went wrong.