The weighted gradient identity

The space-time integration identity used in eq:carleman-gradient-integrated of the Escauriaza–Seregin–Šverák manuscript and eq:carleman-half-gradient-id of the Escauriaza–Seregin–Šverák manuscript.

@[instance_reducible]

noncomputable def CKN.carlemanCoreGradientMeasureSpace : MeasureTheory.MeasureSpace Foundation.Parabolic.ParabolicPoint

The product measure structure on space-time for the gradient identities.

Equations

• CKN.carlemanCoreGradientMeasureSpace = MeasureTheory.Measure.prod.measureSpace

@[instance_reducible]

def CKN.carlemanCoreGradientNormedAddCommGroup : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure used in the gradient identities.

Equations

• CKN.carlemanCoreGradientNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

noncomputable def CKN.carlemanCoreGradientNormedSpace : NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

The real product normed-space structure used in the gradient identities.

Equations

• CKN.carlemanCoreGradientNormedSpace = CKN.carlemanProductNormedSpace

theorem CKN.timePartial_time_pow (m : ℕ) (z : Foundation.Parabolic.ParabolicPoint) : timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m) z = ↑m * z.2 ^ (m - 1)

The time derivative of an integral power of the time coordinate.

theorem CKN.spatialPartial_time_pow (m : ℕ) (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) : spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m) i z = 0

A function of time alone has zero spatial derivative.

theorem CKN.timePartial_sq_at {v : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hv : DifferentiableAt ℝ v z) : timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => v y ^ 2) z = 2 * v z * timePartial v z

The time derivative of the square of a smooth scalar field.

theorem CKN.spatialPartial_sq_at {v : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hv : DifferentiableAt ℝ v z) (i : Fin 3) : spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => v y ^ 2) i z = 2 * v z * spatialPartial v i z

A spatial derivative of the square of a smooth scalar field.

theorem CKN.timePartial_time_pow_mul_sq_at (m : ℕ) {v : Foundation.Parabolic.ParabolicPoint → ℝ} (hv : ContDiff ℝ (↑⊤) v) (z : Foundation.Parabolic.ParabolicPoint) : timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2) z = ↑m * z.2 ^ (m - 1) * v z ^ 2 + 2 * z.2 ^ m * v z * timePartial v z

Time derivative of the weighted square flux.

theorem CKN.spatialPartial_time_pow_mul_gradient_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) (m : ℕ) {v : Foundation.Parabolic.ParabolicPoint → ℝ} (hv : ContDiff ℝ (↑⊤) v) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) : spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y * spatialPartial v i y) i z = z.2 ^ m * (spatialPartial v i z ^ 2 + v z * spatialSecondPartial v i i z)

Spatial derivative of the weighted gradient flux.

theorem CKN.spatialPartial_time_pow_mul_phase_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) (m : ℕ) {φ v : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) : spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2 * spatialPartial φ i y) i z = z.2 ^ m * (2 * v z * spatialPartial v i z * spatialPartial φ i z + v z ^ 2 * spatialSecondPartial φ i i z)

Spatial derivative of the weighted phase flux.

theorem CKN.carleman_gradient_density {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) (m : ℕ) {φ v : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) : z.2 ^ m * scalarGradSq v z = -(↑m / 2) * z.2 ^ (m - 1) * v z ^ 2 - z.2 ^ m * v z * carlemanConj φ v z + z.2 ^ m * v z ^ 2 * (scalarGradSq φ z - timePartial φ z) + 1 / 2 * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2) z + ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y * spatialPartial v i y) i z - ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2 * spatialPartial φ i y) i z

The weighted gradient density differs from the conjugated heat pairing by space-time derivatives of compactly supported fluxes.

theorem CKN.carleman_gradient_density_global {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) (m : ℕ) {φ v : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) (hvU : tsupport v ⊆ U) (z : Foundation.Parabolic.ParabolicPoint) : z.2 ^ m * scalarGradSq v z = -(↑m / 2) * z.2 ^ (m - 1) * v z ^ 2 - z.2 ^ m * v z * carlemanConj φ v z + z.2 ^ m * v z ^ 2 * (scalarGradSq φ z - timePartial φ z) + 1 / 2 * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2) z + ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y * spatialPartial v i y) i z - ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2 * spatialPartial φ i y) i z

The weighted gradient density identity holds on all space-time when the field is supported in the phase domain.

theorem CKN.carleman_gradient_flux_integrals_zero {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) (m : ℕ) {φ v : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ U) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2) z = 0 ∧ ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y * spatialPartial v i y) i z = 0 ∧ ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * v y ^ 2 * spatialPartial φ i y) i z = 0

All three boundary fluxes in the weighted gradient identity integrate to zero for a field compactly supported in the phase domain.

theorem CKN.integrable_contDiff_compact {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : MeasureTheory.Integrable f MeasureTheory.volume

A smooth compactly supported scalar field on space-time is integrable.

theorem CKN.carleman_gradient_identity (m : ℕ) {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ v : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ U) : ∫ (z : Foundation.Parabolic.ParabolicPoint), z.2 ^ m * scalarGradSq v z = ((-(↑m / 2) * ∫ (z : Foundation.Parabolic.ParabolicPoint), z.2 ^ (m - 1) * v z ^ 2) - ∫ (z : Foundation.Parabolic.ParabolicPoint), z.2 ^ m * v z * carlemanConj φ v z) + ∫ (z : Foundation.Parabolic.ParabolicPoint), z.2 ^ m * v z ^ 2 * (scalarGradSq φ z - timePartial φ z)

The integrated weighted gradient identity from eq:carleman-gradient-integrated (ESS).