GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I

theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I : ∀ (b : ℂ) (c T : ℝ), ‖(-b * (↑T + ↑c * Complex.I) ^ 2).exp‖ = (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2)).exp

This theorem provides an explicit formula for the norm of the Gaussian function along the vertical edges. Specifically, for any complex number `b` and real numbers `c` and `T`, the norm of the exponent of the negative of `b` multiplied by the square of the sum of `T` and `c` times the imaginary unit is equal to the exponent of the negative of the real part of `b` times the square of `T` minus twice the imaginary part of `b` times `c` times `T` minus the real part of `b` times the square of `c`.

More concisely: The norm of the Gaussian function along vertical edges is given by the formula $|e^{-ib(T+ic)^2}| = e^{-|b|(T^2-2ct) + ic^2}$, where $i$ is the imaginary unit.