Quantitative mass bound in the positive-phase plateau #
The absorbed half-space estimate and the global cutoff error bound control every fixed measurable part of the cutoff plateau.
theorem
ESS.bu_short_core_mass_bound :
∃ (a₀ : ℝ) (c : ℝ),
0 < a₀ ∧ 0 < c ∧ ∀ (scale R ε c₁ C₁ C₂ a : ℝ),
0 < scale →
scale ≤ 1 →
∀ (hR : 1 ≤ R),
0 < ε →
0 ≤ c₁ →
0 ≤ C₁ →
(∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁) →
0 ≤ C₂ →
(∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ C₂) →
c * 36 * (c₁ * scale) ^ 2 ≤ 1 / 2 →
max a₀ 1 < 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),
ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) →
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)
w Dw D2w Dtw →
(∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) →
(∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z))) →
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4 * (CKN.Foundation.Parabolic.vec3EuclideanNorm
(buAffineField (-scale ^ 2 / 2) scale w z) ^ 2 + CKN.spatialGradientSq (buAffineField (-scale ^ 2 / 2) scale w)
(buAffineDw (-scale ^ 2 / 2) scale Dw) z))
(buShortWideGapRegion scale) MeasureTheory.volume →
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
buShortShiftedWeight scale a z * (1 + z.1 2) ^ 4 * (CKN.Foundation.Parabolic.vec3EuclideanNorm
(buAffineField (-scale ^ 2 / 2) scale w z) ^ 2 + CKN.spatialGradientSq (buAffineField (-scale ^ 2 / 2) scale w)
(buAffineDw (-scale ^ 2 / 2) scale Dw) z))
(buShortHighStrip scale) MeasureTheory.volume →
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
buShortShiftedWeight scale a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm
(buAffineField (-scale ^ 2 / 2) scale w z) ^ 2 + CKN.spatialGradientSq (buAffineField (-scale ^ 2 / 2) scale w)
(buAffineDw (-scale ^ 2 / 2) scale Dw) z))
(buShortHighStrip scale) MeasureTheory.volume →
∀ (S : Set CKN.Foundation.Parabolic.ParabolicPoint),
MeasurableSet S →
(∀ z ∈ S,
CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortCoreRegion scale R ε) →
have K := buCutSupportSet (buShortFullCutoff scale R ⋯ ε);
have v := buAffineField (-scale ^ 2 / 2) scale w;
have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw;
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, buShortShiftedWeight scale a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ 4 * c * (((4 * buShortUniformErrorCoeff scale c₁ C₁ C₂ ^ 2 * Real.exp (-(a * buShortD scale)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortWideGapRegion scale, Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4 * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z)) + 4 * buShortShellCoeff scale R c₁ ^ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortHighStrip scale, buShortShiftedWeight scale a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z)) + 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortShiftedWeight scale a z * (if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then
8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)
else 0) ^ 2)
The mass on a fixed cutoff plateau is controlled by the negative phase gap, spatial shell, and lower-time transition.