Potential decay foundations

Newtonian-potential identities and component formulas for the Helmholtz potentials.

theorem CKN.Leray.associatedPressureFirstSpatialDerivative_le_iteratedFDeriv {f : Foundation.Parabolic.Vec3 → ℝ} (i : Fin 3) (x : Foundation.Parabolic.Vec3) : |spatialDeriv f i x| ≤ ‖iteratedFDeriv ℝ 1 f x‖

A first spatial derivative is bounded by the first iterated derivative.

theorem CKN.Leray.associatedPressureSecondSpatialDerivative_le_iteratedFDeriv {f : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : |spatialDeriv (spatialDeriv f j) i x| ≤ ‖iteratedFDeriv ℝ 2 f x‖

A second spatial derivative is bounded by the second iterated derivative.

theorem CKN.Leray.associatedPressureThirdSpatialDerivative_le_iteratedFDeriv {f : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j k : Fin 3) (x : Foundation.Parabolic.Vec3) : |spatialDeriv (spatialDeriv (spatialDeriv f k) j) i x| ≤ ‖iteratedFDeriv ℝ 3 f x‖

A third spatial derivative is bounded by the third iterated derivative.

theorem CKN.Leray.associatedPressureHelmholtzPotentials_zero_off_time_support {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {t : ℝ} (ht : t ∉ Prod.snd '' tsupport φ) (x : Foundation.Parabolic.Vec3) : associatedPressureHelmholtzScalarPotential φ (x, t) = 0 ∧ associatedPressureHelmholtzVectorPotential φ (x, t) = 0

The Newtonian Helmholtz potentials vanish on every time slice outside the compact time support of the test field.

theorem CKN.Leray.associatedPressureHelmholtzPotentials_compactTimeSupport {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ∃ (K : Set ℝ), IsCompact K ∧ ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), associatedPressureHelmholtzScalarPotential φ (x, t) = 0 ∧ associatedPressureHelmholtzVectorPotential φ (x, t) = 0

Both Helmholtz potentials have the compact time support required in lem:riesz-duality and in the solenoidal cutoff argument.

theorem CKN.Leray.associatedPressurePotentialSource_slice_integral_bound {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ∃ C ≥ 0, ∀ (t : ℝ), ∫ (x : Foundation.Parabolic.Vec3), |g (x, t)| ≤ C

A compact smooth source has a finite absolute integral on each time slice.

theorem CKN.Leray.associatedPressureNewtonianPotential_neg {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (z : Foundation.Parabolic.Vec3 × ℝ) : associatedPressureNewtonianPotential (fun (q : Foundation.Parabolic.Vec3 × ℝ) => -g q) z = -associatedPressureNewtonianPotential g z

Negation commutes with the Newtonian potential in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureSpatialPartial_finset_sum (f : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hf : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (f i)) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, f j q) i z = ∑ j : Fin 3, spatialPartialProd (f j) i z

A spatial partial derivative distributes over a finite coordinate sum, used to express the scalar and vector Helmholtz potentials componentwise.

theorem CKN.Leray.associatedPressureHelmholtzScalarPotential_eq_sum_spatialPartial {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (z : Foundation.Parabolic.Vec3 × ℝ) : associatedPressureHelmholtzScalarPotential φ z = ∑ i : Fin 3, spatialPartialProd (associatedPressureNewtonianPotential fun (q : Foundation.Parabolic.Vec3 × ℝ) => φ q i) i z

The scalar Helmholtz potential is the sum of the differentiated Newtonian potentials.

theorem CKN.Leray.associatedPressureHelmholtzScalarPotential_direction_eq_sum {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : rieszPressureJointDirection (associatedPressureHelmholtzScalarPotential φ) i z = ∑ k : Fin 3, spatialPartialProd (spatialPartialProd (associatedPressureNewtonianPotential fun (q : Foundation.Parabolic.Vec3 × ℝ) => φ q k) k) i z

The scalar Helmholtz potential gradient is a sum of second derivatives.

theorem CKN.Leray.associatedPressureHelmholtzScalarPotential_hessian_eq_sum {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : rieszPressureJointHessian (associatedPressureHelmholtzScalarPotential φ) i j z = ∑ k : Fin 3, spatialPartialProd (spatialPartialProd (spatialPartialProd (associatedPressureNewtonianPotential fun (q : Foundation.Parabolic.Vec3 × ℝ) => φ q k) k) j) i z

The scalar Helmholtz potential Hessian is a sum of third derivatives.