The momentum identity on one time slice #
On every time slice where the velocity has a square-integrable weak gradient
and the force and force pressure have their slice properties, the spatial
integral of the integrand of eq:reg-momentum-forced is the combination of
frequency pairings that the frequency weak form sets to zero after
integration in time.
noncomputable def
CKN.Leray.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)
(z : Foundation.Parabolic.Vec3 × ℝ)
:
The integrand of eq:reg-momentum-forced for the forced regularized
solution, with the space-time derivatives of the test.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Leray.integral_six_combo
{A1 A2 A3 A4 A5 A6 : Foundation.Parabolic.Vec3 → ℝ}
(h1 : MeasureTheory.Integrable A1 MeasureTheory.volume)
(h2 : MeasureTheory.Integrable A2 MeasureTheory.volume)
(h3 : MeasureTheory.Integrable A3 MeasureTheory.volume)
(h4 : MeasureTheory.Integrable A4 MeasureTheory.volume)
(h5 : MeasureTheory.Integrable A5 MeasureTheory.volume)
(h6 : MeasureTheory.Integrable A6 MeasureTheory.volume)
:
∫ (x : Foundation.Parabolic.Vec3), -A1 x - A2 x + A3 x - (A4 x + A5 x) - A6 x = (((-∫ (x : Foundation.Parabolic.Vec3), A1 x) - ∫ (x : Foundation.Parabolic.Vec3), A2 x) + ∫ (x : Foundation.Parabolic.Vec3), A3 x) - ((∫ (x : Foundation.Parabolic.Vec3), A4 x) + ∫ (x : Foundation.Parabolic.Vec3), A5 x) - ∫ (x : Foundation.Parabolic.Vec3), A6 x
theorem
CKN.Leray.forcedMomentumIntegrand_eq
(ρ : 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)
(x : Foundation.Parabolic.Vec3)
(t : ℝ)
:
forcedMomentumIntegrand ρ ε hε ha f hf φ (x, t) = -∑ i : Fin 3, forcedRegRep ρ ε hε ha hf (x, t) i * timeDeriv φ (x, t) i - ∑ i : Fin 3,
∑ j : Fin 3,
regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) (x, t) j * forcedRegRep ρ ε hε ha hf (x, t) i * spaceDeriv j φ (x, t) i + ∑ i : Fin 3, ∑ j : Fin 3, forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (x, t) i j * spaceDeriv j φ (x, t) i - (forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (x, t) * sliceDiv φ t x + forcePressure f hf (x, t) * sliceDiv φ t x) - ∑ i : Fin 3, f (x, t) i * φ (x, t) i
theorem
CKN.Leray.integral_forcedMomentumIntegrand_slice
(ρ : 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 : ℝ}
{Y : Foundation.Parabolic.L2Vec3 → ComplexVec3}
{Fh : Foundation.Parabolic.L2Vec3 → ComplexTensor3}
{Hh : Foundation.Parabolic.L2Vec3 → ComplexVec3}
(hZ :
∃ (Z : ↥ComplexVectorL2),
realPartVectorL2 Z = forcedRegCurve ρ ε hε ha hf t ∧ Y =ᵐ[MeasureTheory.volume] ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) Z))
(hFh :
Fh =ᵐ[MeasureTheory.volume]
↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3)
(complexifyTensorL2 (regularizedMildTensor ρ ε hε (forcedRegCurve ρ ε hε ha hf t)))))
(hHh :
Hh =ᵐ[MeasureTheory.volume]
↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3)
(complexifyVectorL2 (forcedForceSlice (forcedForceMod f hf) t))))
(hweak :
∀ (i : Fin 3),
HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcedRegRep ρ ε hε ha hf (x, t) i) fun (x : Vec 3) =>
forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (x, t) i)
(hDu :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) => forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (x, t) i j) 2
MeasureTheory.volume)
(hF2 : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => forcedForceMod f hf (x, t)) 2 MeasureTheory.volume)
(hFf :
(fun (x : Foundation.Parabolic.Vec3) => forcedForceMod f hf (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : Foundation.Parabolic.Vec3) => f (x, t))
(hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume)
(hpf :
HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcePressure f hf (x, t))
(forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft))
(hpfl :
MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t))
MeasureTheory.volume)
:
∫ (x : Foundation.Parabolic.Vec3), forcedMomentumIntegrand ρ ε hε ha f hf φ (x, t) = (((-∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Y ξ) (testHat (timeDeriv φ) (ξ, t))).re) + ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Y ξ) (↑(forcedFourierLam ξ) • testHat φ (ξ, t))).re) - ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) (Fh ξ)))
((leraySymbol ξ) (testHat φ (ξ, t)))).re) - ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Hh ξ) ((leraySymbol ξ) (testHat φ (ξ, t)))).re
The momentum integrand on one time slice in frequency variables.