Smooth space-time integration by parts

Directional integration by parts for a smooth field and a compactly supported test on the raw product of space and time, expressed using factor derivatives.

theorem CKN.ShearCalculus.instIsAddHaarMeasureProdVec3RealVolume : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.ShearCalculus.spatial_eq_joint {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) : spatialPartial g i z = (fderiv ℝ g z) (basisVec i, 0)

The spatial factor derivative is the joint derivative in a spatial direction.

theorem CKN.ShearCalculus.time_eq_joint {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial g z = (fderiv ℝ g z) (0, 1)

The time factor derivative is the joint derivative in the time direction.

theorem CKN.ShearCalculus.directional_smooth {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (v : Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ g z) v

A directional derivative of a smooth scalar function is smooth.

theorem CKN.ShearCalculus.integral_directional {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (v : Foundation.Parabolic.Vec3 × ℝ) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * (fderiv ℝ G z) v = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), (fderiv ℝ F z) v * G z

Integration by parts in an arbitrary space-time direction.

theorem CKN.ShearCalculus.integral_spatial {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (i : Fin 3) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * spatialPartial G i z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), spatialPartial F i z * G z

Space-time integration by parts for a spatial factor derivative.

theorem CKN.ShearCalculus.integral_time {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * timePartial G z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), timePartial F z * G z

Space-time integration by parts for the time factor derivative.

theorem CKN.ShearCalculus.spatial_smooth {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial F i z

Smoothness of a spatial factor derivative.

theorem CKN.ShearCalculus.spatial_support {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (i : Fin 3) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial F i z) ⊆ tsupport F

A spatial derivative has no larger support than its smooth input.

theorem CKN.ShearCalculus.time_support {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial F z) ⊆ tsupport F

A time derivative has no larger support than its smooth input.

theorem CKN.ShearCalculus.integrable_product {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F z * G z) MeasureTheory.volume

A smooth field times a compactly supported test is integrable.

theorem CKN.ShearCalculus.integrable_spatial {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (i : Fin 3) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F z * spatialPartial G i z) MeasureTheory.volume

Products with spatial test derivatives are integrable.

theorem CKN.ShearCalculus.integrable_time {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F z * timePartial G z) MeasureTheory.volume

Products with time test derivatives are integrable.

theorem CKN.ShearCalculus.spatial_mul {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => F w * G w) i z = spatialPartial F i z * G z + F z * spatialPartial G i z

Product rule for spatial factor derivatives.

theorem CKN.ShearCalculus.time_mul {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => F w * G w) z = timePartial F z * G z + F z * timePartial G z

Product rule for time factor derivatives.

theorem CKN.ShearCalculus.integral_second {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (i : Fin 3) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * spatialPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial G i w) i z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), spatialPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial F i w) i z * G z

Two spatial integrations by parts against a compactly supported test.