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/normed_space/operator_norm): add 2 new versions of op_norm_le_* #15417

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/operator_norm): add 2 new versions of op_norm_le_* #15417

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
da58809
feat(analysis/normed_space/operator_norm): add 2 new versions of `op_…
urkud Jul 16, 2022
a02da7a
Merge branch 'master' into YK-op-norm-le
urkud Jul 18, 2022
372d4fa
Add some `nnnorm` versions.
urkud Jul 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
38 changes: 31 additions & 7 deletions src/analysis/normed_space/operator_norm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,13 @@ lemma op_norm_le_bound (f : E →SL[σ₁₂] F) {M : ℝ} (hMp: 0 ≤ M) (hM :
∥f∥ ≤ M :=
cInf_le bounds_bdd_below ⟨hMp, hM⟩

/-- If one controls the norm of every `A x`, `∥x∥ ≠ 0`, then one controls the norm of `A`. -/
lemma op_norm_le_bound' (f : E →SL[σ₁₂] F) {M : ℝ} (hMp: 0 ≤ M)
(hM : ∀ x, ∥x∥ ≠ 0 → ∥f x∥ ≤ M * ∥x∥) :
∥f∥ ≤ M :=
op_norm_le_bound f hMp $ λ x, (ne_or_eq (∥x∥) 0).elim (hM x) $
λ h, by simp only [h, mul_zero, norm_image_of_norm_zero f f.2 h]

theorem op_norm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : lipschitz_with K f) :
∥f∥ ≤ K :=
f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0
Expand Down Expand Up @@ -301,13 +308,7 @@ mul_one ∥f∥ ▸ f.le_op_norm_of_le
lemma op_norm_le_of_shell {f : E →SL[σ₁₂] F} {ε C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
{c : 𝕜} (hc : 1 < ∥c∥) (hf : ∀ x, ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥f x∥ ≤ C * ∥x∥) :
∥f∥ ≤ C :=
begin
refine f.op_norm_le_bound hC (λ x, _),
by_cases hx : ∥x∥ = 0,
{ rw [hx, mul_zero],
exact le_of_eq (norm_image_of_norm_zero f f.2 hx) },
exact semilinear_map_class.bound_of_shell_semi_normed f ε_pos hc hf hx
end
f.op_norm_le_bound' hC $ λ x hx, semilinear_map_class.bound_of_shell_semi_normed f ε_pos hc hf hx

lemma op_norm_le_of_ball {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
(hf : ∀ x ∈ ball (0 : E) ε, ∥f x∥ ≤ C * ∥x∥) : ∥f∥ ≤ C :=
Expand Down Expand Up @@ -335,6 +336,18 @@ begin
rwa [norm_inv, div_eq_mul_inv, inv_inv] }
end

/-- For a continuous real linear map `f`, if one controls the norm of every `f x`, `∥x∥ = 1`, then
one controls the norm of `f`. -/
lemma op_norm_le_of_unit_norm [normed_space ℝ E] [normed_space ℝ F] {f : E →L[ℝ] F} {C : ℝ}
(hC : 0 ≤ C) (hf : ∀ x, ∥x∥ = 1 → ∥f x∥ ≤ C) : ∥f∥ ≤ C :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that the file normed_space.is_R_or_C precisely exists for the purpose of having is_R_or_C-scalars-specific facts about normed spaces. Can you move to there, generalize to scalars is_R_or_C, and rewrite to use the lemma norm_smul_inv_norm already existing there? Here's a first version, you can probably golf it further :)

lemma op_norm_le_of_unit_norm  {f : E →L[𝕜] F} {C : ℝ}
  (hC : 0 ≤ C) (hf : ∀ x, ∥x∥ = 1 → ∥f x∥ ≤ C) : ∥f∥ ≤ C :=
begin
  refine f.op_norm_le_bound' hC (λ x hx, _),
  have H₁ : ∥((∥x∥⁻¹ : 𝕜) • x)∥ = 1 := norm_smul_inv_norm (by simpa using hx),
  have H₂ := hf _ H₁,
  rwa [map_smul, norm_smul, norm_inv, is_R_or_C.norm_coe_norm, ← div_eq_inv_mul, div_le_iff] at H₂,
  exact (norm_nonneg x).lt_of_ne' hx,
end

Same for the nnnorm version.

(I just noticed that actually, over in that file, there is a lemma op_norm_bound_of_ball_bound which looks like it should work for a nondiscrete normed field, but that's a discussion for another day ...)

Copy link
Member Author

@urkud urkud Jul 19, 2022 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A normed space over an is_R_or_C is a normed space over reals, isn't it? Or it needs a letI? Also, your proof needs a normed_group while my proof works for a semi_normed_group.

If I generalize it to is_R_or_C, then the field should be an explicit argument in the lemma. Am I right?

begin
refine op_norm_le_bound' f hC (λ x hx, _),
have H₁ : ∥(∥x∥⁻¹ • x)∥ = 1, by rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel hx],
have H₂ := hf _ H₁,
rwa [map_smul, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul, div_le_iff] at H₂,
exact (norm_nonneg x).lt_of_ne' hx
end

/-- The operator norm satisfies the triangle inequality. -/
theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
(f + g).op_norm_le_bound (add_nonneg f.op_norm_nonneg g.op_norm_nonneg) $
Expand Down Expand Up @@ -385,6 +398,17 @@ lemma op_nnnorm_le_bound (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x,
∥f∥₊ ≤ M :=
op_norm_le_bound f (zero_le M) hM

/-- If one controls the norm of every `A x`, `∥x∥₊ ≠ 0`, then one controls the norm of `A`. -/
lemma op_nnnorm_le_bound' (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ∥x∥₊ ≠ 0 → ∥f x∥₊ ≤ M * ∥x∥₊) :
∥f∥₊ ≤ M :=
op_norm_le_bound' f (zero_le M) $ λ x hx, hM x $ by rwa [← nnreal.coe_ne_zero]

/-- For a continuous real linear map `f`, if one controls the norm of every `f x`, `∥x∥₊ = 1`, then
one controls the norm of `f`. -/
lemma op_nnnorm_le_of_unit_nnnorm [normed_space ℝ E] [normed_space ℝ F] {f : E →L[ℝ] F} {C : ℝ≥0}
(hf : ∀ x, ∥x∥₊ = 1 → ∥f x∥₊ ≤ C) : ∥f∥₊ ≤ C :=
op_norm_le_of_unit_norm C.coe_nonneg $ λ x hx, hf x $ by rwa [← nnreal.coe_eq_one]

theorem op_nnnorm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : lipschitz_with K f) :
∥f∥₊ ≤ K :=
op_norm_le_of_lipschitz hf
Expand Down