English
If a is nonnegative (ha: 0 ≤ a) in the presence of a module structure and IsScalarTower relations, then QuasispectrumRestricts a realToNNReal.
Русский
Если a неотрицательно и имеются соответствующие структуры модуля и скалярного башмака, тогда QuasispectrumRestricts a realToNNReal.
LaTeX
$$$\text{QuasispectrumRestricts}(a,\text{realToNNReal})$$$
Lean4
/-- Alternative constructor for a `Seminorm` over a normed field `𝕜` that only assumes `f 0 = 0`
and an inequality for the scalar multiplication. -/
def ofSMulLE [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (f : E → ℝ) (map_zero : f 0 = 0)
(add_le : ∀ x y, f (x + y) ≤ f x + f y) (smul_le : ∀ (r : 𝕜) (x), f (r • x) ≤ ‖r‖ * f x) : Seminorm 𝕜 E :=
Seminorm.of f add_le fun r x => by
refine le_antisymm (smul_le r x) ?_
by_cases h : r = 0
· simp [h, map_zero]
rw [← mul_le_mul_iff_right₀ (inv_pos.mpr (norm_pos_iff.mpr h))]
rw [inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr h)]
specialize smul_le r⁻¹ (r • x)
rw [norm_inv] at smul_le
convert smul_le
simp [h]
