Local solutions of the regularized mild equation

The solution is constructed as a continuous trajectory on the closed lifespan interval in lem:reg-local-mild.

@[reducible, inline]

abbrev CKN.Leray.RegularizedMildTimeInterval (T : ℝ) : Set ℝ

The compact time interval for a local mild trajectory.

Equations

• CKN.Leray.RegularizedMildTimeInterval T = Set.Icc 0 T

def CKN.Leray.IsRegularizedMildTrajectory (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (T : ℝ) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : Prop

A continuous trajectory satisfies the regularized mild equation on its time interval.

Equations

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

theorem CKN.Leray.regularizedMildTrajectory_norm_le_iff (T : ℝ) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (R : ℝ) (hR : 0 ≤ R) : ‖u‖ ≤ R ↔ ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R

The continuous time space on the closed interval has the supremum norm used in the contraction argument.