Gaussian tail weights

The time weight comparison used in lem:bu-gaussian#weight-decay.

noncomputable def ESS.buGaussianBeta : ℝ

The fixed Gaussian decay exponent in the manuscript.

Equations

• ESS.buGaussianBeta = 1 / 10 ^ 6

noncomputable def ESS.buGaussianH : ℝ

The logarithmic time weight at time 3/2 in the manuscript.

Equations

• ESS.buGaussianH = Real.log (CKN.gaussCarlemanTimeWeight (3 / 2))

noncomputable def ESS.buGaussianLogTailExponent (a ρ s : ℝ) : ℝ

The logarithmic exponent of the collar Gaussian weight.

Equations

• ESS.buGaussianLogTailExponent a ρ s = -2 * a * Real.log (CKN.gaussCarlemanTimeWeight s) - ρ ^ 2 / (32 * s)

theorem ESS.buGaussian_log_tail_monotone {a ρ β H : ℝ} (hH : 0 < H) (hβ : 0 < β) (hβH : β / H < 1 / 96) (ha : a = β * ρ ^ 2 / H) : MonotoneOn (buGaussianLogTailExponent a ρ) (Set.Icc (1 / 6) 2)

The logarithmic Gaussian tail exponent increases up to time 2 (lem:bu-gaussian#weight-decay).

theorem ESS.buGaussian_weight_eq_exp_log_tail {a ρ s : ℝ} (hs : 0 < s) : CKN.gaussCarlemanTimeWeight s ^ (-2 * a) * Real.exp (-ρ ^ 2 / (32 * s)) = Real.exp (buGaussianLogTailExponent a ρ s)

The collar weight equals the exponential of its logarithmic exponent on positive times.

theorem ESS.buGaussian_source_weight_parameters : 0 < buGaussianBeta ∧ buGaussianBeta ≤ 1 / 128 ∧ 0 < buGaussianH ∧ buGaussianBeta / buGaussianH < 1 / 96

The manuscript constants satisfy the hypotheses of the Gaussian log-weight estimate.

theorem ESS.buGaussian_time_weight_log_two_nonneg : 0 ≤ Real.log (CKN.gaussCarlemanTimeWeight 2)

The late endpoint of the Gaussian time weight is at least its value at time 3/2, so its logarithm is nonnegative.

theorem ESS.buGaussian_time_weight_endpoint {a ρ : ℝ} (ha : a = buGaussianBeta * ρ ^ 2 / buGaussianH) : CKN.gaussCarlemanTimeWeight (3 / 2) ^ (-2 * a) = Real.exp (-2 * buGaussianBeta * ρ ^ 2)

The spatially independent endpoint of the Carleman time weight is the source Gaussian factor (lem:bu-gaussian#weight-decay).

theorem ESS.buGaussian_time_weight_late_decreasing {a s : ℝ} (ha : 0 ≤ a) (hslo : 3 / 2 ≤ s) (hshi : s ≤ 2) : CKN.gaussCarlemanTimeWeight s ^ (-2 * a) ≤ CKN.gaussCarlemanTimeWeight (3 / 2) ^ (-2 * a)

The negative time power decreases on the late-time collar.

theorem ESS.buGaussian_omega2_pointwise_bound {a β ρ A barA scale s : ℝ} {x y : CKN.Foundation.Parabolic.Vec3} (ha : 0 ≤ a) (hA : 0 ≤ A) (hAbar : A ≤ barA) (hslo : 3 / 2 ≤ s) (hshi : s ≤ 2) (hsmall : 4 * A * scale ^ 2 ≤ 1 / (8 * s)) (hendpoint : CKN.gaussCarlemanTimeWeight (3 / 2) ^ (-2 * a) = Real.exp (-2 * β * ρ ^ 2)) (v : CKN.Foundation.Parabolic.Vec3) (hgrowth : CKN.Foundation.Parabolic.vec3EuclideanNorm v ≤ Real.exp (2 * A * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2 + 2 * A * scale ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm y ^ 2)) : CKN.gaussCarlemanTimeWeight s ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm y ^ 2 / (4 * s)) * CKN.Foundation.Parabolic.vec3EuclideanNorm v ^ 2 ≤ Real.exp (8 * barA * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2) * Real.exp (-2 * β * ρ ^ 2) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm y ^ 2 / (8 * s))

The mass-only part of the late-time collar error has the source Gaussian bound (eq:bu-gaussian-collar).

theorem ESS.buGaussian_source_spatial_absorption {A scale s : ℝ} (hA : 0 ≤ A) (hA0 : A ≤ 1 / 10 ^ 12) (hscale : scale ^ 2 ≤ 1 / 4) (hslo : 3 / 2 ≤ s) (hshi : s ≤ 2) : 4 * A * scale ^ 2 ≤ 1 / (8 * s)

The manuscript growth threshold makes the transverse Gaussian absorb the rescaled growth on the late-time collar (eq:bu-gaussian-collar).

theorem ESS.buGaussian_source_spatial_absorption_all_times {A scale s : ℝ} (hA : 0 ≤ A) (hA0 : A ≤ 1 / 10 ^ 12) (hscale : scale ^ 2 ≤ 1 / 4) (hs : 0 < s) (hs2 : s ≤ 2) : 4 * A * scale ^ 2 ≤ 1 / (8 * s)

The small source growth is absorbed by the transverse Gaussian at every positive Carleman time up to two.

theorem ESS.buGaussian_radial_weighted_pointwise_bound {a ρ A barA scale s : ℝ} {x y : CKN.Foundation.Parabolic.Vec3} (hA : 0 ≤ A) (hA0 : A ≤ 1 / 10 ^ 12) (hAbar : A ≤ barA) (hρ : 0 < ρ) (hscale : scale ^ 2 ≤ 1 / 4) (hs : 0 < s) (hs2 : s ≤ 2) (hradial : ρ / 2 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y) (v : CKN.Foundation.Parabolic.Vec3) (hgrowth : CKN.Foundation.Parabolic.vec3EuclideanNorm v ≤ Real.exp (2 * A * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2 + 2 * A * scale ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm y ^ 2)) : ucGaussianWeight a (y, s) * CKN.Foundation.Parabolic.vec3EuclideanNorm v ^ 2 ≤ Real.exp (8 * barA * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2) * Real.exp (buGaussianLogTailExponent a ρ s)

On a radial collar outside ρ/2, the weighted field is bounded by the one-dimensional logarithmic tail used in eq:bu-gaussian-collar.

theorem ESS.buGaussian_log_tail_integral_bound {a ρ β H : ℝ} (hH : 0 < H) (hβ : 0 < β) (hβsmall : β ≤ 1 / 128) (hβH : β / H < 1 / 96) (ha : a = β * ρ ^ 2 / H) : ∫ (s : ℝ) in 1 / 6..2, Real.exp (buGaussianLogTailExponent a ρ s) ≤ 2 * Real.exp (-2 * β * ρ ^ 2)

The weight integral is bounded by its exponentially small endpoint value (lem:bu-gaussian#weight-decay).

theorem ESS.buGaussian_polynomial_tail_bound {β H ρ : ℝ} (hβ : 0 < β) (hH : 0 < H) (hρ : 1 ≤ ρ) : (1 + β / H * ρ ^ 2) * (1 + ρ) ^ 2 * Real.exp (-2 * β * ρ ^ 2) ≤ 16 * (1 + β / H) / β ^ 2 * Real.exp (-β * ρ ^ 2)

The collar polynomial is absorbed by the remaining Gaussian factor (lem:bu-gaussian#weight-decay).

theorem ESS.buGaussian_source_log_tail_integral_bound {a ρ : ℝ} (ha : a = buGaussianBeta * ρ ^ 2 / buGaussianH) : ∫ (s : ℝ) in 1 / 6..2, Real.exp (buGaussianLogTailExponent a ρ s) ≤ 2 * Real.exp (-2 * buGaussianBeta * ρ ^ 2)

The preceding interval estimate with the fixed manuscript exponent and time weight.