Coordinate identities for the vector Gaussian estimate

These identities translate componentwise scalar estimates into the vector norms in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.gauss_vec3EuclideanNorm_sq (x : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm x ^ 2 = ∑ i : Fin 3, x i ^ 2

The square of the Euclidean norm on Vec3 is the sum of coordinate squares.

theorem CKN.gauss_spatialGradientSq_eq_sum_scalarGradSq (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : spatialGradientSq w (spatialGradient w) z = ∑ i : Fin 3, scalarGradSq (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) z

The gradient density is the sum of scalar gradient densities.

theorem CKN.gauss_heatVec_norm_sq (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : (Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2 = ∑ i : Fin 3, (timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) z + scalarLaplacian (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) z) ^ 2

The backward heat operator has the expected sum-of-squares norm.

theorem CKN.gauss_conjugated_norm_sq (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : (Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (φ z) * w z i) ^ 2 = Real.exp (φ z) ^ 2 * Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2

Scalar exponential conjugation scales the squared vector norm.

theorem CKN.gauss_exp_two_phase_eq_weight (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : Real.exp (2 * gaussCarlemanPhase q z) = gaussCarlemanTimeWeight z.2 ^ (-2 * q) * Real.exp (-Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2))

The exponential of twice the phase is the Gaussian weight with parameter q.

theorem CKN.gauss_timeWeight_shift (a t : ℝ) (ht : 0 < t) : gaussCarlemanTimeWeight t ^ (-2 * a) = gaussCarlemanTimeWeight t ^ 2 * gaussCarlemanTimeWeight t ^ (-2 * (a + 1))

Shifting the Gaussian time exponent by one produces exactly h².

theorem CKN.gauss_weight_eq_timeWeight_sq_mul_exp_phase (a : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) = gaussCarlemanTimeWeight z.2 ^ 2 * Real.exp (2 * gaussCarlemanPhase (a + 1) z)

The original Gaussian weight differs from the conjugation weight by h².

theorem CKN.gauss_weight_le_phase (a : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht0 : 0 < z.2) (ht2 : z.2 < 2) : gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) ≤ Real.exp (2 / 3) * (z.2 ^ 2 * Real.exp (2 * gaussCarlemanPhase (a + 1) z))

The original weight is controlled by the phase weight with the first factor e^(2/3) from the time comparison.

theorem CKN.gauss_phase_le_weight (a : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht0 : 0 < z.2) (ht2 : z.2 < 2) : z.2 ^ 2 * Real.exp (2 * gaussCarlemanPhase (a + 1) z) ≤ Real.exp (2 / 3) * (gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)))

The phase-weighted operator energy is controlled by the original weight with the second factor e^(2/3).

theorem CKN.gauss_setIntegral_eq_integral_of_zero_outside (f : Foundation.Parabolic.ParabolicPoint → ℝ) (h : ∀ z ∉ spaceTimeSet Set.univ (Set.Ioo 0 2), f z = 0) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 2), f z = ∫ (z : Foundation.Parabolic.ParabolicPoint), f z

A density supported inside the open cylinder has the same integral on the cylinder and on the full space-time domain.

theorem CKN.gauss_component_zero_outside (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (hz : z ∉ tsupport (have this := w; this)) (i : Fin 3) : w z i = 0 ∧ timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) z = 0 ∧ ∀ (j : Fin 3), spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) j z = 0 ∧ spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => w y i) j j z = 0

A component and its first and second derivatives vanish off the support of a smooth vector field.