Energy on shifted dyadic cells

The energy of each shifted cell is bounded by the Gaussian velocity average and the local Caccioppoli estimate.

theorem ESS.bu_short_shifted_cell_energy_le_average (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (C : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hAvgInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 √(3 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 2)) (Set.Ioo (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 2) (1 / 2 + 5 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 4))) MeasureTheory.volume) (hGradInt : MeasureTheory.IntegrableOn (CKN.spatialGradientSq v Dv) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8)) (Set.Ioo (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 - (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8) ^ 2 / 2) (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 - (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8) ^ 2 / 2 + (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8) ^ 2))) MeasureTheory.volume) (hCacc : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8)) (Set.Ioo (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 - (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8) ^ 2 / 2) (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 - (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8) ^ 2 / 2 + (√(CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 8) ^ 2)), CKN.spatialGradientSq v Dv z ≤ C * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 √(3 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 2)) (Set.Ioo (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 2) (1 / 2 + 5 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 4)), CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortShiftedDyadicCell k m ell, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z ≤ (1 + C) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 √(3 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 2)) (Set.Ioo (1 / 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 2) (1 / 2 + 5 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 / 4)), CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2

Combining the local gradient estimate with containment of a dyadic cell in its averaging box bounds its quadratic energy (lem:bu-small-time).