Support and integral forms of the Gaussian commutator

The density identity from eq:carleman-I extends across the complement of the test field's support, which permits whole-space integration.

@[instance_reducible]

def ESS.gaussIntegralToolsNormedAddCommGroup : NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

The product norm on parabolic space-time used in this identity.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def ESS.gaussIntegralToolsNormedSpace : NormedSpace ℝ CKN.Foundation.Parabolic.ParabolicPoint

The real scalar action compatible with the product norm on parabolic space-time.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.gauss_commutatorDensity_global (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hvU : tsupport (have this := v; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.carlemanCommutatorDensity (CKN.gaussCarlemanPhase q) v z = q / 3 * z.2 * v z ^ 2

The Gaussian commutator identity holds globally for a field supported in the positive-time cylinder.

theorem ESS.gauss_commutator_integral_eq (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hvU : tsupport (have this := v; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.carlemanCommutatorDensity (CKN.gaussCarlemanPhase q) v z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), q / 3 * z.2 * v z ^ 2

The Gaussian commutator integral is its explicit positive density.

theorem ESS.gauss_potential_times_field_global (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hvU : tsupport (have this := v; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : v z ^ 2 * (CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z - CKN.timePartial (CKN.gaussCarlemanPhase q) z) = v z ^ 2 * (-CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z + q * (1 / z.2 - 1 / 3))

The Gaussian phase potential can be rewritten wherever the field is supported, and both sides vanish elsewhere.

theorem ESS.gauss_coefficient_times_field_le (q : ℝ) (hq : 0 ≤ q) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hvU : tsupport (have this := v; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : (-z.2 + q * z.2 ^ 2 * (1 / z.2 - 1 / 3)) * v z ^ 2 ≤ q * z.2 * v z ^ 2

The coefficient in the Gaussian integrated gradient identity is bounded by the commutator density.

theorem ESS.gauss_original_energy_zero_outside (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z) = 0

The weighted field and gradient density vanishes outside the test field's supporting cylinder.

theorem ESS.gauss_original_heat_zero_outside (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2 = 0

The weighted heat density vanishes outside the test field's supporting cylinder.

theorem ESS.gauss_original_energy_setIntegral_eq_integral (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z) = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z)

The original energy integral over the cylinder equals the whole-space integral of its zero extension.

theorem ESS.gauss_original_heat_setIntegral_eq_integral (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2 = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2

The original heat integral over the cylinder equals the whole-space integral of its zero extension.

theorem ESS.gauss_vector_conjugated_heat_sq_global (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ∑ i : Fin 3, CKN.carlemanConj (CKN.gaussCarlemanPhase q) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z ^ 2 = Real.exp (CKN.gaussCarlemanPhase q z) ^ 2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2

The vector conjugation identity extends globally because both sides vanish off the field's support.

theorem ESS.gauss_component_conjugation_global (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.carlemanConj (CKN.gaussCarlemanPhase q) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z = Real.exp (CKN.gaussCarlemanPhase q z) * (CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + CKN.scalarLaplacian (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z)

Scalar Gaussian conjugation holds globally for each component of a supported vector field.

theorem ESS.gauss_vector_weighted_energy_le_global (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ha : 0 < a) (hw : ContDiff ℝ (↑⊤) w) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z) ≤ Real.exp (2 / 3) * ((a + 1) * z.2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase (a + 1) z) * w z i) ^ 2 + 2 * z.2 ^ 2 * (∑ i : Fin 3, CKN.scalarGradSq (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase (a + 1) y) * w y i) z + (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase (a + 1) z) * w z i) ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase (a + 1)) z))

The pointwise vector energy comparison holds globally after extension by zero outside the supporting cylinder.

theorem ESS.gauss_vector_operator_energy_le_global (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwU : tsupport (have this := w; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z.2 ^ 2 * ∑ i : Fin 3, CKN.carlemanConj (CKN.gaussCarlemanPhase (a + 1)) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase (a + 1) y) * w y i) z ^ 2 ≤ Real.exp (2 / 3) * (CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2)

The conjugated heat energy comparison holds across the complement of the supporting cylinder.