Continuity of the shifted complete Sobolev Stokes integral

The time translation fixes the Abel singularity at the left endpoint of the integration interval, giving a common integrable bound for every evaluation time.

theorem CKN.Leray.shiftedBesselMeasure : MeasureTheory.IsSeparable MeasureTheory.volume

theorem CKN.Leray.shiftedBesselComplexVecSeparable : TopologicalSpace.SeparableSpace ComplexVec3

theorem CKN.Leray.shiftedBesselTwoFinite : Fact (2 ≠ ⊤)

theorem CKN.Leray.shiftedBesselVectorSeparable (k : ℕ) : TopologicalSpace.SeparableSpace (BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)

theorem CKN.Leray.shiftedBesselVectorSecondCountable (k : ℕ) : SecondCountableTopology (BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)

@[instance_reducible]

noncomputable def CKN.Leray.shiftedBesselVectorMeasurableSpace (k : ℕ) : MeasurableSpace (BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)

The Borel measurable structure on the vector Bessel-potential space used by the shifted Stokes integral.

Equations

• CKN.Leray.shiftedBesselVectorMeasurableSpace k = borel (BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * k)) 2)

theorem CKN.Leray.shiftedBesselVectorBorelSpace (k : ℕ) : BorelSpace (BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)

noncomputable def CKN.Leray.regularisedBesselShiftedStokesIntegrand (k : ℕ) (F : ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (t τ : ℝ) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2

The translated complete Sobolev Stokes integrand, set to zero outside the interval where its elapsed-time parameter is positive.

Equations

• CKN.Leray.regularisedBesselShiftedStokesIntegrand k F t τ = if h : 0 < τ ∧ τ < t then (CKN.Leray.regularisedBesselStokesOperator ⋯ k) (F (t - τ)) else 0

theorem CKN.Leray.regularisedBesselShiftedStokesIntegral_continuous (k : ℕ) (F : ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (T : ℝ) (hT : 0 ≤ T) : Continuous fun (t : ℝ) => ∫ (τ : ℝ) in 0..T, regularisedBesselShiftedStokesIntegrand k F t τ

The fixed-upper-limit translated Stokes integral is continuous on the complete even-order Bessel potential space.