Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.ForcePressureOperator

Linearity of the force pressure #

The field (I - ℙ) f of lem:force-pressure is the orthogonal projection of f onto the closure of the test gradients: it lies in that closure, and the Leray part ℙ f is orthogonal to every test gradient. Hence it is linear in f, and by uniqueness the L⁶ pressure of one slice is linear up to null sets.

source
theorem CKN.Leray.inner_eq_integral_realVectorL2Representative (u w : ↥RealVectorL2) :
inner ℝ u w = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, realVectorL2Representative u x i * realVectorL2Representative w x i

The real pairing of two spatial L² fields is the integral of the dot product of their coordinate representatives.

source
theorem CKN.Leray.realLerayProjection_mem_orthogonal_testGradientSpan (v : ↥RealVectorL2) :
realLerayProjection v ∈ forcePressureTestGradientSpanᗮ

The Leray part of a field is orthogonal to every test gradient.

source
theorem CKN.Leray.forcePressureGradientL2_eq_starProjection (v : ↥RealVectorL2) :
forcePressureGradientL2 v = forcePressureTestGradientSpan.topologicalClosure.starProjection v

The field (I - ℙ) f of lem:force-pressure is the orthogonal projection of f onto the closure of the test gradients.

source
theorem CKN.Leray.forcePressureGradientL2_add (v w : ↥RealVectorL2) :
forcePressureGradientL2 (v + w) = forcePressureGradientL2 v + forcePressureGradientL2 w

The field (I - ℙ) f is additive in f.

source
theorem CKN.Leray.forcePressureGradientL2_smul (c : ℝ) (v : ↥RealVectorL2) :
forcePressureGradientL2 (c • v) = c • forcePressureGradientL2 v

The field (I - ℙ) f is homogeneous in f.

source
noncomputable def CKN.Leray.forcePressureSlice (v : ↥RealVectorL2) :
Foundation.Parabolic.Vec3 → ℝ

The force pressure of lem:force-pressure on one time slice: an L⁶ function whose weak gradient is the field (I - ℙ) f.

Equations
Instances For
    source
    theorem CKN.Leray.forcePressureSlice_memLp (v : ↥RealVectorL2) :
    MeasureTheory.MemLp (forcePressureSlice v) 6 MeasureTheory.volume

    The slice force pressure lies in L⁶.

    source
    theorem CKN.Leray.forcePressureSlice_eLpNorm_le (v : ↥RealVectorL2) :
    MeasureTheory.eLpNorm (forcePressureSlice v) 6 MeasureTheory.volume ≤ gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm (↑↑(forcePressureGradientL2 v)) 2 MeasureTheory.volume

    The homogeneous Sobolev bound for the slice force pressure.

    source
    theorem CKN.Leray.forcePressureSlice_hasWeakGradientOn (v : ↥RealVectorL2) :
    HasWeakGradientOn Set.univ (forcePressureSlice v) (realVectorL2Representative (forcePressureGradientL2 v))

    The weak gradient of the slice force pressure is (I - ℙ) f.

    source
    theorem CKN.Leray.hasWeakGradientOn_congr_ae_left {p q : Foundation.Parabolic.Vec3 → ℝ} {G : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hpq : p =ᵐ[MeasureTheory.volume] q) (h : HasWeakGradientOn Set.univ p G) :
    HasWeakGradientOn Set.univ q G

    A weak gradient is unchanged when the function is modified on a null set.

    source
    theorem CKN.Leray.hasWeakGradientOn_congr_ae_right {p : Foundation.Parabolic.Vec3 → ℝ} {G H : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hGH : G =ᵐ[MeasureTheory.volume] H) (h : HasWeakGradientOn Set.univ p G) :
    HasWeakGradientOn Set.univ p H

    A weak gradient may be modified on a null set.

    source
    theorem CKN.Leray.forcePressureSlice_linearCombination_ae (a b : ℝ) (v w : ↥RealVectorL2) :
    forcePressureSlice (a • v + b • w) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => a * forcePressureSlice v x + b * forcePressureSlice w x

    The slice force pressure is linear up to null sets.