Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(Analysis/Seminorm): add more *ball_smul_*ball #8724

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(Analysis/Seminorm): add more *ball_smul_*ball #8724

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 31 additions & 25 deletions Mathlib/Analysis/Seminorm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -919,31 +919,6 @@ theorem closedBall_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x :
exact closedBall_finset_sup_eq_iInter _ _ _ hr
#align seminorm.closed_ball_finset_sup Seminorm.closedBall_finset_sup

theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
rw [Set.subset_def]
intro x hx
rw [Set.mem_smul] at hx
rcases hx with ⟨a, y, ha, hy, hx⟩
rw [← hx, mem_ball_zero, map_smul_eq_mul]
gcongr
· exact mem_ball_zero_iff.mp ha
· exact p.mem_ball_zero.mp hy
#align seminorm.ball_smul_ball Seminorm.ball_smul_ball

theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) := by
rw [Set.subset_def]
intro x hx
rw [Set.mem_smul] at hx
rcases hx with ⟨a, y, ha, hy, hx⟩
rw [← hx, mem_closedBall_zero, map_smul_eq_mul]
rw [mem_closedBall_zero_iff] at ha
gcongr
· exact (norm_nonneg a).trans ha
· exact p.mem_closedBall_zero.mp hy
#align seminorm.closed_ball_smul_closed_ball Seminorm.closedBall_smul_closedBall

@[simp]
theorem ball_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r ≤ 0) : p.ball x r = ∅ := by
ext
Expand All @@ -959,6 +934,37 @@ theorem closedBall_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r <
exact hr.trans_le (map_nonneg _ _)
#align seminorm.closed_ball_eq_emptyset Seminorm.closedBall_eq_emptyset

theorem closedBall_smul_ball (p : Seminorm 𝕜 E) {r₁ : ℝ} (hr₁ : r₁ ≠ 0) (r₂ : ℝ) :
Metric.closedBall (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
refine fun a ha b hb ↦ mul_lt_mul' ha hb (map_nonneg _ _) ?_
exact hr₁.lt_or_lt.resolve_left <| ((norm_nonneg a).trans ha).not_lt

theorem ball_smul_closedBall (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ} (hr₂ : r₂ ≠ 0) :
Metric.ball (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
map_smul_eq_mul]
intro a ha b hb
rw [mul_comm, mul_comm r₁]
refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_lt.resolve_left ?_)
exact ((map_nonneg p b).trans hb).not_lt

theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) := by
rcases eq_or_ne r₂ 0 with rfl | hr₂
· simp
· exact (smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans
(ball_smul_closedBall _ _ hr₂)
#align seminorm.ball_smul_ball Seminorm.ball_smul_ball

theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) := by
simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
intro a ha b hb
gcongr
exact (norm_nonneg _).trans ha
#align seminorm.closed_ball_smul_closed_ball Seminorm.closedBall_smul_closedBall

-- Porting note: TODO: make that an `iff`
theorem neg_mem_ball_zero (r : ℝ) (hx : x ∈ ball p 0 r) : -x ∈ ball p 0 r := by
simpa only [mem_ball_zero, map_neg_eq_map] using hx
Expand Down
Loading