Continuity of the local endpoint energy

Local suitability makes the cubic velocity and pressure densities integrable on compact subsets of the open cylinder. Dominated convergence then gives continuity of the energy when an interior cylinder is translated.

noncomputable def ESS.goodPointEnergyDensity (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal

The velocity-cubed and pressure-to-the-three-halves density used at good points.

Equations

• ESS.goodPointEnergyDensity u p z = ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2)

theorem ESS.goodPointEnergy_continuousAt_of_compact {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hdata : CKN.IsSuitableWeakSolutionData (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) 3 u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) (hKsub : K ⊆ goodPointDomain) {z₀ : CKN.Foundation.Parabolic.ParabolicPoint} {r δ : ℝ} (hδ : 0 < δ) (hnear : ∀ (c : CKN.Foundation.Parabolic.ParabolicPoint), CKN.Foundation.Parabolic.parabolicDist c z₀ < δ → CKN.Foundation.Parabolic.parabolicCylinder c.1 c.2 r ⊆ K) : Filter.Tendsto (fun (c : CKN.Foundation.Parabolic.ParabolicPoint) => goodPointEnergy u p c.1 c.2 r) (nhds z₀) (nhds (goodPointEnergy u p z₀.1 z₀.2 r))

The energy in a fixed interior-radius cylinder is continuous as its center varies, provided nearby cylinders stay in a compact subset of the domain.