Integrability of the translated complete Sobolev Stokes term

The positive-time Stokes estimate controls the translated integrand by an integrable Abel kernel on every bounded interval.

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

theorem CKN.Leray.shiftedIntegrabilityComplexSeparable : TopologicalSpace.SeparableSpace ComplexVec3

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

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

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

@[instance_reducible]

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

The Borel measurable structure on the shifted vector Bessel-potential space.

Equations

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

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

theorem CKN.Leray.regularisedBesselShiftedStokesIntegrand_intervalIntegrable (k : ℕ) (F : ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (T t : ℝ) (hT : 0 ≤ T) : IntervalIntegrable (regularisedBesselShiftedStokesIntegrand k F t) MeasureTheory.volume 0 T

The translated complete Sobolev Stokes integrand is integrable on every bounded time interval under a uniform tensor bound.