The contraction on the local mild trajectory ball

The fixed-interval mild map is a self-map and a strict contraction on the closed divergence-free ball in lem:reg-local-mild.

noncomputable def CKN.Leray.regularizedMildLocalM (b : ↥RealVectorL2) : ℝ

The local mild radius parameter M from eq:reg-lifespan.

Equations

• CKN.Leray.regularizedMildLocalM b = 1 + ‖b‖

theorem CKN.Leray.regularizedMildBallAbelBalance (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) : 2 * (regularizedMildMollifierConstant ρ ε * (2 * regularizedMildLocalM b) ^ 2 / √(2 * Real.exp 1)) * √(regularizedMildLocalLifespan ρ ε b) = regularizedMildLocalM b / 2

The Abel estimate at the lifespan in eq:reg-lifespan maps a radius 2M tensor bound to an integral bound of M/2.

theorem CKN.Leray.regularizedMildLocalMap_sub_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (u v : C(↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b)), ↥RealVectorL2)) (hu : ∀ (t : ↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b))), ‖u t‖ ≤ 2 * regularizedMildLocalM b) (hv : ∀ (t : ↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b))), ‖v t‖ ≤ 2 * regularizedMildLocalM b) : ‖regularizedMildLocalMap ρ ε hε b (regularizedMildLocalLifespan ρ ε b) ⋯ u - regularizedMildLocalMap ρ ε hε b (regularizedMildLocalLifespan ρ ε b) ⋯ v‖ ≤ 1 / 2 * ‖u - v‖

The local mild map has contraction factor one half on the closed ball of radius 2(1+‖b‖).

def CKN.Leray.regularizedMildLocalBall (T M : ℝ) : Set C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)

The set of continuous mild paths whose values satisfy the J condition and the uniform 2M norm bound.

Equations

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

theorem CKN.Leray.regularizedMildLocalFixedPoint (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) : ∃ (u : C(↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b)), ↥RealVectorL2)), IsRegularizedMildTrajectory ρ ε hε b (regularizedMildLocalLifespan ρ ε b) u ∧ ∀ (t : ↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b))), RegularizedMildJData (u t) ∧ ‖u t‖ ≤ 2 * regularizedMildLocalM b

A fixed point of the local mild map gives the local solution and remains in the closed divergence-free ball.