Duhamel Adjoint

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.Step3.canonical_spaceTime_cutoff_box {r R t₀ : ℝ} (hr : 0 ≤ r) (hrR : r < R) : have χ := spaceTimeCutoff 0 t₀ r R; χ ∈ spaceTimeTestFunction Set.univ Set.univ ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.1 ∈ euclideanBall 0 r → z.2 ∈ Set.Icc (t₀ - r ^ 2) t₀ → χ z = 1

The causal heat potential with a divergence-form source.

noncomputable def CKN.Core.Step3.duhamelPotential (g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Vec3

Vector Duhamel potential with the sign convention for the localized divergence equation.

Equations

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

structure CKN.Core.Step3.DuhamelSupportData (v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Type

Common interior cylinder containing the supports needed for the localized Duhamel argument.

• r : ℝ

  Inner radius on which the common Duhamel cutoff is one.

• R : ℝ

  Outer radius containing the supports of all localized sources.

• t₀ : ℝ

  Reference time for the common Duhamel support cylinder.

• hr : 0 ≤ self.r
• hrR : self.r < self.R
• v_support (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : (z ∈ tsupport fun (w : Foundation.Parabolic.ParabolicPoint) => v w i) → z.1 ∈ euclideanBall 0 self.r ∧ z.2 ∈ Set.Ioo (self.t₀ - self.r ^ 2) self.t₀
• g_support (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : (z ∈ tsupport fun (w : Foundation.Parabolic.ParabolicPoint) => g w i) → z.1 ∈ euclideanBall 0 self.r ∧ z.2 ∈ Set.Ioo (self.t₀ - self.r ^ 2) self.t₀
• h_support (j i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : (z ∈ tsupport fun (w : Foundation.Parabolic.ParabolicPoint) => h j w i) → z.1 ∈ euclideanBall 0 self.r ∧ z.2 ∈ Set.Ioo (self.t₀ - self.r ^ 2) self.t₀

theorem CKN.Core.Step3.duhamelPotential_pairing {ζ : Foundation.Parabolic.ParabolicPoint → ℝ} {g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (i : Fin 3) (hFg : MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatKernel q.1 q.2 * ζ q.1 * g q.2 i) (MeasureTheory.volume.prod MeasureTheory.volume)) (hFh : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatSpatialKernel j q.1 q.2 * ζ q.1 * h j q.2 i) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (z : Foundation.Parabolic.ParabolicPoint), ζ z * duhamelPotential g h z i = (∫ (v : Foundation.Parabolic.ParabolicPoint), g v i * Foundation.Heat.backwardHeatPotential ζ v) + ∑ j : Fin 3, ∫ (v : Foundation.Parabolic.ParabolicPoint), h j v i * Foundation.Heat.backwardHeatPotentialSpatial j ζ v

theorem CKN.Core.Step3.duhamel_of_adjoint_identity {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i) MeasureTheory.volume) (hpotential : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => duhamelPotential g h z i) MeasureTheory.volume) (hadjoint : ∀ (ζ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ζ → HasCompactSupport ζ → ∀ (i : Fin 3), ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ζ z * v z i = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ζ z * duhamelPotential g h z i) : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), v z = duhamelPotential g h z

theorem CKN.Core.Step3.duhamel_of_cutoff_localized_equation {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i) MeasureTheory.volume) (hpotential : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => duhamelPotential g h z i) MeasureTheory.volume) (hFg : ∀ (ζ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ζ → HasCompactSupport ζ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatKernel q.1 q.2 * ζ q.1 * g q.2 i) (MeasureTheory.volume.prod MeasureTheory.volume)) (hFh : ∀ (ζ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ζ → HasCompactSupport ζ → ∀ (j i : Fin 3), MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatSpatialKernel j q.1 q.2 * ζ q.1 * h j q.2 i) (MeasureTheory.volume.prod MeasureTheory.volume)) (hweak : ∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, ∫ (z : Foundation.Parabolic.ParabolicPoint), v z i * (-timePartial ψ z - ∑ j : Fin 3, spatialSecondPartial ψ j j z) = (∫ (z : Foundation.Parabolic.ParabolicPoint), g z i * ψ z) + ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint), h j z i * spatialPartial ψ j z) (hsupport : DuhamelSupportData v g h) : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), v z = duhamelPotential g h z

theorem CKN.Core.Step3.duhamel_of_localized_velocity {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {u g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => localizedVelocity φ u z i) MeasureTheory.volume) (hpotential : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => duhamelPotential g h z i) MeasureTheory.volume) (hFg : ∀ (ζ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ζ → HasCompactSupport ζ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatKernel q.1 q.2 * ζ q.1 * g q.2 i) (MeasureTheory.volume.prod MeasureTheory.volume)) (hFh : ∀ (ζ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ζ → HasCompactSupport ζ → ∀ (j i : Fin 3), MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatSpatialKernel j q.1 q.2 * ζ q.1 * h j q.2 i) (MeasureTheory.volume.prod MeasureTheory.volume)) (hweak : ∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, ∫ (z : Foundation.Parabolic.ParabolicPoint), localizedVelocity φ u z i * (-timePartial ψ z - ∑ j : Fin 3, spatialSecondPartial ψ j j z) = (∫ (z : Foundation.Parabolic.ParabolicPoint), g z i * ψ z) + ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint), h j z i * spatialPartial ψ j z) (hsupport : DuhamelSupportData (localizedVelocity φ u) g h) : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), localizedVelocity φ u z = duhamelPotential g h z