no goals
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i : ι, ‖↑b i‖
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 _)
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖ ≤ ‖↑b i‖
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i : ι, ‖↑b i‖
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 _ => ?_
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖ ≤ ‖↑b 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
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ ≤ ‖1‖
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
rw [(norm_one.symm : 1 = ‖(1 : K)‖)]
case h
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ abs (Int.fract (↑(↑b.repr m) i)) ≤ abs 1
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ ≤ ‖1‖
apply norm_le_norm_of_abs_le_abs
case h
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ Int.fract (↑(↑b.repr m) i) ≤ 1
case h
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ abs (Int.fract (↑(↑b.repr m) i)) ≤ abs 1
rw [abs_one, Int.abs_fract]
no goals
case h
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ Int.fract (↑(↑b.repr m) i) ≤ 1
exact le_of_lt (Int.fract_lt_one _)
no goals
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ = ‖∑ i : ι, ↑(↑b.repr (fract b m)) i • ↑b i‖
rw [b.sum_repr]
no goals
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖∑ i : ι, ↑(↑b.repr (fract b m)) i • ↑b i‖ = ‖∑ i : ι, Int.fract (↑(↑b.repr m) i) • ↑b i‖
simp_rw [repr_fract_apply]
no goals
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ∑ i : ι, ‖Int.fract (↑(↑b.repr m) i) • ↑b i‖ = ∑ i : ι, ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖
simp_rw [norm_smul]
case h.e'_4
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
⊢ ‖↑b i‖ = 1 * ‖↑b i‖
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖ ≤ ‖↑b i‖
convert mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
no goals
case h.e'_4
E : Type u_2
ι : Type u_3
K : Type u_1
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
⊢ ‖↑b i‖ = 1 * ‖↑b i‖
exact (one_mul _).symm