Integrability of the translated complex physical Stokes term

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

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

theorem CKN.Leray.complexShiftedIntegrabilityComplexSeparable : TopologicalSpace.SeparableSpace ComplexVec3

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

theorem CKN.Leray.complexShiftedIntegrabilityVectorSeparable : TopologicalSpace.SeparableSpace ↥ComplexVectorL2

theorem CKN.Leray.complexShiftedIntegrabilityVectorSecondCountable : SecondCountableTopology ↥ComplexVectorL2

@[instance_reducible]

noncomputable def CKN.Leray.complexShiftedIntegrabilityVectorMeasurableSpace : MeasurableSpace ↥ComplexVectorL2

The Borel measurable structure on the complex shifted vector integrability space.

Equations

• CKN.Leray.complexShiftedIntegrabilityVectorMeasurableSpace = borel ↥CKN.Leray.ComplexVectorL2

theorem CKN.Leray.complexShiftedIntegrabilityVectorBorelSpace : BorelSpace ↥ComplexVectorL2

noncomputable def CKN.Leray.regularisedComplexShiftedStokesIntegrand (F : ℝ → ↥ComplexTensorL2) (t τ : ℝ) : ↥ComplexVectorL2

The complex physical Stokes kernel at elapsed time τ, truncated to the causal interval of the observation time t.

Equations

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

theorem CKN.Leray.regularisedComplexShiftedStokesIntegrand_intervalIntegrable (F : ℝ → ↥ComplexTensorL2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (T t : ℝ) (hT : 0 ≤ T) : IntervalIntegrable (regularisedComplexShiftedStokesIntegrand F t) MeasureTheory.volume 0 T

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