Helmholtz cutoff derivative bounds

Common spatial profiles bound derivatives of the compact Helmholtz tests.

noncomputable def CKN.Leray.associatedPressurePotentialDirectionCutoffCoefficient {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hdecay : RieszPressurePotentialDecay ψ) : ℝ

Decay coefficient for the potential gradient after multiplying by a spatial cutoff.

Equations

• CKN.Leray.associatedPressurePotentialDirectionCutoffCoefficient hdecay = Classical.choose ⋯ + CKN.cutoffGradientConstant * Classical.choose ⋯

noncomputable def CKN.Leray.associatedPressurePotentialHessianCutoffCoefficient {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hdecay : RieszPressurePotentialDecay ψ) : ℝ

Decay coefficient for the potential Hessian after multiplying by a spatial cutoff.

Equations

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

theorem CKN.Leray.associatedPressureHelmholtzTestCutoff_derivative_profile_bounds {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ∃ (K : Set ℝ), IsCompact K ∧ K ⊆ Set.Ioo 0 T ∧ ∃ C ≥ 0, ∀ (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3), |timePartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureHelmholtzTestCutoff φ n q i) z| ≤ C * associatedPressureSpatialProfile K 2 z ∧ |spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureHelmholtzTestCutoff φ n q i) j z| ≤ C * associatedPressureSpatialProfile K 2 z

The Helmholtz cutoffs and both Helmholtz components have common spatial derivative profiles for thm:assoc-pressure.