linear_map_bound_of_ball_bound

Stream: Is there code for X?

[Kalle Kytölä]

Do the following exist? Can they be proven under meaningful more general assumptions than [is_R_or_C 𝕜]?

import tactic
import analysis.normed_space.dual

open metric

variables {𝕜 : Type*} [is_R_or_C 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]

lemma linear_map_bound_of_sphere_bound
  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
  (h : ∀ z ∈ sphere (0 : E) r, ∥ f z ∥ ≤ c) (z : E) :
  ∥ f z ∥ ≤ c / r * ∥ z ∥ := sorry

lemma linear_map_bound_of_ball_bound
  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
  (h : ∀ z ∈ closed_ball (0 : E) r, ∥ f z ∥ ≤ c) :
  ∀ (z : E), ∥ f z ∥ ≤ c / r * ∥ z ∥ := sorry

[Kalle Kytölä]

I am asking because in a proof of the Banach-Alaoglu theorem I had to resort to the following very clumsy way... Something better should exist, right?

import tactic
import analysis.normed_space.dual

open metric

variables {𝕜 : Type*} [is_R_or_C 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]

lemma linear_map_bound_of_sphere_bound
  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
  (h : ∀ z ∈ sphere (0 : E) r, ∥ f z ∥ ≤ c) (z : E) : ∥ f z ∥ ≤ c / r * ∥ z ∥ :=
begin
  by_cases z_zero : z = 0,
  { rw z_zero, simp only [linear_map.map_zero, norm_zero, mul_zero], },
  have norm_z_eq : ∥(∥ z ∥ : 𝕜)∥ =  ∥ z ∥ := norm_norm' 𝕜 E z,
  have norm_r_eq : ∥(r : 𝕜)∥ = r,
  { rw [is_R_or_C.norm_eq_abs, is_R_or_C.abs_of_real],
    exact abs_of_pos r_pos, },
  set z₁ := (r * ∥ z ∥⁻¹ : 𝕜) • z with hz₁,
  have norm_f_z₁ : ∥ f z₁ ∥ ≤ c,
  { apply h z₁,
    rw [mem_sphere_zero_iff_norm, hz₁, norm_smul, normed_field.norm_mul],
    simp only [normed_field.norm_inv],
    rw [norm_z_eq, mul_assoc, inv_mul_cancel (norm_pos_iff.mpr z_zero).ne.symm, mul_one],
    unfold_coes,
    simp only [norm_algebra_map_eq, ring_hom.to_fun_eq_coe],
    exact abs_of_pos r_pos, },
  have r_ne_zero : (r : 𝕜) ≠ 0 := (algebra_map ℝ 𝕜).map_ne_zero.mpr r_pos.ne.symm,
  have eq : f z = ∥ z ∥ / r * (f z₁),
  { rw [hz₁, linear_map.map_smul, smul_eq_mul],
    rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul],
    simp only [z_zero, is_R_or_C.of_real_eq_zero, norm_eq_zero, ne.def, not_false_iff], },
  rw [eq, normed_field.norm_mul, normed_field.norm_div, norm_z_eq, norm_r_eq,
      div_mul_eq_mul_div, div_mul_eq_mul_div, mul_comm],
  apply div_le_div _ _ r_pos rfl.ge,
  { exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z), },
  apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁),
end

lemma linear_map_bound_of_ball_bound
  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
  (h : ∀ z ∈ closed_ball (0 : E) r, ∥ f z ∥ ≤ c) :
  ∀ (z : E), ∥ f z ∥ ≤ c / r * ∥ z ∥ :=
begin
  apply linear_map_bound_of_sphere_bound r_pos c f,
  exact λ z hz, h z hz.le,
end

[Patrick Massot]

There is stuff that is at least related to this in src/analysis/normed_space/operator_norm.lean. Search for shell

[Sebastien Gouezel]

docs#continuous_linear_map.op_norm_le_of_ball

[Sebastien Gouezel]

Sorry, it's not the right form, it assumes a bound ∥f x∥ ≤ C * ∥x∥.

[Kalle Kytölä]

I had found linear_map.bound_of_shell, which is indeed morally quite similar to the linear_map_bound_of_sphere_bound above, and which works more generally under the assumption [nondiscrete_normed_field 𝕜]. By contrast, I don't think linear_map_bound_of_sphere_bound would work in this generality, since one can't necessarily rescale by exactly the norm (there might not be scalars of the desired norm). I also didn't find great ways of using these "shell"-lemmas for my purpose. (Although I must say that after I decided to give up the generality of [nondiscrete_normed_field 𝕜], I also didn't try hard to use the "shell"-lemmas, as they appear overly complicated for 𝕜=ℝ or 𝕜=ℂ).

[Kalle Kytölä]

So I believe linear_map_bound_of_sphere_bound is useful when 𝕜=ℝ or 𝕜=ℂ. But I do view linear_map_bound_of_ball_bound more fundamental, and it is not as obvious that it doesn't generalize. That said, with some trying I failed to generalize it to [nondiscrete_normed_field 𝕜] --- I never work with such fields, but e.g. one property that I would have liked was ∥ n • x ∥ = n * ∥ x ∥ for n : ℕ and x : 𝕜, which obviously fails for positive characteristic... This is partly why I asked for meaningful generalizations of the second lemma --- perhaps there are people to whom positive characteristic nondiscrete normed fields exist (to me they very nearly don't :stuck_out_tongue_wink:).

[Sebastien Gouezel]

linear_map_bound_of_ball_bound is not true over a general nondiscrete normed field, for the same reason as the shell one. Think of the case where there is no element of norm between 1 and 2. Then if you have the assumptions of your lemma with r = 3/2, in fact it is only speaking of points in the ball of radius 1.

[Sebastien Gouezel]

Probably the right way to state general lemmas is to introduce a quantity a which would be the infimum of the norms of elements of norm > 1, and get statements in term of this (where there would be a loss of a constant compared to the real or complex case, which would be exactly a). But it also makes sense to just state and prove your lemmas over is_R_or_C, I think.

[Kalle Kytölä]

Thank you @Sebastien Gouezel!

If these lemmas are done assuming [is_R_or_C 𝕜] then my question is a golfing challenge :golf:.

[Kalle Kytölä]

[EDIT: Sorry, what I say below doesn't show what I said it did...]

Sebastien Gouezel said:

linear_map_bound_of_ball_bound is not true over a general nondiscrete normed field, for the same reason as the shell one. Think of the case where there is no element of norm between 1 and 2. Then if you have the assumptions of your lemma with r = 3/2, in fact it is only speaking of points in the ball of radius 1.

This one I didn't quite understand... I thought [EDIT: incorrectly] that the combination of the following shows that there are always elements of norm between $1$ and $1+\varepsilon$ for any $\varepsilon > 0$:

example (𝕜 : Type*) [nondiscrete_normed_field 𝕜]  (x : 𝕜) (x_ne_zero : x ≠ 0) :
  ∥ x⁻¹ ∥ = ∥ x ∥⁻¹ := normed_field.norm_inv _

example (𝕜 : Type*) [nondiscrete_normed_field 𝕜] (ε : ℝ) (ε_pos : 0 < ε) :
  ∃ (x : 𝕜), 1 - ε < ∥ x ∥ ∧ ∥ x ∥ < 1 + ε :=
begin
  rcases normed_field.exists_norm_lt 𝕜 ε_pos with ⟨z, ⟨norm_z_pos, norm_z_lt⟩⟩,
  use 1+z,
  split,
  { have key := le_trans (le_abs_self (∥(1 : 𝕜)∥ - ∥-z∥)) (abs_norm_sub_norm_le (1 : 𝕜) (-z)),
    simp at key,
    apply lt_of_lt_of_le _ key,
    linarith, },
  { apply lt_of_le_of_lt (norm_add_le (1 : 𝕜) z) _,
    simp,
    assumption, },
end

But as I said, I don't really work with nondiscrete normed fields that do not satisfy the assumption [is_R_or_C 𝕜].

[Kalle Kytölä]

Sorry about the above thoughtless post.

Anyway, following Sébastien's comment that [is_R_or_C 𝕜]-generality makes some sense, I think I will soon PR the Banach-Alaoglu. Golfing the lemmas in that generality will then anyway be done either before or during the review...

(Actually, perhaps Banach-Alaoglu holds under weaker assumptions than [is_R_or_C 𝕜]. How about [nondiscrete_normed_field 𝕜] [proper_space 𝕜]? Anyways, I think I have formally proven that I am confused about such fields, so someone else can generalize later :smile:.)

[Kalle Kytölä]

#9827

In order to keep the review more manageable to both me and the reviewers, I separated the above lemmas from the Banach-Alaoglu PR. Very sorry that I did not manage to get nicer proofs yet! I hope someone generous reviewer is willing to help golf them (provided they are deemed worthy in mathlib in the first place). Thank you in advance!