A high-strip cell bound from its velocity average #
Caccioppoli controls the full quadratic energy by the velocity average; a bounded scalar factor then multiplies the estimate.
theorem
ESS.bu_short_cell_weighted_average_bound
(scale c b Cw : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hc : 0 ≤ c)
(hCw : 0 ≤ Cw)
(k : ℤ)
(hk : 1 ≤ k)
(m : Fin 3 → ℤ)
(ell : Fin 2048)
{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}
(hcont : ContinuousOn v ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico (1 / 2) (3 / 2)))
(hweak :
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)) v Dv D2v Dtv)
(hlocal :
∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2))), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (√(CKN.spatialGradientSq v Dv z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)))
(W : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hWcont : ContinuousOn W {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2})
(hW :
∀ z ∈ buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale,
0 ≤ W z ∧ W z ≤ Cw * Real.exp
(-((CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 0 ^ 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 1 ^ 2) / 8) * Real.exp (b * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 2 ^ 2))
(z₀ : CKN.Foundation.Parabolic.ParabolicPoint)
(hz₀ : z₀ ∈ buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale)
:
have d := CKN.Foundation.buSmallTimeDyadicScale k;
have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1;
have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2;
have Avg :=
CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4));
have Ce := 1 + 256 * (1 + c ^ 2 + 128);
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale, W z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z) ≤ Cw * Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8) * Real.exp (b * Y 2 ^ 2) * (Ce / d) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Avg, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2
A fixed nonnegative weight on a high-strip cell is bounded by the
Gaussian velocity average with one inverse dyadic factor
(lem:bu-small-time).