Uniqueness of the local mild trajectory

The lifespan bound also controls any continuous mild trajectory with the same initial data. This supplies uniqueness without a radius hypothesis.

def CKN.Leray.regularizedMildPathRestrict {T : ℝ} (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (τ : ↑(RegularizedMildTimeInterval T)) : C(↑(RegularizedMildTimeInterval ↑τ), ↥RealVectorL2)

The restriction of a mild solution path to the shorter time interval ending at τ.

Equations

• CKN.Leray.regularizedMildPathRestrict u τ = { toFun := fun (s : ↑(CKN.Leray.RegularizedMildTimeInterval ↑τ)) => u ⟨↑s, ⋯⟩, continuous_toFun := ⋯ }

theorem CKN.Leray.regularizedMildTrajectory_norm_le_local (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (u : C(↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b)), ↥RealVectorL2)) (hu : IsRegularizedMildTrajectory ρ ε hε b (regularizedMildLocalLifespan ρ ε b) u) (t : ↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b))) : ‖u t‖ ≤ 2 * regularizedMildLocalM b

Every continuous solution of eq:reg-mild lies in the contraction ball throughout the lifespan of eq:reg-lifespan.

theorem CKN.Leray.regularizedMildTrajectory_unique_local (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (u v : C(↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b)), ↥RealVectorL2)) (hu : IsRegularizedMildTrajectory ρ ε hε b (regularizedMildLocalLifespan ρ ε b) u) (hv : IsRegularizedMildTrajectory ρ ε hε b (regularizedMildLocalLifespan ρ ε b) v) : u = v

The mild trajectory on the lifespan of eq:reg-lifespan is unique among all continuous spatial L² mild trajectories with the same initial data.