Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.AssocPressureTestCutoff

Assoc Pressure Test Cutoff #

Supporting estimates for the Navier–Stokes development.

source
noncomputable def CKN.Leray.associatedPressureHelmholtzScalarPotentialCutoff (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (n : ℕ) :
Foundation.Parabolic.Vec3 × ℝ → ℝ

The spatial cutoff of the scalar Newtonian potential in the Helmholtz decomposition of a compact vector test.

Equations
Instances For
    source
    theorem CKN.Leray.associatedPressureHelmholtzScalarPotentialCutoff_mem_spaceTimeTestFunction {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) :
    associatedPressureHelmholtzScalarPotentialCutoff φ n ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)

    The cutoff scalar potential is a compactly supported space-time test, with support inside the original test interval.

    source
    theorem CKN.Leray.associatedPressureHelmholtzScalarPotentialCutoffGradient_mem_spaceTimeTestFunction {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) :
    associatedPressureTestGradient (associatedPressureHelmholtzScalarPotentialCutoff φ n) ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)

    The gradient of the cutoff scalar potential is a compact vector test in the same time slab.

    source
    theorem CKN.Leray.associatedPressureCutoffTimePartial_eq {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (n : ℕ) :
    timePartialProd (rieszPressurePotentialCutoffTest ψ n) = rieszPressurePotentialCutoffTest (timePartialProd ψ) n

    Time differentiation commutes with a spatial cutoff of a smooth scalar potential.

    source
    theorem CKN.Leray.associatedPressureHelmholtzScalarPotentialCutoff_spatial_eventually_eq {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
    ∀ᶠ (n : ℕ) in Filter.atTop, spatialSecondPartialProd (associatedPressureHelmholtzScalarPotentialCutoff φ n) i j z = spatialSecondPartialProd (associatedPressureHelmholtzScalarPotential φ) i j z

    Spatial Hessians of the cutoff scalar potential eventually agree at each fixed space-time point with the uncut Hessian.

    source
    theorem CKN.Leray.associatedPressureHelmholtzScalarPotentialCutoff_timeSpatial_eventually_eq {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
    ∀ᶠ (n : ℕ) in Filter.atTop, timePartialProd (spatialPartialProd (associatedPressureHelmholtzScalarPotentialCutoff φ n) i) z = timePartialProd (spatialPartialProd (associatedPressureHelmholtzScalarPotential φ) i) z

    Time derivatives of the cutoff scalar gradient eventually agree at each fixed point with the uncut scalar gradient time derivative.

    source
    theorem CKN.Leray.associatedPressureHelmholtzScalarPotentialCutoffGradient_momentum_zero {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) :
    ∫ (z : Foundation.Parabolic.Vec3 × ℝ), -∑ i : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * timePartialProd (spatialPartialProd (associatedPressureHelmholtzScalarPotentialCutoff φ n) i) z - ∑ i : Fin 3, ∑ j : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * u (Foundation.Parabolic.parabolicHomeomorph.symm z) j * spatialSecondPartialProd (associatedPressureHelmholtzScalarPotentialCutoff φ n) i j z + ∑ i : Fin 3, ∑ j : Fin 3, Du (Foundation.Parabolic.parabolicHomeomorph.symm z) i j * spatialSecondPartialProd (associatedPressureHelmholtzScalarPotentialCutoff φ n) i j z - rieszPressureSpaceTime (5 / 3) associatedPressureHelmholtzScalarPotentialCutoffGradient_momentum_zero._proof_1 (associatedPressureTensor T u) ⋯ z * rieszPressureJointLaplacian (associatedPressureHelmholtzScalarPotentialCutoff φ n) z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

    The complete momentum functional vanishes on the compactly supported gradient cutoff used in the Helmholtz decomposition.