Integrability of the Gaussian heat density

The heat density in prop:carleman-gauss is smooth where the weight is defined and has compact support in the positive-time cylinder.

@[instance_reducible]

def ESS.gaussIntegrableNormedAddCommGroup : 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.gaussIntegrableNormedSpace : 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_original_weight_contDiffOn (a : ℝ) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2))) (CKN.spaceTimeSet Set.univ (Set.Ioo 0 2))

The original Gaussian weight is smooth on the positive-time cylinder.

theorem ESS.gauss_heat_density_smooth_support (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) : (ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (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) ∧ (HasCompactSupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (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) ∧ (tsupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (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) ⊆ tsupport w

The squared vector heat density is smooth and has no support outside the original vector field.

theorem ESS.gauss_original_heat_integrable (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => 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) MeasureTheory.volume

The right-hand heat density of prop:carleman-gauss is integrable.

theorem ESS.gauss_phase_energy_coefficient_contDiffOn (q : ℝ) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => z.2 ^ 2 * Real.exp (2 * CKN.gaussCarlemanPhase q z)) (CKN.spaceTimeSet Set.univ (Set.Ioo 0 2))

The coefficient of the conjugated heat energy is smooth on positive time.

theorem ESS.gauss_conjugated_heat_integrable (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * ∑ 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) MeasureTheory.volume

The conjugated vector heat energy is integrable on space-time.

theorem ESS.gauss_component_conjugated_heat_integrable (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (i : Fin 3) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * CKN.carlemanConj (CKN.gaussCarlemanPhase q) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z ^ 2) MeasureTheory.volume

Each scalar conjugated heat energy is integrable.

theorem ESS.gauss_mass_integrable (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport (have this := v; this)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => q / 3 * z.2 * v z ^ 2) MeasureTheory.volume

The Gaussian commutator mass density is integrable for a smooth compactly supported scalar field.

theorem ESS.gauss_cross_integral_le (q : ℝ) (hq : 1 ≤ q) (v L : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hvU : tsupport (have this := v; this) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (hC : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * v z * L z) MeasureTheory.volume) (hI : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => q / 3 * z.2 * v z ^ 2) MeasureTheory.volume) (hP : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * L z ^ 2) MeasureTheory.volume) : |∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.2 ^ 2 * v z * L z| ≤ √6 / 2 * ((∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), q / 3 * z.2 * v z ^ 2) + ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.2 ^ 2 * L z ^ 2)

The Gaussian cross integral satisfies the sharp Young form of the Cauchy–Schwarz bound from eq:carleman-E.

theorem ESS.gauss_cross_integrable (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * v z * CKN.carlemanConj (CKN.gaussCarlemanPhase q) v z) MeasureTheory.volume

The Gaussian cross density is integrable for a smooth scalar field supported in the positive-time cylinder.

theorem ESS.gauss_potential_integrable (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * v z ^ 2 * (CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z - CKN.timePartial (CKN.gaussCarlemanPhase q) z)) MeasureTheory.volume

The phase potential term in the Gaussian integrated gradient identity is integrable.

theorem ESS.gauss_phase_gradient_mass_integrable (q : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * v z ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z) MeasureTheory.volume

The phase-gradient part of the Gaussian energy is integrable.

theorem ESS.gauss_scalar_gradient_integrable (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * CKN.scalarGradSq v z) MeasureTheory.volume

The squared scalar gradient of a smooth compactly supported field is integrable after multiplication by t².