Rescaled data on the unit cylinder

Fix a Leray–Hopf solution on ℝ³ × (0, T), a point x₀, a time 0 < t₀ ≤ T and a radius R with R² ≤ t₀. The parabolic rescaling u_R(y, s) = R u(x₀ + R y, t₀ + R² s) places the cylinder B_R(x₀) × (t₀ - R², t₀), which may end at the terminal time T, onto the unit cylinder B₁ × (-1, 0). This file proves the measurability, energy, slice, pressure and weak-gradient hypotheses of thm:ess-local for the rescaled fields, as used in the proof of lem:pv-positive-bound.

theorem ESS.pv_unit_subset_rescaled_slab {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) ⊆ CKN.scalingParabolic R (x₀, t₀) ⁻¹' CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)

The unit cylinder lies in the rescaled slab.

theorem ESS.pv_unit_time_subset_rescaled {T t₀ R : ℝ} (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) : Set.Ioo (-1) 0 ⊆ CKN.rescaledTime R t₀ (Set.Ioo 0 T)

The unit time interval lies in the rescaled time interval.

theorem ESS.pv_unit_aestronglyMeasurable_comp {E : Type} [TopologicalSpace E] {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : MeasureTheory.AEStronglyMeasurable (f ∘ CKN.scalingParabolic R (x₀, t₀)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))

A field that is almost everywhere strongly measurable on the slab rescales to one that is almost everywhere strongly measurable on the unit cylinder.

theorem ESS.pv_unit_slice_essSup_le {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) (g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Φ : CKN.Foundation.Parabolic.Vec3 → ENNReal) {c K : ENNReal} (hc : c ≠ ⊤) (hΦ : ∀ (v : CKN.Foundation.Parabolic.Vec3), Φ (R • v) = c * Φ v) (hK : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), Φ (g (y, τ)) ≤ K) : essSup (fun (s : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, Φ (CKN.rescaleVelocity R (x₀, t₀) g (x, s))) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) ≤ c * (ENNReal.ofReal (R⁻¹ ^ 3) * K)

Slice bounds of a homogeneous nonnegative functional pass to the unit ball under rescaling.

theorem ESS.pv_unit_L2_essSup_lt_top {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hL2 : essSup (fun (s : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖u (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤) : essSup (fun (s : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖CKN.rescaleVelocity R (x₀, t₀) u (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤

The rescaled velocity has essentially bounded L² norms on the unit ball.

theorem ESS.pv_unit_L3_essSup_lt_top {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤) : essSup (fun (s : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (CKN.rescaleVelocity R (x₀, t₀) u (x, s))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤

The rescaled velocity has essentially bounded critical L³ norms on the unit ball.

theorem ESS.pv_unit_energy_lt_top {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hEnergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖CKN.rescaleVelocity R (x₀, t₀) u z‖ₑ ^ 2 + ‖CKN.rescaleGradient R (x₀, t₀) Du z‖ₑ ^ 2 < ⊤

The rescaled velocity and gradient have finite energy on the unit cylinder.

theorem ESS.pv_unit_weakGradient {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hU : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hGrad : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u (x, s) i) fun (x : CKN.Vec 3) => Du (x, s) i) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => CKN.rescaleVelocity R (x₀, t₀) u (x, s) i) fun (x : CKN.Vec 3) => CKN.rescaleGradient R (x₀, t₀) Du (x, s) i

The rescaled velocity has a weak spatial gradient on almost every slice of the unit cylinder.