The forced regularized solution on a bounded interval

The fixed point of the truncated map satisfies the energy balance of lem:regularised-forced without its transport term, since the transport pairing vanishes. With 2⟨u, f⟩ ≤ |u|² + |f|² and Grönwall this bounds the solution independently of the truncation radius, as in eq:reg-energy-forced-gronwall; for a large radius the truncation is inactive and the fixed point solves eq:reg-mild-forced.

theorem CKN.Leray.le_mul_exp_of_le_add_integral {φ : ℝ → ℝ} (hφ : Continuous φ) {A T : ℝ} (h : ∀ t ∈ Set.Icc 0 T, φ t ≤ A + ∫ (s : ℝ) in Set.Ioc 0 t, φ s) (t : ℝ) : t ∈ Set.Icc 0 T → φ t ≤ A * Real.exp t

Grönwall's inequality in integral form for a continuous function.

theorem CKN.Leray.regularizedMildStokesIntegral_congr_Icc {F G : ℝ → ↥RealTensorL2} {t : ℝ} (hFG : ∀ s ∈ Set.Icc 0 t, F s = G s) : regularizedMildStokesIntegral F t = regularizedMildStokesIntegral G t

The Stokes Duhamel integral at time t depends only on the tensor curve up to time t.

theorem CKN.Leray.forcedMildRHS_congr_Icc (b : ↥RealVectorL2) (h : ℝ → ↥RealVectorL2) {F G : ℝ → ↥RealTensorL2} {t : ℝ} (ht : 0 ≤ t) (hFG : ∀ s ∈ Set.Icc 0 t, F s = G s) : forcedMildRHS b h F t ht = forcedMildRHS b h G t ht

The right-hand side of eq:reg-mild-forced at time t depends only on the tensor curve up to time t.

theorem CKN.Leray.forcedFourierDissipation_nonneg (v : ↥ComplexVectorL2) : 0 ≤ forcedFourierDissipation v

theorem CKN.Leray.memLp_forcedFourierGradHat_of_integrable (v : ↥ComplexVectorL2) (hv : MeasureTheory.Integrable (fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierLam ξ * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) ξ‖ ^ 2) MeasureTheory.volume) : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume

Square integrability of the frequency gradient from integrability of the weighted square of the transform.

theorem CKN.Leray.forcedMildMap_eq_forcedMildCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 T) MeasureTheory.volume) {R : ℝ} (hR : 0 ≤ R) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hu : forcedMildMap ρ ε hε b hh hH hR T hT u = u) {s : ℝ} (hs : s ∈ RegularizedMildTimeInterval T) : forcedMildCurve b h (forcedTensorCurve ρ ε hε R T hT u) s = u ⟨s, hs⟩

The truncated forced mild map evaluated at an interior time is the forced mild curve of its tensor curve.

theorem CKN.Leray.forcedTruncSolution_energy (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH2 : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume) {R : ℝ} (hR : 0 ≤ R) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hu : forcedMildMap ρ ε hε b hh ⋯ hR T hT u = u) {τ : ℝ} (hτ : τ ∈ RegularizedMildTimeInterval T) : have v := forcedComplexCurve b (forcedTensorCurve ρ ε hε R T hT u) h; (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 τ), MeasureTheory.MemLp (forcedFourierGradHat (v s)) 2 MeasureTheory.volume) ∧ MeasureTheory.IntegrableOn (fun (s : ℝ) => forcedFourierDissipation (v s)) (Set.Ioc 0 τ) MeasureTheory.volume ∧ (∀ (s : ℝ) (hs : s ∈ RegularizedMildTimeInterval T), realPartVectorL2 (v s) = u ⟨s, hs⟩) ∧ ‖u ⟨τ, hτ⟩‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 τ, forcedFourierDissipation (v s) ≤ ‖b‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 τ, inner ℝ (u (regularizedMildTimeClamp T hT s)) (h s)

The energy inequality of the truncated forced solution: the transport pairing drops out of the energy balance.

theorem CKN.Leray.forcedTruncSolution_norm_sq_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH2 : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume) {R : ℝ} (hR : 0 ≤ R) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hu : forcedMildMap ρ ε hε b hh ⋯ hR T hT u = u) (t : ↑(RegularizedMildTimeInterval T)) : ‖u t‖ ^ 2 ≤ (‖b‖ ^ 2 + ∫ (s : ℝ) in Set.Ioc 0 T, ‖h s‖ ^ 2) * Real.exp ↑t

The Grönwall bound for the truncated forced solution, independent of the truncation radius.

theorem CKN.Leray.forcedTensorCurve_eq_clamped (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hbound : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R) : forcedTensorCurve ρ ε hε R T hT u = regularizedMildClampedTensorTrajectory ρ ε hε T hT u

theorem CKN.Leray.forcedMildMap_eq_self_of_solution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 T) MeasureTheory.volume) {R : ℝ} (hR : 0 ≤ R) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), u t = forcedMildRHS b h (regularizedMildClampedTensorTrajectory ρ ε hε T hT u) ↑t ⋯) (hbound : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R) : forcedMildMap ρ ε hε b hh hH hR T hT u = u

theorem CKN.Leray.exists_forcedMildSolution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH2 : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume) (T : ℝ) (hT : 0 ≤ T) : ∃ (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)), (∀ (t : ↑(RegularizedMildTimeInterval T)), u t = forcedMildRHS b h (regularizedMildClampedTensorTrajectory ρ ε hε T hT u) ↑t ⋯) ∧ ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ^ 2 ≤ (‖b‖ ^ 2 + ∫ (s : ℝ) in Set.Ioc 0 T, ‖h s‖ ^ 2) * Real.exp T

Existence of a continuous L² solution of eq:reg-mild-forced on [0, T] obeying the Grönwall bound eq:reg-energy-forced-gronwall.

theorem CKN.Leray.forcedMildSolution_unique (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 T) MeasureTheory.volume) (T : ℝ) (hT : 0 ≤ T) (u u' : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), u t = forcedMildRHS b h (regularizedMildClampedTensorTrajectory ρ ε hε T hT u) ↑t ⋯) (hu' : ∀ (t : ↑(RegularizedMildTimeInterval T)), u' t = forcedMildRHS b h (regularizedMildClampedTensorTrajectory ρ ε hε T hT u') ↑t ⋯) : u = u'

Uniqueness of continuous L² solutions of eq:reg-mild-forced on [0, T].

theorem CKN.Leray.forcedMildSolution_energy (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH2 : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), u t = forcedMildRHS b h (regularizedMildClampedTensorTrajectory ρ ε hε T hT u) ↑t ⋯) : ∃ (v : ℝ → ↥ComplexVectorL2), (∀ (s : ℝ) (hs : s ∈ RegularizedMildTimeInterval T), realPartVectorL2 (v s) = u ⟨s, hs⟩) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 T), MeasureTheory.MemLp (forcedFourierGradHat (v s)) 2 MeasureTheory.volume) ∧ MeasureTheory.IntegrableOn (fun (s : ℝ) => forcedFourierDissipation (v s)) (Set.Ioc 0 T) MeasureTheory.volume ∧ ∀ (τ : ℝ) (hτ : τ ∈ RegularizedMildTimeInterval T), ‖u ⟨τ, hτ⟩‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 τ, forcedFourierDissipation (v s) ≤ ‖b‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 τ, inner ℝ (u (regularizedMildTimeClamp T hT s)) (h s)

The energy inequality eq:reg-energy-forced for the solution on [0, T], with the frequency dissipation of a complex solution curve whose real part is the solution.