Reg Uniform Integration By Parts

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regUniform_continuousOn_pullback {F : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} {Sprod : Set (Foundation.Parabolic.Vec3 × ℝ)} (hF : ContinuousOn F S) (hS : ∀ z ∈ Sprod, (z.1, z.2) ∈ S) : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F (z.1, z.2)) Sprod

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

theorem CKN.Leray.regUniform_contDiffOn_spatialSlice_differentiableAt {S : Set (Foundation.Parabolic.Vec3 × ℝ)} {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hS : IsOpen S) (hF : ContDiffOn ℝ 1 F S) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ S) : DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => F (x, z.2)) z.1

theorem CKN.Leray.regUniform_contDiffOn_timeSlice_differentiableAt {S : Set (Foundation.Parabolic.Vec3 × ℝ)} {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hS : IsOpen S) (hF : ContDiffOn ℝ 1 F S) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ S) : DifferentiableAt ℝ (fun (t : ℝ) => F (z.1, t)) z.2

theorem CKN.Leray.regUniform_integrable_mul_of_tsupport_subset {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hS : IsOpen S) (hF : ContinuousOn F S) (hG : ContinuousOn G S) (hGc : HasCompactSupport G) (hGs : tsupport G ⊆ S) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F z * G z) MeasureTheory.volume

A continuous product with compact support inside an open carrier is integrable on the whole product space.

theorem CKN.Leray.regUniform_integral_mul_spatialPartial_eq_neg {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (i : Fin 3) (hS : IsOpen S) (hFcont : ContinuousOn F S) (hFpartialCont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (have this := F; this) i (z.1, z.2)) S) (hFdiff : ∀ z ∈ S, DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => F (x, z.2)) z.1) (hGcont : ContinuousOn G S) (hGpartialCont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (have this := G; this) i (z.1, z.2)) S) (hGdiff : ∀ z ∈ S, DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => G (x, z.2)) z.1) (hGc : HasCompactSupport G) (hGs : tsupport G ⊆ S) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, F z * spatialPartial (have this := G; this) i z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, spatialPartial (have this := F; this) i z * G z

Spatial integration by parts on an open carrier for a compactly supported factor whose derivatives are controlled on that carrier.

theorem CKN.Leray.regUniform_spatialPartial_mul {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (t : ℝ) (j : Fin 3) (hF : DifferentiableAt ℝ (fun (y : Foundation.Parabolic.Vec3) => F (y, t)) x) (hG : DifferentiableAt ℝ (fun (y : Foundation.Parabolic.Vec3) => G (y, t)) x) : spatialPartial (have this := fun (z : Foundation.Parabolic.ParabolicPoint) => F z * G z; this) j (x, t) = F (x, t) * spatialPartial (have this := G; this) j (x, t) + G (x, t) * spatialPartial (have this := F; this) j (x, t)

Spatial product rule from differentiability of the two time slices.

theorem CKN.Leray.regUniform_timePartial_mul {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (x : Foundation.Parabolic.Vec3) (t : ℝ) (hF : DifferentiableAt ℝ (fun (s : ℝ) => F (x, s)) t) (hG : DifferentiableAt ℝ (fun (s : ℝ) => G (x, s)) t) : timePartial (have this := fun (z : Foundation.Parabolic.ParabolicPoint) => F z * G z; this) (x, t) = F (x, t) * timePartial (have this := G; this) (x, t) + G (x, t) * timePartial (have this := F; this) (x, t)

Time product rule from differentiability of the two spatially fixed slices.

theorem CKN.Leray.regUniform_integral_mul_timePartial_eq_neg {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hS : IsOpen S) (hFcont : ContinuousOn F S) (hFtimeCont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial (have this := F; this) (z.1, z.2)) S) (hFdiff : ∀ z ∈ S, DifferentiableAt ℝ (fun (t : ℝ) => F (z.1, t)) z.2) (hGcont : ContinuousOn G S) (hGtimeCont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial (have this := G; this) (z.1, z.2)) S) (hGdiff : ∀ z ∈ S, DifferentiableAt ℝ (fun (t : ℝ) => G (z.1, t)) z.2) (hGc : HasCompactSupport G) (hGs : tsupport G ⊆ S) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, F z * timePartial (have this := G; this) z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, timePartial (have this := F; this) z * G z

Time integration by parts on an open carrier for a compactly supported factor whose derivatives are controlled on that carrier.

theorem CKN.Leray.regUniform_integral_spatialPartial_eq_zero {G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (i : Fin 3) (hS : IsOpen S) (hGcont : ContinuousOn G S) (hGpartialCont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (have this := G; this) i (z.1, z.2)) S) (hGdiff : ∀ z ∈ S, DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => G (x, z.2)) z.1) (hGc : HasCompactSupport G) (hGs : tsupport G ⊆ S) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, spatialPartial (have this := G; this) i z = 0

A compactly supported spatial derivative has zero integral on an open carrier containing its support.

theorem CKN.Leray.regUniform_integral_timePartial_eq_zero {G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hS : IsOpen S) (hGcont : ContinuousOn G S) (hGtimeCont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial (have this := G; this) (z.1, z.2)) S) (hGdiff : ∀ z ∈ S, DifferentiableAt ℝ (fun (t : ℝ) => G (z.1, t)) z.2) (hGc : HasCompactSupport G) (hGs : tsupport G ⊆ S) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, timePartial (have this := G; this) z = 0

A compactly supported time derivative has zero integral on an open carrier containing its support.