1.8. Norm square function🔗

@[pp_nodot] def normSq : ℚ[i] →*₀ ℚ where toFun z := z.re * z.re + z.im * z.im map_zero' := by⊢ complexQ.re 0 * complexQ.re 0 + complexQ.im 0 * complexQ.im 0 = 0 dsimp⊢ 0 * 0 + 0 * 0 = 0; simpAll goals completed! 🐙 map_one' := by⊢ complexQ.re 1 * complexQ.re 1 + complexQ.im 1 * complexQ.im 1 = 1 simp [one_def, ofRational_def, ofRational_re, mul_one, ofRational_im, mul_zero,add_zero]All goals completed! 🐙 map_mul' z w := byz:ℚ[i]w:ℚ[i]⊢ (z * w).re * (z * w).re + (z * w).im * (z * w).im = (z.re * z.re + z.im * z.im) * (w.re * w.re + w.im * w.im) simpz:ℚ[i]w:ℚ[i]⊢ (z.re * w.re - z.im * w.im) * (z.re * w.re - z.im * w.im) + (z.re * w.im + z.im * w.re) * (z.re * w.im + z.im * w.re) = (z.re * z.re + z.im * z.im) * (w.re * w.re + w.im * w.im); ringAll goals completed! 🐙 theorem normSq_apply (z : ℚ[i]) : normSq z = z.re * z.re + z.im * z.im := rfl @[simp] theorem normSq_ofRational (r : ℚ) : normSq r = r * r := byr:ℚ⊢ normSq ↑r = r * r simp [normSq]All goals completed! 🐙 @[simp] theorem normSq_natCast (n : ℕ) : normSq n = n * n := normSq_ofRational _ @[simp] theorem normSq_intCast (z : ℤ) : normSq z = z * z := normSq_ofRational _ @[simp] theorem normSq_ofNat (n : ℕ) [n.AtLeastTwo] : normSq (no_index (OfNat.ofNat n : ℚ[i])) = OfNat.ofNat n * OfNat.ofNat n := normSq_natCast _ @[simp] theorem normSq_mk (x y : ℚ) : normSq ⟨x,y⟩ = x*x + y*y := rfl theorem normSq_add_mul_I (x y : ℚ) : normSq (x + y * I) = x ^ 2 + y ^ 2 := byx:ℚy:ℚ⊢ normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2 rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]All goals completed! 🐙 theorem normSq_eq_conj_mul_self {z : ℚ} : (normSq z : ℚ[i]) = conj z * z := byz:ℚ⊢ ↑(normSq ↑z) = ↑((starRingEnd ℚ) z) * ↑z extrez:ℚ⊢ (↑(normSq ↑z)).re = (↑((starRingEnd ℚ) z) * ↑z).reimz:ℚ⊢ (↑(normSq ↑z)).im = (↑((starRingEnd ℚ) z) * ↑z).im repeat dsimpimz:ℚ⊢ 0 = (starRingEnd ℚ) z * 0 + 0 * z ; simp [normSq]All goals completed! 🐙 theorem normSq_zero : normSq 0 = 0 := normSq.map_zero theorem normSq_one : normSq 1 = 1 := normSq.map_one theorem normSq_nonneg (z : ℚ[i]) : 0 ≤ normSq z := add_nonneg (mul_self_nonneg _) (mul_self_nonneg _) theorem normSq_eq_zero {z : ℚ[i]} : normSq z = 0 ↔ z = 0 := ⟨fun h => ext (eq_zero_of_mul_self_add_mul_self_eq_zero h) (eq_zero_of_mul_self_add_mul_self_eq_zero <| (add_comm _ _).trans h), fun h => h.symm ▸ normSq_zero⟩ @[simp] theorem normSq_pos {z : ℚ[i]} : 0 < normSq z ↔ z ≠ 0 := (normSq_nonneg z).lt_iff_ne.trans <| not_congr (eq_comm.trans normSq_eq_zero) @[simp] theorem normSq_neg (z : ℚ[i]) : normSq (-z) = normSq z := byz:ℚ[i]⊢ normSq (-z) = normSq z simp [normSq]All goals completed! 🐙 @[simp] theorem normSq_conj (z : ℚ[i]) : normSq (conj z) = normSq z := byz:ℚ[i]⊢ normSq ((starRingEnd ℚ[i]) z) = normSq z simp [normSq]All goals completed! 🐙 theorem normSq_mul (z w : ℚ[i]) : normSq (z * w) = normSq z * normSq w := normSq.map_mul z w theorem normSq_add (z w : ℚ[i]) : normSq (z + w) = normSq z + normSq w + 2 * (z * conj w).re := byz:ℚ[i]w:ℚ[i]⊢ normSq (z + w) = normSq z + normSq w + 2 * (z * (starRingEnd ℚ[i]) w).re dsimp [normSq]z:ℚ[i]w:ℚ[i]⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) = z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im); ringAll goals completed! 🐙 theorem re_sq_le_normSq (z : ℚ[i]) : z.re * z.re ≤ normSq z := le_add_of_nonneg_right (mul_self_nonneg _) theorem im_sq_le_normSq (z : ℚ[i]) : z.im * z.im ≤ normSq z := le_add_of_nonneg_left (mul_self_nonneg _) theorem mul_conj (z : ℚ[i]) : z * conj z = normSq z := byz:ℚ[i]⊢ z * (starRingEnd ℚ[i]) z = ↑(normSq z) apply ext_iff.mprz:ℚ[i]⊢ (z * (starRingEnd ℚ[i]) z).re = (↑(normSq z)).re ∧ (z * (starRingEnd ℚ[i]) z).im = (↑(normSq z)).im dsimpz:ℚ[i]⊢ z.re * z.re - z.im * -z.im = normSq z ∧ z.re * -z.im + z.im * z.re = 0 ; simp [normSq]z:ℚ[i]⊢ -(z.re * z.im) + z.im * z.re = 0 ringAll goals completed! 🐙 theorem add_conj (z : ℚ[i]) : z + conj z = (2 * z.re : ℚ) := byz:ℚ[i]⊢ z + (starRingEnd ℚ[i]) z = ↑(2 * z.re) apply ext_iff.mprz:ℚ[i]⊢ (z + (starRingEnd ℚ[i]) z).re = (↑(2 * z.re)).re ∧ (z + (starRingEnd ℚ[i]) z).im = (↑(2 * z.re)).im dsimpz:ℚ[i]⊢ z.re + z.re = 2 * z.re ∧ z.im + -z.im = 0 ; simp only [add_neg_cancel, and_true]z:ℚ[i]⊢ z.re + z.re = 2 * z.re ringAll goals completed! 🐙 @[simp, norm_cast] theorem ofRational_one : ((1 : ℚ) : ℚ[i]) = 1 := rfl -- The coercion `ℚ → ℚ[i]` is a ring homomorphism -- The symbol `→+*` signifies that -- the mapping is a ring homomorphism def ofRational' : ℚ →+* ℚ[i] where toFun x := (x : ℚ[i]) map_one' := ofRational_one map_zero' := ofRational_zero map_mul' := ofRational_mul map_add' := ofRational_add @[simp] theorem ofRational_eq_coe (r : ℚ) : ofRational r = r := rfl @[simp] theorem I_sq : I ^ 2 = -1 := by⊢ I ^ 2 = -1 rw [sq, I_mul_I]All goals completed! 🐙 @[simp] theorem I_pow_four : I ^ 4 = 1 := by⊢ I ^ 4 = 1 rw [(by norm_num : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]All goals completed! 🐙 -- The next two theorem are not true by definition, -- and require some proof. @[simp] theorem sub_re (z w : ℚ[i]) : (z - w).re = z.re - w.re := byz:ℚ[i]w:ℚ[i]⊢ (z - w).re = z.re - w.re rw [(by rfl : z-w = z+(-w)), add_re, neg_re]z:ℚ[i]w:ℚ[i]⊢ z.re + -w.re = z.re - w.re ringAll goals completed! 🐙 @[simp] theorem sub_im (z w : ℚ[i]) : (z - w).im = z.im - w.im := byz:ℚ[i]w:ℚ[i]⊢ (z - w).im = z.im - w.im rw [(by rfl : z-w = z+(-w)), add_im, neg_im]z:ℚ[i]w:ℚ[i]⊢ z.im + -w.im = z.im - w.im ringAll goals completed! 🐙 @[simp, norm_cast] theorem ofRational_sub (r s : ℚ) : ((r - s : ℚ) : ℚ[i]) = r - s := byr:ℚs:ℚ⊢ ↑(r - s) = ↑r - ↑s apply ext_iff.mprr:ℚs:ℚ⊢ (↑(r - s)).re = (↑r - ↑s).re ∧ (↑(r - s)).im = (↑r - ↑s).im dsimpr:ℚs:ℚ⊢ r - s = (↑r - ↑s).re ∧ 0 = (↑r - ↑s).im ; simp [sub_re, sub_im]All goals completed! 🐙 @[simp, norm_cast] theorem ofRational_pow (r : ℚ) (n : ℕ) : ((r^n : ℚ) : ℚ[i]) = (r : ℚ[i])^n := byr:ℚn:ℕ⊢ ↑(r ^ n) = ↑r ^ n induction' n with n hnzeror:ℚ⊢ ↑(r ^ 0) = ↑r ^ 0succr:ℚn:ℕhn:↑(r ^ n) = ↑r ^ n⊢ ↑(r ^ (n + 1)) = ↑r ^ (n + 1) ·zeror:ℚ⊢ ↑(r ^ 0) = ↑r ^ 0 rw [pow_zero, pow_zero]zeror:ℚ⊢ ↑1 = 1 rflAll goals completed! 🐙 ·succr:ℚn:ℕhn:↑(r ^ n) = ↑r ^ n⊢ ↑(r ^ (n + 1)) = ↑r ^ (n + 1) -- inductive step rw [pow_succ, ofRational_mul, hn]succr:ℚn:ℕhn:↑(r ^ n) = ↑r ^ n⊢ ↑r ^ n * ↑r = ↑r ^ (n + 1) ringAll goals completed! 🐙 theorem sub_conj (z : ℚ[i]) : z - conj z = (2 * z.im : ℚ) * I := byz:ℚ[i]⊢ z - (starRingEnd ℚ[i]) z = ↑(2 * z.im) * I apply ext_iff.mprz:ℚ[i]⊢ (z - (starRingEnd ℚ[i]) z).re = (↑(2 * z.im) * I).re ∧ (z - (starRingEnd ℚ[i]) z).im = (↑(2 * z.im) * I).im dsimpz:ℚ[i]⊢ (z - (starRingEnd ℚ[i]) z).re = 2 * z.im * 0 - 0 * 1 ∧ (z - (starRingEnd ℚ[i]) z).im = 2 * z.im * 1 + 0 * 0 ; simpz:ℚ[i]⊢ z.im + z.im = 2 * z.im ringAll goals completed! 🐙 theorem normSq_sub (z w : ℚ[i]) : normSq (z - w) = normSq z + normSq w - 2 * (z * conj w).re := byz:ℚ[i]w:ℚ[i]⊢ normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℚ[i]) w).re rw [sub_eq_add_neg]z:ℚ[i]w:ℚ[i]⊢ normSq (z + -w) = normSq z + normSq w - 2 * (z * (starRingEnd ℚ[i]) w).re rw [normSq_add]z:ℚ[i]w:ℚ[i]⊢ normSq z + normSq (-w) + 2 * (z * (starRingEnd ℚ[i]) (-w)).re = normSq z + normSq w - 2 * (z * (starRingEnd ℚ[i]) w).re simpz:ℚ[i]w:ℚ[i]⊢ normSq z + normSq w + 2 * (-(z.im * w.im) + -(z.re * w.re)) = normSq z + normSq w - 2 * (z.re * w.re + z.im * w.im) ringAll goals completed! 🐙