English
Under suitable tower and commutativity hypotheses, gauge (a • s) = a⁻¹ • gauge s for nonnegative a.
Русский
При надлежащих условиях башни и коммутативности gauge (a • s) = a⁻¹ • gauge s при неотрицательном a.
LaTeX
$$$$(\\mathrm{gauge}(a\\cdot s) = a^{-1} \\cdot \\mathrm{gauge}(s))\\quad (a \\ge 0).$$$$
Lean4
theorem gauge_smul_left_of_nonneg [MulActionWithZero α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ]
[IsScalarTower α ℝ E] {s : Set E} {a : α} (ha : 0 ≤ a) : gauge (a • s) = a⁻¹ • gauge s :=
by
obtain rfl | ha' := ha.eq_or_lt
· rw [inv_zero, zero_smul, gauge_of_subset_zero (zero_smul_set_subset _)]
ext x
rw [gauge_def', Pi.smul_apply, gauge_def', ← Real.sInf_smul_of_nonneg (inv_nonneg.2 ha)]
congr 1
ext r
simp_rw [Set.mem_smul_set, Set.mem_sep_iff]
constructor
· rintro ⟨hr, y, hy, h⟩
simp_rw [mem_Ioi] at hr ⊢
refine ⟨a • r, ⟨smul_pos ha' hr, ?_⟩, inv_smul_smul₀ ha'.ne' _⟩
rwa [smul_inv₀, smul_assoc, ← h, inv_smul_smul₀ ha'.ne']
· rintro ⟨r, ⟨hr, hx⟩, rfl⟩
rw [mem_Ioi] at hr ⊢
refine ⟨smul_pos (inv_pos.2 ha') hr, r⁻¹ • x, hx, ?_⟩
rw [smul_inv₀, smul_assoc, inv_inv]
