polar_ball_subset_closedBall_div — Mathlib

English

For a scalar c with norm > 1 and radius r > 0, the polar of the ball is contained in a larger closed ball in the dual by the factor ||c||/r.

Русский

Для скалярa c с нормой > 1 и радиуса r > 0 полярBall содержится в большем замкнутом шаре двойственного пространства с множителем ||c||/r.

LaTeX

$$$1 < \\|c\\| \\Rightarrow \\forall r>0,\\; \\operatorname{polar}(ball(0,r)) \\subseteq closedBall(0, \\|c\\|/r)$$$

Lean4

theorem polar_ball_subset_closedBall_div {c : 𝕜} (hc : 1 < ‖c‖) {r : ℝ} (hr : 0 < r) :
    StrongDual.polar 𝕜 (ball (0 : E) r) ⊆ closedBall (0 : StrongDual 𝕜 E) (‖c‖ / r) :=
  by
  intro x' hx'
  rw [StrongDual.mem_polar_iff] at hx'
  simp only [mem_closedBall_zero_iff, mem_ball_zero_iff] at *
  have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr
  refine ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_
  calc
    ‖x' x‖ ≤ 1 := hx' _ h₂
    _ ≤ ‖c‖ / r * ‖x‖ := (inv_le_iff_one_le_mul₀' hcr).1 (by rwa [inv_div])

Похожие утверждения