The canonical pressure of the global regularized curve

The pressure is the canonical mollification-limit pressure of the global regularized mild curve. On each finite interval, the regularized tensor has an H⁴ lift; applying the double-Riesz Fourier symbol to that lift supplies a continuous pressure representative and its first spatial derivatives.

theorem CKN.Leray.instFactLeENNRealOfNat_leanPool_1 : Fact (1 ≤ 2)

@[reducible, inline]

abbrev CKN.Leray.RegR12TensorH4 : Type

The tensor-valued Bessel-potential space of order four and exponent two used for the regularized pressure.

Equations

• CKN.Leray.RegR12TensorH4 = BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexTensor3 (↑(2 * 2)) 2

@[reducible, inline]

abbrev CKN.Leray.RegR12ScalarH4 : Type

The scalar Bessel-potential space of order four and exponent two used for the regularized pressure.

Equations

• CKN.Leray.RegR12ScalarH4 = BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 ℂ (↑(2 * 2)) 2

@[reducible, inline]

noncomputable abbrev CKN.Leray.RegR12ScalarL2 : AddSubgroup (Foundation.Parabolic.L2Vec3 →ₘ[MeasureTheory.volume] ℂ)

The scalar L² space used in the regularized pressure construction.

Equations

• CKN.Leray.RegR12ScalarL2 = MeasureTheory.Lp ℂ 2 MeasureTheory.volume

theorem CKN.Leray.regR12PressureApplyFormula_add (ξ : Foundation.Parabolic.L2Vec3) (F G : ComplexTensor3) : pressureApplyFormula ξ (F + G) = pressureApplyFormula ξ F + pressureApplyFormula ξ G

theorem CKN.Leray.regR12PressureApplyFormula_smul (ξ : Foundation.Parabolic.L2Vec3) (c : ℂ) (F : ComplexTensor3) : pressureApplyFormula ξ (c • F) = c • pressureApplyFormula ξ F

noncomputable def CKN.Leray.regR12PressureFourierCLM : ↥ComplexTensorL2 →L[ℂ] ↥RegR12ScalarL2

The double-Riesz Fourier symbol as a bounded linear map on frequency space tensor fields.

Equations

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

noncomputable def CKN.Leray.regR12PressureBesselMap : RegR12TensorH4 →L[ℂ] RegR12ScalarH4

The H⁴ pressure map obtained by applying the double-Riesz symbol to the weighted Fourier transform of an H⁴ tensor.

Equations

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

noncomputable def CKN.Leray.regR12PressurePath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) : ℝ → RegR12ScalarH4

The H⁴ pressure path associated with the global H⁴ velocity path.

Equations

• CKN.Leray.regR12PressurePath ρ ε hε T hT v s = CKN.Leray.regR12PressureBesselMap (CKN.Leray.regularisedBesselClampedTensorPath ρ ε hε 2 T hT v s)

noncomputable def CKN.Leray.regR12PressureFreqPath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) : ℝ → ↥RegR12ScalarL2

The frequency-space pressure path produced by the regularized R¹² construction.

Equations

• CKN.Leray.regR12PressureFreqPath ρ ε hε T hT v t = (MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 ℂ) (CKN.Leray.regR12PressurePath ρ ε hε T hT v t).toLp

noncomputable def CKN.Leray.regR12PressureModel (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) : Foundation.Parabolic.ParabolicPoint → ℝ

The continuous Fourier realization of the canonical pressure on [0,T]. The canonical pressure itself is identified with this field below.

Equations

• CKN.Leray.regR12PressureModel ρ ε hε T hT v = CKN.Leray.regR12SpaceTimeField Complex.reCLM (fun (x : CKN.Foundation.Parabolic.L2Vec3) => 1) (CKN.Leray.regR12PressureFreqPath ρ ε hε T hT v)

noncomputable def CKN.Leray.regR12PressureRealCurvePath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (T : ℝ) : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)

The real-space continuous pressure curve obtained from the frequency-space path.

Equations

• CKN.Leray.regR12PressureRealCurvePath ρ ε hε a ha T = { toFun := fun (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)) => CKN.Leray.regR12Curve ρ ε hε a ha ↑t, continuous_toFun := ⋯ }

noncomputable def CKN.Leray.regR12TensorBesselSymbol : Foundation.Parabolic.L2Vec3 × ComplexTensor3 → ComplexTensor3

The tensor Bessel-potential symbol used to construct the regularized pressure path.

Equations

• CKN.Leray.regR12TensorBesselSymbol p = ↑((1 + ‖p.1‖ ^ 2) ^ (-↑(2 * 2) / 2)) • p.2

theorem CKN.Leray.regR12Pressure_regularity (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (hPath : ∀ (T : ℝ), 0 ≤ T → ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12Pressure_regularity._proof_1) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t)) : have p := forcedQuadPressure ρ ε hε (regR12Curve ρ ε hε a ha); ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ), 0 < δ → δ < T → ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), |p z| ≤ C ∧ ∀ (i : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z| ≤ C) ∧ ∀ (δ T : ℝ), 0 < δ → δ < T → MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T))) ∧ ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))

The canonical pressure of the global regularized curve is continuously differentiable in space on positive times, with uniform strip bounds and square integrability on bounded positive-time slabs.