English
The norm of fract b m is bounded by the sum of norms of the basis vectors.
Русский
Норма fract b m ограничена суммой норм базисных векторов.
LaTeX
$$$ \|\operatorname{fract}_b(m)\| \le \sum_i \|b_i\| $$$
Lean4
theorem norm_fract_le [HasSolidNorm K] (m : E) : ‖fract b m‖ ≤ ∑ i, ‖b i‖ := by
classical
calc
‖fract b m‖ = ‖∑ i, b.repr (fract b m) i • b i‖ := by rw [b.sum_repr]
_ = ‖∑ i, Int.fract (b.repr m i) • b i‖ := by simp_rw [repr_fract_apply]
_ ≤ ∑ i, ‖Int.fract (b.repr m i) • b i‖ := (norm_sum_le _ _)
_ = ∑ i, ‖Int.fract (b.repr m i)‖ * ‖b i‖ := by simp_rw [norm_smul]
_ ≤ ∑ i, ‖b i‖ := Finset.sum_le_sum fun i _ => ?_
suffices ‖Int.fract ((b.repr m) i)‖ ≤ 1
by
convert mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
exact (one_mul _).symm
rw [(norm_one.symm : 1 = ‖(1 : K)‖)]
apply norm_le_norm_of_abs_le_abs
rw [abs_one, Int.abs_fract]
exact le_of_lt (Int.fract_lt_one _)
