[Merged by Bors] - feat(analysis/normed_space/operator_norm): add 2 new versions of op_norm_le_*
#15417
Conversation
…norm_le_*` * `continuous_linear_map.op_norm_le_bound'` requires an estimate on `∥f x∥` for any `x`, `∥x∥ ≠ 0`; * `continuous_linear_map.op_norm_le_of_unit_norm` works only for real linear map and requires that `∥f x∥ ≤ C` for all `x`, `∥x∥ = 1`.
urkud
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
|
@eric-wieser Done. |
| /-- 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 := |
There was a problem hiding this comment.
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,
endSame 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 ...)
There was a problem hiding this comment.
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?
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
@hrmacbeth I'm going to merge this PR as is. The first time we'll need it for |
|
bors merge |
github-actions
bot
added
the
ready-to-merge
…norm_le_*` (#15417) * `continuous_linear_map.op_norm_le_bound'` requires an estimate on `∥f x∥` for any `x`, `∥x∥ ≠ 0`; * `continuous_linear_map.op_norm_le_of_unit_norm` works only for real linear map and requires that `∥f x∥ ≤ C` for all `x`, `∥x∥ = 1`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
op_norm_le_*op_norm_le_*
…norm_le_*` (#15417) * `continuous_linear_map.op_norm_le_bound'` requires an estimate on `∥f x∥` for any `x`, `∥x∥ ≠ 0`; * `continuous_linear_map.op_norm_le_of_unit_norm` works only for real linear map and requires that `∥f x∥ ≤ C` for all `x`, `∥x∥ = 1`.
continuous_linear_map.op_norm_le_bound'requires an estimate on∥f x∥for anyx,∥x∥ ≠ 0;continuous_linear_map.op_norm_le_of_unit_normworks only for reallinear map and requires that
∥f x∥ ≤ Cfor allx,∥x∥ = 1.