Gaussian Integer Norm Convexity Identity

import Mathlib

theorem gaussian_integer_norm_convexity (x z : ℂ) : let y : ℂ := (x + z) / 2; Complex.normSq y = (1 / 2 : ℝ) * Complex.normSq x + (1 / 2 : ℝ) * Complex.normSq z - (1 / 4 : ℝ) * Complex.normSq (x - z) := by sorry