Gaussian weight comparison on collar cells #
The Gaussian weight changes by a fixed factor on each enlarged space-time cell when the parabolic radius is chosen from the Carleman parameter.
theorem
ESS.buGaussian_weight_cell_comparison
{ρ a r σ δ : ℝ}
(hρ : 0 < ρ)
(ha : 0 < a)
(hr : 0 < r)
(hσ : σ = 1 / 6)
(hδ : δ = r ^ 2)
{x y : CKN.Foundation.Parabolic.Vec3}
{s t : ℝ}
(hyx : CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) < 2 * r)
(hyρ : CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ ρ)
(hxρ : CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ ρ)
(hs : σ ≤ s)
(ht : σ ≤ t)
(hdt : |s - t| ≤ 4 * δ)
:
The Carleman weight varies by a uniform factor over an outer collar cell.
The displayed exponent is expressed in the geometric cell parameters so it
can be bounded using the fixed product ρ r.