Associated-pressure momentum integrand

Product-coordinate momentum expressions and their algebraic estimates.

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

The compact Helmholtz test obtained by cutting off both potentials in the decomposition used for thm:assoc-pressure.

Equations

• One or more equations did not get rendered due to their size.

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

Each cutoff Helmholtz test remains in the original compact test class.

noncomputable def CKN.Leray.associatedPressureMomentumProductIntegrand (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.Vec3 × ℝ → ℝ) (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The full velocity--gradient--pressure momentum integrand in product coordinates, used by thm:assoc-pressure.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.associatedPressureAbs_sub_le (a b : ℝ) : |a - b| ≤ |a| + |b|

The absolute value of a difference is bounded by the sum of the absolute values.

def CKN.Leray.associatedPressureMomentumProfileMajorant (C : ℝ) (S : Foundation.Parabolic.Vec3 × ℝ → ℝ) (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.Vec3 × ℝ → ℝ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The common integrable majorant used to remove the spatial cutoffs in thm:assoc-pressure.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.associatedPressureMomentumProductIntegrand_abs_le_profileMajorant {C : ℝ} {S : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} {Φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hTime : ∀ (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3), |timePartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => Φ q i) z| ≤ C * S z) (hSpace : ∀ (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3), |spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => Φ q i) j z| ≤ C * S z) (z : Foundation.Parabolic.Vec3 × ℝ) : |associatedPressureMomentumProductIntegrand u Du p Φ z| ≤ associatedPressureMomentumProfileMajorant C S u Du p z

A derivative profile bound controls the complete momentum integrand in thm:assoc-pressure.

theorem CKN.Leray.associatedPressureTimePartialProd_add {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => f q + g q) z = timePartialProd f z + timePartialProd g z

The product-coordinate time derivative distributes over addition of smooth functions.

theorem CKN.Leray.associatedPressureSpatialPartialProd_add {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => f q + g q) i z = spatialPartialProd f i z + spatialPartialProd g i z

The product-coordinate spatial derivative distributes over addition of smooth functions.

theorem CKN.Leray.associatedPressureMomentumProductIntegrand_add {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} {φ ψ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hψ : ContDiff ℝ (↑⊤) ψ) (z : Foundation.Parabolic.Vec3 × ℝ) : associatedPressureMomentumProductIntegrand u Du p (fun (q : Foundation.Parabolic.Vec3 × ℝ) => φ q + ψ q) z = associatedPressureMomentumProductIntegrand u Du p φ z + associatedPressureMomentumProductIntegrand u Du p ψ z

The product-coordinate momentum functional is linear in its test field, as used in thm:assoc-pressure.

theorem CKN.Leray.associatedPressureMomentumProductIntegrand_pressureless_curl {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} {A : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hA : ContDiff ℝ (↑⊤) A) (z : Foundation.Parabolic.Vec3 × ℝ) : associatedPressureMomentumProductIntegrand u Du p (associatedPressureTestCurl A) z = -∑ i : Fin 3, u z i * timePartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl A q i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl A q i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl A q i) j z

The pressure contribution vanishes on a curl test in thm:assoc-pressure.