Exact source: MathlibAnnex/Analysis/Normed/Module/EquivalentSeminorm/Topology.lean
Pinned GitHub source · Raw UTF-8 source
Back to A seminorm with two-sided bounds against a reference norm
1import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm2import Mathlib.Analysis.Normed.Module.FiniteDimension3import Mathlib.Topology.MetricSpace.Lipschitz45/-! # Topology and comparison estimates for equivalent seminorms -/67namespace MathlibAnnex.EquivalentSeminorm89open Set1011variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]12 [NormedAddCommGroup F] [NormedSpace ℝ F] (M : EquivalentSeminorm E)1314/-- The model unit ball is bounded for the reference norm. -/15theorem isBounded_closedUnitBall : Bornology.IsBounded M.closedUnitBall := by16 rw [Metric.isBounded_iff_subset_closedBall (0 : E)]17 refine ⟨1 / M.lower, ?_⟩18 intro x hx19 have hprod : M.lower * ‖x‖ ≤ 1 :=20 (M.lower_le x).trans (M.mem_closedUnitBall.mp hx)21 have hnorm : ‖x‖ ≤ 1 / M.lower := by22 apply (le_div_iff₀ M.lower_pos).223 nlinarith24 simpa [Metric.mem_closedBall, dist_eq_norm] using hnorm2526/-- Finite dimensional model unit balls are compact, including dimension zero. -/27theorem isCompact_closedUnitBall [FiniteDimensional ℝ E] :28 IsCompact M.closedUnitBall := by29 apply Metric.isCompact_of_isClosed_isBounded _ M.isBounded_closedUnitBall30 change IsClosed (M.p.closedBall 0 1)31 have h : M.p.closedBall 0 1 = {x : E | M.p x ≤ 1} := by ext x; simp32 rw [h]33 exact isClosed_le M.continuous_p continuous_const3435/-- The origin is an interior point of the model unit ball. -/36theorem zero_mem_interior_closedUnitBall : (0 : E) ∈ interior M.closedUnitBall := by37 rw [mem_interior_iff_mem_nhds]38 refine Filter.mem_of_superset39 (Metric.ball_mem_nhds (0 : E) (one_div_pos.mpr M.upper_pos)) ?_40 intro x hx41 have hnorm : ‖x‖ < 1 / M.upper := by42 simpa [Metric.mem_ball, dist_eq_norm] using hx43 have hprod : M.upper * ‖x‖ < 1 := by44 have := (lt_div_iff₀ M.upper_pos).1 hnorm45 nlinarith46 exact M.mem_closedUnitBall.mpr ((M.le_upper x).trans hprod.le)4748/-- A model increment bound gives the stored upper Lipschitz constant. -/49theorem lipschitzWith_upper_of_model_bound {f : E → F}50 (hf : ∀ x y, ‖f x - f y‖ ≤ M.p (x - y)) :51 LipschitzWith M.upper.toNNReal f := by52 refine LipschitzWith.of_dist_le_mul ?_53 intro x y54 calc55 dist (f x) (f y) = ‖f x - f y‖ := by simp [dist_eq_norm]56 _ ≤ M.p (x - y) := hf x y57 _ ≤ M.upper * ‖x - y‖ := M.le_upper (x - y)58 _ = (M.upper.toNNReal : ℝ) * dist x y := by59 rw [Real.coe_toNNReal M.upper M.upper_pos.le, dist_eq_norm]6061end MathlibAnnex.EquivalentSeminorm