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_cutoff_field_eq_on_average_box {ρ ε : ℝ} (hρ : 4 < ρ) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 12) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet (Metric.ball 0 1) (Set.Ioo (1 / 2) 1)) : ucCutoffScalar (ucSpatialCutoff ρ ⋯) (fun (s : ℝ) => ucFinalTimeCutoff (s - 1 / 6)) (fun (s : ℝ) => ucInitialTimeCutoff ε (s - 1 / 6)) z = 1 ∧ buGaussianShiftedCutoffField ρ ⋯ ε v z = buGaussianShiftedField (1 / 6) v z

theorem ESS.buGaussian_metric_average_physical_integrable (A : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hderiv : CKN.HasSpaceTimeWeakDerivs buHalfSpace (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ S ⊆ buHalfCylinder, Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hgrowth : ∀ z ∈ buHalfCylinder, CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (A * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) (x : CKN.Foundation.Parabolic.Vec3) (scale t : ℝ) (hx₃ : 2 < x 2) (hscalele : scale ≤ 1) (ht : 0 < t) (httop : 5 * t / 2 < 1) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (Metric.ball x scale) (Set.Ioo t (5 * t / 2))) MeasureTheory.volume

theorem ESS.buGaussian_change_back_metric_average (x : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (hscale : 0 < scale) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (Metric.ball x scale) (Set.Ioo (scale ^ 2 / 3) (5 * scale ^ 2 / 6))) MeasureTheory.volume) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball 0 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianAverageScaledField x scale (1 / 6) w z) ^ 2 = (scale ^ 5)⁻¹ * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball x scale) (Set.Ioo (scale ^ 2 / 3) (5 * scale ^ 2 / 6)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2

theorem ESS.buGaussian_shifted_scalar_derivatives {ρ ε : ℝ} (hρ : 0 < ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j k : Fin 3) : CKN.spatialPartial (ucCutoffScalar (ucSpatialCutoff ρ hρ) (fun (s : ℝ) => ucFinalTimeCutoff (s - 1 / 6)) fun (s : ℝ) => ucInitialTimeCutoff ε (s - 1 / 6)) j z = CKN.spatialPartial (ucGaussianCutoff ρ hρ ε) j ((buGaussianTimeShiftPoint (-1 / 6)) z) ∧ CKN.spatialSecondPartial (ucCutoffScalar (ucSpatialCutoff ρ hρ) (fun (s : ℝ) => ucFinalTimeCutoff (s - 1 / 6)) fun (s : ℝ) => ucInitialTimeCutoff ε (s - 1 / 6)) j k z = CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) j k ((buGaussianTimeShiftPoint (-1 / 6)) z) ∧ CKN.timePartial (ucCutoffScalar (ucSpatialCutoff ρ hρ) (fun (s : ℝ) => ucFinalTimeCutoff (s - 1 / 6)) fun (s : ℝ) => ucInitialTimeCutoff ε (s - 1 / 6)) z = CKN.timePartial (ucGaussianCutoff ρ hρ ε) ((buGaussianTimeShiftPoint (-1 / 6)) z)

theorem ESS.buGaussian_average_time_weight_le_one {s : ℝ} (hs : s ∈ Set.Icc (1 / 2) 1) : CKN.gaussCarlemanTimeWeight s ≤ 1

theorem ESS.buGaussian_carleman_mass_density_lower {a ρ ε : ℝ} (hρ : 4 < ρ) (ha : 1 ≤ a) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 12) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet (Metric.ball 0 1) (Set.Ioo (1 / 2) 1)) : Real.exp (-(3 / 2)) * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField (1 / 6) v z) ^ 2 ≤ ucGaussianWeight a z * (a / z.2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedCutoffField ρ ⋯ ε v z) ^ 2

theorem ESS.buGaussian_shifted_cutoff_heat_eq_raw {ρ ε : ℝ} (hρ : 0 < ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (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) : ucCutoffHeat (ucSpatialCutoff ρ hρ) (fun (s : ℝ) => ucFinalTimeCutoff (s - 1 / 6)) (fun (s : ℝ) => ucInitialTimeCutoff ε (s - 1 / 6)) (buGaussianShiftedField (1 / 6) v) (buGaussianShiftedDw (1 / 6) Dv) (buGaussianShiftedD2w (1 / 6) D2v) (buGaussianShiftedDtw (1 / 6) Dtv) z = ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv ((buGaussianTimeShiftPoint (1 / 6)).symm z)

theorem ESS.buGaussian_shifted_cutoff_field_dw_eq_raw {ρ ε : ℝ} (hρ : 0 < ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : buGaussianShiftedCutoffField ρ hρ ε v z = ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v ((buGaussianTimeShiftPoint (1 / 6)).symm z) ∧ buGaussianShiftedCutoffDw ρ hρ ε v Dv z = ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv ((buGaussianTimeShiftPoint (1 / 6)).symm z)

theorem ESS.buGaussian_shifted_operator_localized_ae_bound {ρ ε c₁ scale : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hεsmall : 2 * ε ≤ 1 / 2) (hc₁ : 0 ≤ c₁) (hscale : 0 ≤ scale) (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) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (buGaussianShiftedCutoffD2w ρ hρ ε v Dv D2v) (buGaussianShiftedCutoffDtw ρ hρ ε v Dtv) z) ≤ ((c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedCutoffField ρ hρ ε v z) + 3 * √(CKN.spatialGradientSq (buGaussianShiftedCutoffField ρ hρ ε v) (buGaussianShiftedCutoffDw ρ hρ ε v Dv) z)) + if z.1 ∈ {y : CKN.Foundation.Parabolic.Vec3 | 13 * ρ / 20 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ 3 * ρ / 4} then (32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2) + 3 * c₁ * scale * (CKN.cutoffGradientConstant / ρ)) * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField (1 / 6) v z) + 18 * (CKN.cutoffGradientConstant / ρ) * √(CKN.spatialGradientSq (buGaussianShiftedField (1 / 6) v) (buGaussianShiftedDw (1 / 6) Dv) z) else 0) + if 3 / 2 ≤ ((buGaussianTimeShiftPoint (1 / 6)).symm z).2 ∧ ((buGaussianTimeShiftPoint (1 / 6)).symm z).2 ≤ 7 / 4 then 32 * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField (1 / 6) v z) else 0) + if ε ≤ ((buGaussianTimeShiftPoint (1 / 6)).symm z).2 ∧ ((buGaussianTimeShiftPoint (1 / 6)).symm z).2 ≤ 2 * ε then 8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField (1 / 6) v z) else 0