Uniform-time linear complete Sobolev fixed point

A prescribed bounded physical L² velocity gives a unique complete Sobolev solution of its linearized mild equation on a time interval independent of the initial complete Sobolev norm.

theorem CKN.Leray.regularisedBesselLinearLocalFixedPoint (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (B : ℝ) (hB : 0 ≤ B) (g : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), ↥ComplexVectorL2)) (hg : ∀ (q : ↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B))), ‖g q‖ ≤ B) : ∃ (v : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), regularisedBesselLinearLocalMap ρ ε hε k b (regularisedBesselUniformEnergyStep ρ ε hε k B) ⋯ g B hB hg v = v

The linearized complete H²ᵏ mild map has a fixed point on the uniform energy time step, without a complete Sobolev norm ball.

theorem CKN.Leray.regularisedBesselLinearLocalFixedPoint_unique (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (B : ℝ) (hB : 0 ≤ B) (g : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), ↥ComplexVectorL2)) (hg : ∀ (q : ↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B))), ‖g q‖ ≤ B) (v w : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (hv : regularisedBesselLinearLocalMap ρ ε hε k b (regularisedBesselUniformEnergyStep ρ ε hε k B) ⋯ g B hB hg v = v) (hw : regularisedBesselLinearLocalMap ρ ε hε k b (regularisedBesselUniformEnergyStep ρ ε hε k B) ⋯ g B hB hg w = w) : v = w

The linearized complete Sobolev mild equation has at most one continuous solution on the uniform energy time step.