Continuity and integrability of the mild Stokes term

The Abel singularity is kept at a fixed elapsed-time endpoint by translating the time variable in the Stokes integral.

@[instance_reducible]

noncomputable def CKN.Leray.instMeasurableSpaceSubtypeAEEqFunL2Vec3VolumeMemAddSubgroupRealVectorL2 : MeasurableSpace ↥RealVectorL2

The Borel measurable structure used for the real vector-valued L² space.

Equations

• CKN.Leray.instMeasurableSpaceSubtypeAEEqFunL2Vec3VolumeMemAddSubgroupRealVectorL2 = borel ↥CKN.Leray.RealVectorL2

theorem CKN.Leray.instBorelSpaceSubtypeAEEqFunL2Vec3VolumeMemAddSubgroupRealVectorL2 : BorelSpace ↥RealVectorL2

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

theorem CKN.Leray.instSeparableSpaceL2Vec3 : TopologicalSpace.SeparableSpace Foundation.Parabolic.L2Vec3

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

theorem CKN.Leray.instSecondCountableTopologySubtypeAEEqFunL2Vec3VolumeMemAddSubgroupRealVectorL2 : SecondCountableTopology ↥RealVectorL2

noncomputable def CKN.Leray.mildShiftedStokesIntegrand (F : ℝ → ↥RealTensorL2) (t τ : ℝ) : ↥RealVectorL2

The translated Stokes integrand, extended by zero outside 0 < τ < t.

Equations

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

theorem CKN.Leray.mildShiftedStokesIntegral_continuousAt (F : ℝ → ↥RealTensorL2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (t : ℝ), ‖F t‖ ≤ C) (hC : 0 ≤ C) (T : ℝ) (hT : 0 ≤ T) {t₀ : ℝ} : ContinuousAt (fun (t : ℝ) => ∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand F t τ) t₀

The fixed-upper-limit translated Stokes integral is continuous in its evaluation time.

theorem CKN.Leray.mildShiftedStokesIntegral_continuous (F : ℝ → ↥RealTensorL2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (t : ℝ), ‖F t‖ ≤ C) (hC : 0 ≤ C) (T : ℝ) (hT : 0 ≤ T) : Continuous fun (t : ℝ) => ∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand F t τ

The fixed-upper-limit translated Stokes integral is a continuous trajectory.

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

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

theorem CKN.Leray.regularizedMildStokesIntegral_eq_shifted {F : ℝ → ↥RealTensorL2} (T t : ℝ) (hT : 0 ≤ T) (ht : 0 ≤ t) (htT : t ≤ T) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) : regularizedMildStokesIntegral F t = ∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand F t τ

Translation of the time variable turns the singularity into a fixed integrable Abel kernel.