English
If r is strictly less than the operator NN-norm of f, there exists x with ‖x‖₊ < 1 such that r < ‖f x‖₊.
Русский
Если r < ‖f‖₊, тогда существует x с ‖x‖₊ < 1 и r < ‖f x‖₊.
LaTeX
$$Exists x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊$$
Lean4
theorem exists_lt_apply_of_lt_opNNNorm (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) : ∃ x : E, ‖x‖₊ < 1 ∧ r < ‖f x‖₊ :=
by
obtain ⟨y, hy⟩ := f.exists_mul_lt_apply_of_lt_opNNNorm hr
have hy' : ‖y‖₊ ≠ 0 := nnnorm_ne_zero_iff.2 fun heq => by simp [heq, nnnorm_zero, map_zero] at hy
have hfy : ‖f y‖₊ ≠ 0 := (zero_le'.trans_lt hy).ne'
rw [← inv_inv ‖f y‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm ‖y‖₊, ← mul_assoc, ←
NNReal.lt_inv_iff_mul_lt hy'] at hy
obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 hy
refine ⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, ?_⟩
rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv, RingHomIsometric.nnnorm_map]
