The forced regularized momentum identity #
eq:reg-momentum-forced: the forced regularized velocity, its weak gradient
and the pressure P[J_εu_ε ⊗ u_ε] + p_f satisfy the weak momentum identity
against every smooth compactly supported test on positive times. The space-time
integral is an integral over the time slices, each slice is a combination of
frequency pairings, and their time integral vanishes by the frequency weak form
of the forced mild equation.
theorem
CKN.Leray.exists_time_bound
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφc : HasCompactSupport φ)
(hφs : tsupport φ ⊆ spaceTimeSet Set.univ (Set.Ioi 0))
:
theorem
CKN.Leray.fderiv_eq_zero_of_notMem_tsupport'
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.Vec3 × ℝ}
(hz : z ∉ tsupport φ)
:
theorem
CKN.Leray.forcedMomentumIntegrand_eq_zero
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(hf : IsLocallySquareIntegrableForce f)
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.Vec3 × ℝ}
(hz : z ∉ tsupport φ)
:
theorem
CKN.Leray.integrable_lam_testHat_sq
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
(T : ℝ)
:
MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => (forcedFourierLam p.1 * ‖testHat φ p‖) ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))
theorem
CKN.Leray.integrable_six_sum
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{A1 A2 A3 A4 A5 A6 : α → ℝ}
(h1 : MeasureTheory.Integrable A1 μ)
(h2 : MeasureTheory.Integrable A2 μ)
(h3 : MeasureTheory.Integrable A3 μ)
(h4 : MeasureTheory.Integrable A4 μ)
(h5 : MeasureTheory.Integrable A5 μ)
(h6 : MeasureTheory.Integrable A6 μ)
:
theorem
CKN.Leray.integrable_forcedMomentumIntegrand
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
{T : ℝ}
(hT : 0 < T)
:
MeasureTheory.Integrable (forcedMomentumIntegrand ρ ε hε ha f hf φ)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))
theorem
CKN.Leray.forcedReg_weak_form
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
{T : ℝ}
(hT : 0 < T)
(hTs : ∀ z ∈ tsupport φ, z.2 ∈ Set.Ioo 0 T)
:
The frequency weak form of the forced regularized solution against the transforms of a test.
theorem
CKN.Leray.integral_forcedMomentumIntegrand_eq_zero
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
(hφs : tsupport φ ⊆ spaceTimeSet Set.univ (Set.Ioi 0))
:
∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), forcedMomentumIntegrand ρ ε hε ha f hf φ z = 0
The weak momentum identity of the forced regularized solution.
theorem
CKN.Leray.forcedRegPressure_apply
(ρ : RegMollifierProfile)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{ε : ℝ}
(hε : 0 < ε)
(z : Foundation.Parabolic.ParabolicPoint)
:
forcedRegPressure ρ a ha f hf ε z = forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) z + forcePressure f hf z
theorem
CKN.Leray.timePartial_eq_timeDeriv'
{φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => φ z)
(i : Fin 3)
(z : Foundation.Parabolic.ParabolicPoint)
:
theorem
CKN.Leray.spatialPartial_eq_spaceDeriv'
{φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => φ z)
(i j : Fin 3)
(z : Foundation.Parabolic.ParabolicPoint)
:
theorem
CKN.Leray.forcedRegMomentum
(ρ : RegMollifierProfile)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(hf : IsLocallySquareIntegrableForce f)
(ε : ℝ)
(hε : 0 < ε)
(φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0) →
∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3,
forcedRegVelocity ρ a ha f hf ε z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε) z j * forcedRegVelocity ρ a ha f hf ε z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
forcedRegGradient ρ a ha f hf ε z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - forcedRegPressure ρ a ha f hf ε z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, f z i * φ z i = 0
eq:reg-momentum-forced: the weak momentum identity of the forced
regularized solutions, in the form used by the limiting argument of
thm:leray-forced.