The backward Gaussian test function at a general base point

For a base point z₀ = (x₀, t₀) the paper's backward Gaussian test function of eq:psi-r is ψ_r(x, t) = r² G(x - x₀, r² - (t - t₀)), the translate of the canonical-center function backwardHeatTestFunction. This file records the translated test function and proves the statements of eq:psi-backward, eq:psi-lower, eq:psi-upper, eq:grad-psi, and eq:psi-far of paper/ckn.tex at an arbitrary base point, keeping the constants of the canonical-center statements exactly.

noncomputable def CKN.Foundation.Heat.centeredBackwardHeatTest (x₀ : Parabolic.Vec3) (t₀ r : ℝ) (z : Parabolic.ParabolicPoint) : ℝ

The backward Gaussian test function ψ_r of eq:psi-r based at z₀ = (x₀, t₀), namely x ↦ r² G(x - x₀, r² - (t - t₀)) on a parabolic point z = (x, t).

Equations

• CKN.Foundation.Heat.centeredBackwardHeatTest x₀ t₀ r z = CKN.Foundation.Heat.backwardHeatTestFunction r (z.1 - x₀) (z.2 - t₀)

noncomputable def CKN.Foundation.Heat.centeredBackwardHeatTestGradientNorm (x₀ : Parabolic.Vec3) (t₀ r : ℝ) (z : Parabolic.ParabolicPoint) : ℝ

The Euclidean norm |∇ψ_r| of eq:grad-psi for the backward Gaussian test function based at z₀ = (x₀, t₀).

Equations

• CKN.Foundation.Heat.centeredBackwardHeatTestGradientNorm x₀ t₀ r z = CKN.Foundation.Heat.backwardHeatTestGradientNorm r (z.1 - x₀) (z.2 - t₀)

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_spatialPartial {x₀ : Parabolic.Vec3} {t₀ r : ℝ} {z : Parabolic.ParabolicPoint} (ht : z.2 - t₀ < r ^ 2) (i : Fin 3) : spatialPartial (centeredBackwardHeatTest x₀ t₀ r) i z = r ^ 2 * heatKernelSpaceDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i

The first spatial derivative of the backward Gaussian test function based at z₀ = (x₀, t₀) is the corresponding translate of heatKernelSpaceDerivative, scaled by r².

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_timePartial {x₀ : Parabolic.Vec3} {t₀ r : ℝ} {z : Parabolic.ParabolicPoint} (ht : z.2 - t₀ < r ^ 2) : timePartial (centeredBackwardHeatTest x₀ t₀ r) z = -r ^ 2 * heatKernelTimeDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀))

The time derivative of the backward Gaussian test function based at z₀ = (x₀, t₀) is the corresponding translate of heatKernelTimeDerivative, scaled by -r².

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_secondSpatialPartial {x₀ : Parabolic.Vec3} {t₀ r : ℝ} {z : Parabolic.ParabolicPoint} (ht : z.2 - t₀ < r ^ 2) (i : Fin 3) : spatialSecondPartial (centeredBackwardHeatTest x₀ t₀ r) i i z = r ^ 2 * heatKernelSpaceSecondDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i

The second spatial derivative of the backward Gaussian test function based at z₀ = (x₀, t₀) is the corresponding translate of heatKernelSpaceSecondDerivative, scaled by r².

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_heat_equation {x₀ : Parabolic.Vec3} {t₀ r : ℝ} {z : Parabolic.ParabolicPoint} (ht : z.2 < t₀ + r ^ 2) : timePartial (centeredBackwardHeatTest x₀ t₀ r) z + ∑ i : Fin 3, spatialSecondPartial (centeredBackwardHeatTest x₀ t₀ r) i i z = 0

eq:psi-backward: the backward Gaussian test function based at z₀ = (x₀, t₀) solves the backward heat equation on {z | z.2 < t₀ + r²}.

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_lower_on_cylinder {x₀ : Parabolic.Vec3} {t₀ r : ℝ} (hr : 0 < r) {z : Parabolic.ParabolicPoint} (hz : z ∈ Parabolic.parabolicCylinder x₀ t₀ r) : 1 / (2000 * r) ≤ centeredBackwardHeatTest x₀ t₀ r z

eq:psi-lower: the backward Gaussian test function based at z₀ = (x₀, t₀) is bounded below by 1/(2000 r) on the cylinder Cyl(r, z₀).

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_upper_on_cylinder {x₀ : Parabolic.Vec3} {t₀ r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) {z : Parabolic.ParabolicPoint} (hz : z ∈ Parabolic.parabolicCylinder x₀ t₀ ρ) : centeredBackwardHeatTest x₀ t₀ r z ≤ 1000 / r

eq:psi-upper, first part: the backward Gaussian test function based at z₀ = (x₀, t₀) is bounded above by 1000/r on the cylinder Cyl(ρ, z₀).

theorem CKN.Foundation.Heat.centeredBackwardHeatTest_upper_on_annulus {x₀ : Parabolic.Vec3} {t₀ r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hscale : r ≤ ρ / 2) {z : Parabolic.ParabolicPoint} (hz : z ∈ Parabolic.parabolicCylinder x₀ t₀ ρ \ Parabolic.parabolicCylinder x₀ t₀ (ρ / 2)) : centeredBackwardHeatTest x₀ t₀ r z ≤ 8000000 * r ^ 2 / ρ ^ 3

eq:psi-far, first part: the backward Gaussian test function based at z₀ = (x₀, t₀) is bounded above by 8000000 r²/ρ³ on the annulus Cyl(ρ, z₀) \ Cyl(ρ/2, z₀) when r ≤ ρ/2.

theorem CKN.Foundation.Heat.centeredBackwardHeatTestGradient_upper_on_annulus {x₀ : Parabolic.Vec3} {t₀ r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hscale : r ≤ ρ / 2) {z : Parabolic.ParabolicPoint} (hz : z ∈ Parabolic.parabolicCylinder x₀ t₀ ρ \ Parabolic.parabolicCylinder x₀ t₀ (ρ / 2)) : centeredBackwardHeatTestGradientNorm x₀ t₀ r z ≤ 5000000 * r ^ 2 / ρ ^ 4

eq:psi-far and eq:grad-psi: the gradient norm of the backward Gaussian test function based at z₀ = (x₀, t₀) is bounded above by 5000000 r²/ρ⁴ on the annulus Cyl(ρ, z₀) \ Cyl(ρ/2, z₀) when r ≤ ρ/2.