Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.BlowupLimitAssemblyPressureLimit

The whole-space pressure of the blow-up limit #

The limit velocity of prop:blowup-limit has bounded L³ slices for all negative times, so its tensor is in space-time L^(3/2) on every finite past window. The pressure P[u ⊗ u] of the limit is assembled from the Riesz pressures of these time-truncated tensors, which agree on common windows.

source
noncomputable def ESS.blowupLimitAssemblyPressureWindowTensor (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (n : ℕ) :
Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The velocity tensor of a field, truncated to the past window (-(n + 1), 0).

Equations
Instances For
    source
    noncomputable def ESS.blowupLimitAssemblyPressureLimit (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hG : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (blowupLimitAssemblyPressureWindowTensor U n i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) :
    CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

    The whole-space pressure of a field with truncated tensors in L^(3/2): at time t < 0 it is the Riesz pressure of the tensor truncated to the window (-(⌈-t⌉ + 1), 0).

    Equations
    Instances For
      source
      theorem ESS.blowupLimitAssemblyPressure_tensor_memLp_of_restrict {U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hS : MeasurableSet S) (hU : MeasureTheory.MemLp U 3 (MeasureTheory.volume.restrict S)) (i j : Fin 3) :
      MeasureTheory.MemLp (S.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U z i * U z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

      A field in L³ of a set has its tensor, truncated to that set, in whole-space L^(3/2).

      source
      theorem ESS.blowupLimitAssemblyPressure_window_agree (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hG : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (blowupLimitAssemblyPressureWindowTensor U n i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {n m : ℕ} (hnm : n ≤ m) :
      ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z ∈ Set.univ ×ˢ Set.Ioo (-(↑n + 1)) 0 → CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressureLimit._proof_1 (blowupLimitAssemblyPressureWindowTensor U m) ⋯ z = CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressureLimit._proof_1 (blowupLimitAssemblyPressureWindowTensor U n) ⋯ z

      Riesz pressures of truncations to nested windows agree on the smaller window.

      source
      theorem ESS.measurable_blowupLimitAssemblyPressureLimit (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hG : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (blowupLimitAssemblyPressureWindowTensor U n i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) :
      Measurable (blowupLimitAssemblyPressureLimit U hG)

      The assembled limit pressure is measurable.

      source
      theorem ESS.blowupLimitAssemblyPressureLimit_ae_eq (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hG : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (blowupLimitAssemblyPressureWindowTensor U n i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (T : ℝ) :
      blowupLimitAssemblyPressureLimit U hG =ᵐ[MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-T) 0)] CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressureLimit._proof_1 (blowupLimitAssemblyPressureWindowTensor U ⌈T⌉₊) ⋯

      On each past window the assembled limit pressure is the Riesz pressure of one truncated tensor.

      source
      theorem ESS.blowupLimitAssemblyPressure_rieszPressure_ae_zero {F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hzero : ∀ (i j : Fin 3), F i j =ᵐ[MeasureTheory.volume] 0) :
      CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressureLimit._proof_1 F hF =ᵐ[MeasureTheory.volume] 0

      The Riesz pressure of an almost-everywhere vanishing tensor vanishes almost everywhere.