The regularized mild equation

The heat evolution and the time-integrated Leray-Stokes term in eq:reg-mild, with values in the real spatial L² carriers.

noncomputable def CKN.Leray.regularizedMildStokesIntegrand (F : ℝ → ↥RealTensorL2) (t s : ℝ) : ↥RealVectorL2

The Stokes integrand in the mild equation, set to zero at its integrable endpoint s = t.

Equations

• CKN.Leray.regularizedMildStokesIntegrand F t s = if hs : s < t then CKN.Leray.realStokesOperator ⋯ (F s) else 0

noncomputable def CKN.Leray.regularizedMildStokesIntegral (F : ℝ → ↥RealTensorL2) (t : ℝ) : ↥RealVectorL2

The Bochner integral in the mild equation, as an element of real spatial L².

Equations

• CKN.Leray.regularizedMildStokesIntegral F t = ∫ (s : ℝ) in Set.Icc 0 t, CKN.Leray.regularizedMildStokesIntegrand F t s

noncomputable def CKN.Leray.regularizedMildRightHandSide (b : ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (t : ℝ) (ht : 0 ≤ t) : ↥RealVectorL2

The right hand side of eq:reg-mild for a given initial field and tensor trajectory.

Equations

• CKN.Leray.regularizedMildRightHandSide b F t ht = CKN.Leray.realHeatOperator t ht b - CKN.Leray.regularizedMildStokesIntegral F t

def CKN.Leray.SatisfiesRegularizedMildEquation (b : ↥RealVectorL2) (u : ℝ → ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) : Prop

A velocity and tensor trajectory satisfy the real L² mild equation eq:reg-mild.

Equations

• CKN.Leray.SatisfiesRegularizedMildEquation b u F = ∀ (t : ℝ) (ht : 0 ≤ t), u t = CKN.Leray.regularizedMildRightHandSide b F t ht