Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.WeakContL3

Weak continuity of the local velocity #

The momentum identity gives a weakly continuous representative of the velocity in L^3 through the terminal time, as in lem:weak-cont-L3.

source
theorem instFactLeENNRealOfNat_leanPool_2 :
Fact (1 ≤ 2)
source
instance ESS.weakContL3SpatialBall_isFiniteMeasure_local :
MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall)
source
noncomputable def ESS.weakContL3MomentSup {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} :
ENNReal

The essential upper bound for the local cubic velocity moment.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def ESS.weakContL3MomentBound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} :
    ENNReal

    The local L³ bound obtained from the essential cubic moment.

    Equations
    Instances For
      source
      theorem ESS.weakContL3_l2Representative {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 → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet CKN.weakContL3SpatialBall (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet CKN.weakContL3SpatialBall (Set.Ioo (-1) 0)))) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet CKN.weakContL3SpatialBall (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hL3 : weakContL3MomentSup < ⊤) (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet CKN.weakContL3SpatialBall (Set.Ioo (-1) 0)))) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn CKN.weakContL3SpatialBall (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) (hS3 : ∀ Φ ∈ CKN.spaceTimeTestFunction CKN.weakContL3SpatialBall (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet CKN.weakContL3SpatialBall (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Φ y i) i z = 0) :
      ∃ (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall))), (∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), ‖v t‖ ≤ (weakContL3MomentBound * (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall) Set.univ ^ (1 / 6)).toReal) ∧ (∀ (w : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall))), Continuous fun (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) => inner ℝ (v t) w) ∧ (∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) (w : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall))), |inner ℝ (v t) w| ≤ weakContL3MomentBound.toReal * ‖(weakContL3L2ToLThreeHalves (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall)) w‖) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0) (hm : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Classical.choose CKN.weakContL3_cutoff_exists x • WithLp.toLp 2 (u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm (x, t)))) 2 (MeasureTheory.volume.restrict CKN.weakContL3SpatialBall)), v ⟨t, ht⟩ = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Classical.choose CKN.weakContL3_cutoff_exists x • WithLp.toLp 2 (u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm (x, t)))) hm) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), t ∈ Set.Icc (-(3 / 4) ^ 2) 0 ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))) ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))) ≤ weakContL3MomentBound

      An all-time weakly continuous local L² representative with a scale-aware L² bound and the L³-controlled pairing estimate.