English
For a nonnegative scalar a and x in E, gauge s (a • x) = a⁻¹ · gauge s x (in the appropriate scalar-setting).
Русский
Для неотрицательного скаляра a и элемента x в E выполняется gauge s (a • x) = a⁻¹ · gauge s x (в заданном контексте скаляра).
LaTeX
$$$$(\\text{gauge}(s, a\\cdot x) = a^{-1} \\cdot \\text{gauge}(s,x))\\quad (a \\ge 0).$$$$
Lean4
theorem gauge_smul_of_nonneg [MulActionWithZero α E] [IsScalarTower α ℝ (Set E)] {s : Set E} {a : α} (ha : 0 ≤ a)
(x : E) : gauge s (a • x) = a • gauge s x :=
by
obtain rfl | ha' := ha.eq_or_lt
· rw [zero_smul, gauge_zero, zero_smul]
rw [gauge_def', gauge_def', ← Real.sInf_smul_of_nonneg ha]
congr 1
ext r
simp_rw [Set.mem_smul_set, Set.mem_sep_iff]
constructor
· rintro ⟨hr, hx⟩
simp_rw [mem_Ioi] at hr ⊢
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
have := smul_pos (inv_pos.2 ha') hr
refine ⟨a⁻¹ • r, ⟨this, ?_⟩, smul_inv_smul₀ ha'.ne' _⟩
rwa [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc, mem_smul_set_iff_inv_smul_mem₀ (inv_ne_zero ha'.ne'),
inv_inv]
· rintro ⟨r, ⟨hr, hx⟩, rfl⟩
rw [mem_Ioi] at hr ⊢
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
have := smul_pos ha' hr
refine ⟨this, ?_⟩
rw [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc]
exact smul_mem_smul_set hx
