Backward Potential

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

The backward heat potential used to test a causal weak equation.

noncomputable def CKN.Foundation.Heat.backwardProductVolume : MeasureTheory.Measure (Parabolic.Vec3 × ℝ)

Product of spatial volume and time volume for backward heat integration.

Equations

• CKN.Foundation.Heat.backwardProductVolume = MeasureTheory.volume.prod MeasureTheory.volume

noncomputable def CKN.Foundation.Heat.backwardTestKernel (p : Parabolic.Vec3 × ℝ) : ℝ

Reflected causal heat kernel used in the backward test-function convolution.

Equations

• CKN.Foundation.Heat.backwardTestKernel p = CKN.Foundation.Heat.heatKernelPlus (have this := -p; this)

noncomputable def CKN.Foundation.Heat.backwardTestPotential (ζ : Parabolic.Vec3 × ℝ → ℝ) (v : Parabolic.Vec3 × ℝ) : ℝ

Backward heat potential of a test function, written as a product-space convolution.

Equations

• CKN.Foundation.Heat.backwardTestPotential ζ v = MeasureTheory.convolution CKN.Foundation.Heat.backwardTestKernel ζ (ContinuousLinearMap.lsmul ℝ ℝ) CKN.Foundation.Heat.backwardProductVolume v

theorem CKN.Foundation.Heat.heatKernelPlus_locallyIntegrable_prod : MeasureTheory.LocallyIntegrable (fun (p : Parabolic.Vec3 × ℝ) => heatKernelPlus (have this := p; this)) backwardProductVolume

theorem CKN.Foundation.Heat.backwardTestKernel_locallyIntegrable : MeasureTheory.LocallyIntegrable backwardTestKernel backwardProductVolume

theorem CKN.Foundation.Heat.backwardTestPotential_smooth {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) : ContDiff ℝ ↑⊤ fun (v : Parabolic.Vec3 × ℝ) => backwardTestPotential ζ v

theorem CKN.Foundation.Heat.backwardTestPotential_hasFDerivAt {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (v : Parabolic.Vec3 × ℝ) : HasFDerivAt (fun (w : Parabolic.Vec3 × ℝ) => backwardTestPotential ζ w) (MeasureTheory.convolution backwardTestKernel (fderiv ℝ ζ) (ContinuousLinearMap.precompR (Parabolic.Vec3 × ℝ) (ContinuousLinearMap.lsmul ℝ ℝ)) backwardProductVolume v) v

theorem CKN.Foundation.Heat.test_slice_contDiff {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : Parabolic.Vec3) => ζ (y, t)

theorem CKN.Foundation.Heat.test_slice_hasCompactSupport {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζc : HasCompactSupport ζ) (t : ℝ) : HasCompactSupport fun (y : Parabolic.Vec3) => ζ (y, t)

theorem CKN.Foundation.Heat.heatConv_time_shift_tendsto {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (x : Parabolic.Vec3) (t : ℝ) : Filter.Tendsto (fun (s : ℝ) => heatConv s (fun (y : Parabolic.Vec3) => ζ (y, t + s)) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (ζ (x, t)))

theorem CKN.Foundation.Heat.timePartial_eq_fderiv_apply {F : Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (x : Parabolic.Vec3) (t : ℝ) : timePartial (have this := F; this) (x, t) = (fderiv ℝ F (x, t)) (0, 1)

theorem CKN.Foundation.Heat.spatialPartial_eq_fderiv_apply {F : Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (i : Fin 3) (x : Parabolic.Vec3) (t : ℝ) : spatialPartial (have this := F; this) i (x, t) = (fderiv ℝ F (x, t)) (basisVec i, 0)

theorem CKN.Foundation.Heat.backwardTestPotential_timePartial {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (x : Parabolic.Vec3) (t : ℝ) : timePartial (have this := fun (z : Parabolic.ParabolicPoint) => backwardTestPotential ζ z; this) (x, t) = backwardTestPotential (fun (z : Parabolic.Vec3 × ℝ) => timePartial (have this := ζ; this) z) (x, t)

theorem CKN.Foundation.Heat.backwardTestPotential_spatialPartial {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (i : Fin 3) (x : Parabolic.Vec3) (t : ℝ) : spatialPartial (have this := fun (z : Parabolic.ParabolicPoint) => backwardTestPotential ζ z; this) i (x, t) = backwardTestPotential (fun (z : Parabolic.Vec3 × ℝ) => spatialPartial (have this := ζ; this) i z) (x, t)

theorem CKN.Foundation.Heat.backwardTestPotential_spatialSecondPartial {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (i j : Fin 3) (x : Parabolic.Vec3) (t : ℝ) : spatialSecondPartial (have this := fun (z : Parabolic.ParabolicPoint) => backwardTestPotential ζ z; this) i j (x, t) = backwardTestPotential (fun (z : Parabolic.Vec3 × ℝ) => spatialSecondPartial (have this := ζ; this) i j z) (x, t)

theorem CKN.Foundation.Heat.shifted_time_hasDerivAt {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (x y : Parabolic.Vec3) (t r : ℝ) : HasDerivAt (fun (s : ℝ) => ζ (x - y, t + s)) (timePartial (have this := ζ; this) (x - y, t + r)) r

theorem CKN.Foundation.Heat.shifted_time_green {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (x y : Parabolic.Vec3) (t ε : ℝ) (hε : 0 < ε) : ∫ (r : ℝ) in Set.Ioi ε, heatKernelTimeDerivative y r * ζ (x - y, t + r) + heatKernel y r * timePartial (have this := ζ; this) (x - y, t + r) = -(heatKernel y ε * ζ (x - y, t + ε))

noncomputable def CKN.Foundation.Heat.backwardHeatKernel (z v : Parabolic.ParabolicPoint) : ℝ

Causal heat kernel pairing a later test point with an earlier source point.

Equations

• CKN.Foundation.Heat.backwardHeatKernel z v = CKN.Foundation.Heat.heatKernelPlus (z.1 - v.1, z.2 - v.2)

noncomputable def CKN.Foundation.Heat.backwardHeatSpatialKernel (i : Fin 3) (z v : Parabolic.ParabolicPoint) : ℝ

Spatial derivative kernel in the backward heat-potential pairing.

Equations

• CKN.Foundation.Heat.backwardHeatSpatialKernel i z v = CKN.Foundation.Heat.heatKernelSpaceDerivative (z.1 - v.1) (z.2 - v.2) i

noncomputable def CKN.Foundation.Heat.backwardHeatPotential (ζ : Parabolic.ParabolicPoint → ℝ) (v : Parabolic.ParabolicPoint) : ℝ

Backward heat potential obtained by integrating against the test variable.

Equations

• CKN.Foundation.Heat.backwardHeatPotential ζ v = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.Foundation.Heat.backwardHeatKernel z v * ζ z

noncomputable def CKN.Foundation.Heat.backwardHeatPotentialSpatial (i : Fin 3) (ζ : Parabolic.ParabolicPoint → ℝ) (v : Parabolic.ParabolicPoint) : ℝ

Spatial derivative of the backward heat potential, including the differentiation sign.

Equations

• CKN.Foundation.Heat.backwardHeatPotentialSpatial i ζ v = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.Foundation.Heat.backwardHeatSpatialKernel i z v * ζ z

theorem CKN.Foundation.Heat.backwardTestPotential_eq_backwardHeatPotential (ζ : Parabolic.Vec3 × ℝ → ℝ) (v : Parabolic.Vec3 × ℝ) : backwardTestPotential ζ v = backwardHeatPotential (have this := ζ; this) (have this := v; this)

theorem CKN.Foundation.Heat.backwardHeatKernel_eq_zero_of_nonpos {z v : Parabolic.ParabolicPoint} (h : z.2 - v.2 ≤ 0) : backwardHeatKernel z v = 0

theorem CKN.Foundation.Heat.backwardHeatSpatialKernel_eq_zero_of_nonpos {i : Fin 3} {z v : Parabolic.ParabolicPoint} (h : z.2 - v.2 ≤ 0) : backwardHeatSpatialKernel i z v = 0

theorem CKN.Foundation.Heat.backwardHeatPotential_eq_zero_of_future {ζ : Parabolic.ParabolicPoint → ℝ} {T : ℝ} {v : Parabolic.ParabolicPoint} (hv : T ≤ v.2) (hζ : ∀ (z : Parabolic.ParabolicPoint), T ≤ z.2 → ζ z = 0) : backwardHeatPotential ζ v = 0

theorem CKN.Foundation.Heat.backwardHeatPotentialSpatial_eq_zero_of_future {i : Fin 3} {ζ : Parabolic.ParabolicPoint → ℝ} {T : ℝ} {v : Parabolic.ParabolicPoint} (hv : T ≤ v.2) (hζ : ∀ (z : Parabolic.ParabolicPoint), T ≤ z.2 → ζ z = 0) : backwardHeatPotentialSpatial i ζ v = 0