Local integrability of weighted cell energy #
Bounded scalar factors preserve the local quadratic energy integral on cell fragments in the high normal strip.
theorem
ESS.bu_short_cell_fragment_energy_integrable
(scale : ℝ)
(hscale : 0 < scale)
(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}
(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 < ⊤)
:
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z)
(buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale) MeasureTheory.volume
Extended local quadratic data make the rescaled energy integrable on each shifted dyadic cell fragment in the high strip.
theorem
ESS.bu_short_cell_fragment_density_integrable
(scale : ℝ)
(hscale : 0 < scale)
(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}
(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 < ⊤)
(W : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hWcont : ContinuousOn W {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2})
(C : ℝ)
(hWbound : ∀ z ∈ buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale, ‖W z‖ ≤ C)
:
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
W z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z))
(buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale) MeasureTheory.volume
A continuous scalar factor bounded on the cell fragment multiplies
its locally integrable quadratic energy (lem:bu-small-time).