The nonlinear regularized mild equation

The tensor in the Stokes integral is the regularized velocity tensor from eq:reg-mild.

noncomputable def CKN.Leray.regularizedMildTensorTrajectory (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : ℝ → ↥RealVectorL2) : ℝ → ↥RealTensorL2

The tensor trajectory generated by a velocity trajectory in eq:reg-mild.

Equations

• CKN.Leray.regularizedMildTensorTrajectory ρ ε hε u t = CKN.Leray.regularizedMildTensor ρ ε hε (u t)

def CKN.Leray.SatisfiesRegularizedMildVelocityEquation (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (u : ℝ → ↥RealVectorL2) : Prop

A trajectory solves the nonlinear regularized mild equation eq:reg-mild with initial datum b.

Equations

• CKN.Leray.SatisfiesRegularizedMildVelocityEquation ρ ε hε b u = CKN.Leray.SatisfiesRegularizedMildEquation b u (CKN.Leray.regularizedMildTensorTrajectory ρ ε hε u)