Exact source: MathlibAnnex/Analysis/Normed/Module/EquivalentSeminorm.lean
Pinned GitHub source · Raw UTF-8 source
Back to A seminorm with two-sided bounds against a reference norm
1import Mathlib.Analysis.Seminorm2import Mathlib.Analysis.Normed.Module.Basic3import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap4import Mathlib.Tactic.Linarith56/-!7# Seminorms quantitatively equivalent to a reference norm89The reference norm stays on the carrier. The eight fields store a real seminorm,10two positive comparison constants, both inequalities, and continuity.11-/1213namespace MathlibAnnex1415/-- A continuous seminorm with explicit positive lower and upper norm comparisons. -/16structure EquivalentSeminorm (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] where17 p : Seminorm ℝ E18 lower : ℝ19 upper : ℝ20 lower_pos : 0 < lower21 upper_pos : 0 < upper22 lower_le : ∀ x, lower * ‖x‖ ≤ p x23 le_upper : ∀ x, p x ≤ upper * ‖x‖24 continuous_p : Continuous p2526namespace EquivalentSeminorm2728variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]29 [NormedAddCommGroup F] [NormedSpace ℝ F] (M : EquivalentSeminorm E)3031/-- The closed unit ball of the stored seminorm, on the reference carrier. -/32def closedUnitBall : Set E := M.p.closedBall 0 13334/-- The unit sphere of the stored seminorm, on the reference carrier. -/35def unitSphere : Set E := {x | M.p x = 1}3637@[simp] theorem mem_closedUnitBall {x : E} : x ∈ M.closedUnitBall ↔ M.p x ≤ 1 := by38 simp [closedUnitBall]3940@[simp] theorem mem_unitSphere {x : E} : x ∈ M.unitSphere ↔ M.p x = 1 := Iff.rfl4142@[simp] theorem zero_mem_closedUnitBall : (0 : E) ∈ M.closedUnitBall := by43 simp [closedUnitBall]4445theorem closedUnitBall_nonempty : M.closedUnitBall.Nonempty :=46 ⟨0, M.zero_mem_closedUnitBall⟩4748/-- The positive lower comparison makes the seminorm definite. -/49theorem eq_zero_of_apply_eq_zero {x : E} (hx : M.p x = 0) : x = 0 := by50 have h : M.lower * ‖x‖ ≤ 0 := by simpa [hx] using M.lower_le x51 have hnorm : ‖x‖ = 0 := by52 have hn : 0 ≤ ‖x‖ := norm_nonneg x53 nlinarith [M.lower_pos]54 exact norm_eq_zero.mp hnorm5556/-- A continuous linear map bounded pointwise by the model seminorm. -/57def IsContraction (A : E →L[ℝ] F) : Prop := ∀ x, ‖A x‖ ≤ M.p x5859@[simp] theorem isContraction_zero : M.IsContraction (0 : E →L[ℝ] F) := by60 intro x61 simp6263/-- The set of all continuous linear contractions for the model seminorm. -/64def contractionSet (F : Type*) [NormedAddCommGroup F] [NormedSpace ℝ F] :65 Set (E →L[ℝ] F) := {A | M.IsContraction A}6667@[simp] theorem mem_contractionSet {A : E →L[ℝ] F} :68 A ∈ M.contractionSet F ↔ M.IsContraction A := Iff.rfl6970end EquivalentSeminorm71end MathlibAnnex