Bounds for the forced mild equation in frequency variables

Pointwise bounds for the Duhamel integrands of eq:reg-mild-forced, the Abel kernel integral, and the resulting bound on the frequency form of the right hand side, uniform on bounded time intervals.

theorem CKN.Leray.integral_norm_sq_eq_norm_sq_Lp {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : ↥(MeasureTheory.Lp E 2 μ)) : ∫ (x : α), ‖↑↑f x‖ ^ 2 ∂μ = ‖f‖ ^ 2

The squared L² norm is the integral of the squared pointwise norm.

theorem CKN.Leray.ae_leraySymbol_fourier_of_mildJData (b : ↥RealVectorL2) (hb : RegularizedMildJData b) : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), (leraySymbol ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 b)) ξ) = ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 b)) ξ

A datum in J has transform fixed by the Leray symbol almost everywhere.

theorem CKN.Leray.integral_abelKernel (s : ℝ) (hs : 0 ≤ s) : ∫ (r : ℝ) in Set.Ioc 0 s, (s - r) ^ (-(1 / 2)) = 2 * √s

The integral of the Abel kernel (s - r)^{-1/2} over (0, s].

theorem CKN.Leray.norm_forcedFourierStokesIntegrand_le {F : ℝ → ↥ComplexTensorL2} {t s C : ℝ} (hs : s ≤ t) (hFC : ‖F s‖ ≤ C) : ‖forcedFourierStokesIntegrand F t s‖ ≤ C / √(2 * Real.exp 1) * (t - s) ^ (-(1 / 2))

The pointwise bound for the frequency Stokes integrand.

theorem CKN.Leray.norm_forcedFourierForceIntegrand_le (H : ℝ → ↥ComplexVectorL2) (t s : ℝ) : ‖forcedFourierForceIntegrand H t s‖ ≤ ‖H s‖

The pointwise bound for the frequency force integrand.

theorem CKN.Leray.norm_forcedFourierMild_le (b : ↥ComplexVectorL2) {F : ℝ → ↥ComplexTensorL2} {H : ℝ → ↥ComplexVectorL2} {t T C : ℝ} (ht : 0 ≤ t) (htT : t ≤ T) (hFC : ∀ s ∈ Set.Ioc 0 T, ‖F s‖ ≤ C) (hH : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖H s‖) (Set.Ioc 0 T) MeasureTheory.volume) (hC : 0 ≤ C) : ‖forcedFourierMild b F H t ht‖ ≤ ‖b‖ + 2 * (C / √(2 * Real.exp 1)) * √T + ∫ (s : ℝ) in Set.Ioc 0 T, ‖H s‖

The frequency form of the right-hand side of eq:reg-mild-forced is bounded on [0, T] uniformly in time.