[GOAL]
x y : ℍ
⊢ ↑(starRingEnd ℝ) (inner y x) = inner x y
[PROOFSTEP]
simp [inner_def, mul_comm]
[GOAL]
x y z : ℍ
⊢ inner (x + y) z = inner x z + inner y z
[PROOFSTEP]
simp only [inner_def, add_mul, add_re]
[GOAL]
x y : ℍ
r : ℝ
⊢ inner (r • x) y = ↑(starRingEnd ℝ) r * inner x y
[PROOFSTEP]
simp [inner_def]
[GOAL]
a : ℍ
⊢ ↑normSq a = ‖a‖ * ‖a‖
[PROOFSTEP]
rw [← inner_self, real_inner_self_eq_norm_mul_norm]
[GOAL]
⊢ ‖1‖ = 1
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]
[GOAL]
a : ℝ
⊢ ‖↑a‖ = ‖a‖
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
[GOAL]
a : ℍ
⊢ ‖star a‖ = ‖a‖
[PROOFSTEP]
simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
[GOAL]
a b : ℍ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖
[PROOFSTEP]
simp only [norm_eq_sqrt_real_inner, inner_self, normSq.map_mul]
[GOAL]
a b : ℍ
⊢ Real.sqrt (↑normSq a * ↑normSq b) = Real.sqrt (↑normSq a) * Real.sqrt (↑normSq b)
[PROOFSTEP]
exact
  Real.sqrt_mul normSq_nonneg
    _
      -- porting note: added `noncomputable`
[GOAL]
z w : ℂ
⊢ ↑(z + w) = ↑z + ↑w
[PROOFSTEP]
ext
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).re = (↑z + ↑w).re
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).imI = (↑z + ↑w).imI
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).imJ = (↑z + ↑w).imJ
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).imK = (↑z + ↑w).imK
[PROOFSTEP]
simp
[GOAL]
z w : ℂ
⊢ ↑(z * w) = ↑z * ↑w
[PROOFSTEP]
ext
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).re = (↑z * ↑w).re
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).imI = (↑z * ↑w).imI
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).imJ = (↑z * ↑w).imJ
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).imK = (↑z * ↑w).imK
[PROOFSTEP]
simp
[GOAL]
r : ℝ
z : ℂ
⊢ ↑(r • z) = ↑r * ↑z
[PROOFSTEP]
ext
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).re = (↑r * ↑z).re
[PROOFSTEP]
simp
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).imI = (↑r * ↑z).imI
[PROOFSTEP]
simp
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).imJ = (↑r * ↑z).imJ
[PROOFSTEP]
simp
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).imK = (↑r * ↑z).imK
[PROOFSTEP]
simp
[GOAL]
x : ℍ
⊢ ‖↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x)‖ = ‖x‖
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply, Fin.sum_univ_four]
[GOAL]
x : ℍ
⊢ Real.sqrt
      (inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0) +
            inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1) +
          inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2)
            (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2) +
        inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)
          (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
[PROOFSTEP]
simp_rw [IsROrC.inner_apply, starRingEnd_apply, star_trivial, ← sq]
[GOAL]
x : ℍ
⊢ Real.sqrt
      (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0 ^ 2 +
            ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1 ^ 2 +
          ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2 ^ 2 +
        ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3 ^ 2) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
[PROOFSTEP]
rfl
[GOAL]
⊢ Continuous ↑normSq
[PROOFSTEP]
simpa [← normSq_eq_norm_mul_self] using (continuous_norm.mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)
[GOAL]
⊢ Continuous fun q => im q
[PROOFSTEP]
simpa only [← sub_self_re] using continuous_id.sub (continuous_coe.comp continuous_re)
[GOAL]
this : UniformEmbedding ↑(LinearEquiv.toEquiv linearIsometryEquivTuple.toLinearEquiv).symm
⊢ CompleteSpace (EuclideanSpace ℝ (Fin 4))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
f : α → ℝ
r : ℝ
h : HasSum (fun a => ↑(f a)) ↑r
⊢ HasSum f r
[PROOFSTEP]
simpa only using h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _) continuous_re
[GOAL]
α : Type u_1
f : α → ℝ
r : ℝ
h : HasSum f r
⊢ HasSum (fun a => ↑(f a)) ↑r
[PROOFSTEP]
simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)
[GOAL]
α : Type u_1
f : α → ℝ
⊢ (Summable fun a => ↑(f a)) ↔ Summable f
[PROOFSTEP]
simpa only using
  Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _)
    (continuous_algebraMap _ _) continuous_re coe_re
[GOAL]
α : Type u_1
f : α → ℝ
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
[PROOFSTEP]
exact (hasSum_coe.mpr hf.hasSum).tsum_eq
[GOAL]
case neg
α : Type u_1
f : α → ℝ
hf : ¬Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
[PROOFSTEP]
simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]
