The Gaussian average estimate for backward uniqueness

The cutoff equals the translated field on the normalized averaging box in lem:bu-gaussian.

theorem ESS.buGaussian_shifted_cutoff_data_zero_late {ρ ε : ℝ} (hρ : 0 < ρ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : have κ := fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ucCutoffScalar (ucSpatialCutoff ρ hρ) (fun (s : ℝ) => ucFinalTimeCutoff (s - 1 / 6)) (fun (s : ℝ) => ucInitialTimeCutoff ε (s - 1 / 6)) q; (∀ z ∉ buCutSupportSet κ, buGaussianShiftedCutoffField ρ hρ ε v z = 0 ∧ buGaussianShiftedCutoffDw ρ hρ ε v Dv z = 0 ∧ buGaussianShiftedCutoffD2w ρ hρ ε v Dv D2v z = 0 ∧ buGaussianShiftedCutoffDtw ρ hρ ε v Dtv z = 0) ∧ ∀ z ∈ buCutSupportSet κ, z.2 ≤ 23 / 12

theorem ESS.buGaussian_sq_four_sum (a b c d : ℝ) : (a + b + c + d) ^ 2 ≤ 4 * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2)

theorem ESS.buGaussian_sq_main_sum (a b : ℝ) : (a + 3 * b) ^ 2 ≤ 2 * a ^ 2 + 18 * b ^ 2

theorem ESS.buGaussian_weighted_four_error_bound {W q m g c b d e h : ℝ} (hW : 0 ≤ W) (hq : 1 / 2 ≤ q) (hm : 0 ≤ m) (hg : 0 ≤ g) (hh : 0 ≤ h) (hOp : h ≤ c * (√m + 3 * √g) + b + d + e) : W * h ^ 2 ≤ 72 * c ^ 2 * W * (q * m + g) + 4 * W * (b ^ 2 + d ^ 2 + e ^ 2)

The main differential term is absorbed by the Gaussian Carleman energy; the remaining three terms retain their individual squares.

theorem ESS.buGaussian_time_slice_null (B : Set CKN.Foundation.Parabolic.Vec3) (s : ℝ) : MeasureTheory.volume (CKN.spaceTimeSet B {s}) = 0

A fixed time slice of a space-time cylinder has zero volume.

theorem ESS.buGaussian_ae_time_ne (s : ℝ) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≠ s

Almost every parabolic point avoids a prescribed time.

theorem ESS.buGaussian_indicator_integral_nonneg {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (K S : Set X) (f : X → ℝ) (hf : 0 ≤ᵐ[μ.restrict K] f) : 0 ≤ ∫ (z : X) in K, S.indicator f z ∂μ

Restricting a nonnegative integrand to another measurable region leaves its integral nonnegative.

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

theorem ESS.buGaussian_shifted_trace_strip_tendsto {B : Set CKN.Foundation.Parabolic.Vec3} {σ : ℝ} (hB : MeasurableSet B) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (htrace : Filter.Tendsto (fun (ε : ℝ) => (∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ Set.Ioc ε (2 * ε), CKN.Foundation.Parabolic.vec3EuclideanNorm (u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)) ^ 2) / ε ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : Filter.Tendsto (fun (ε : ℝ) => (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet B (Set.Ioc (σ + ε) (σ + 2 * ε)), CKN.Foundation.Parabolic.vec3EuclideanNorm (u ((buGaussianTimeShiftPoint σ).symm z)) ^ 2) / ε ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem ESS.buGaussian_local_cylinder_volume_bound {ρ : ℝ} (hρ : 0 < ρ) : (MeasureTheory.volume (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2))).toReal ≤ 12 * ρ ^ 3