The forced regularized solution for all times

The solutions of eq:reg-mild-forced on the intervals [0, T] agree on common times by uniqueness and causality, so they define one continuous divergence-free L² curve on [0, ∞), as stated at the end of the proof of lem:regularised-forced.

noncomputable def CKN.Leray.forcedSolutionOn (ρ : 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) : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)

The solution of eq:reg-mild-forced on [0, T].

Equations

• CKN.Leray.forcedSolutionOn ρ ε hε b hb hh hH2 T hT = Classical.choose ⋯

theorem CKN.Leray.forcedSolutionOn_spec (ρ : 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) : (∀ (t : ↑(RegularizedMildTimeInterval T)), (forcedSolutionOn ρ ε hε b hb hh hH2 T hT) t = forcedMildRHS b h (regularizedMildClampedTensorTrajectory ρ ε hε T hT (forcedSolutionOn ρ ε hε b hb hh hH2 T hT)) ↑t ⋯) ∧ ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖(forcedSolutionOn ρ ε hε b hb hh hH2 T hT) t‖ ^ 2 ≤ (‖b‖ ^ 2 + ∫ (s : ℝ) in Set.Ioc 0 T, ‖h s‖ ^ 2) * Real.exp T

theorem CKN.Leray.forcedSolutionOn_consistent (ρ : 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 T' : ℝ} (hT : 0 ≤ T) (hTT' : T ≤ T') {s : ℝ} (hs : s ∈ RegularizedMildTimeInterval T) : (forcedSolutionOn ρ ε hε b hb hh hH2 T hT) ⟨s, hs⟩ = (forcedSolutionOn ρ ε hε b hb hh hH2 T' ⋯) ⟨s, ⋯⟩

Solutions on nested intervals agree on the smaller interval.

theorem CKN.Leray.forcedSolutionOn_congr (ρ : 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) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A = B) (x : ↑(RegularizedMildTimeInterval A)) (y : ↑(RegularizedMildTimeInterval B)) (hxy : ↑x = ↑y) : (forcedSolutionOn ρ ε hε b hb hh hH2 A hA) x = (forcedSolutionOn ρ ε hε b hb hh hH2 B hB) y

noncomputable def CKN.Leray.forcedSolutionCurve (ρ : 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 : ℝ) : ↥RealVectorL2

The forced regularized solution curve on the real line; negative times are mapped to time zero.

Equations

• CKN.Leray.forcedSolutionCurve ρ ε hε b hb hh hH2 t = (CKN.Leray.forcedSolutionOn ρ ε hε b hb hh hH2 (max t 0 + 1) ⋯) ⟨max t 0, ⋯⟩

theorem CKN.Leray.forcedSolutionCurve_eq (ρ : 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) {t : ℝ} (ht : t ∈ RegularizedMildTimeInterval T) : forcedSolutionCurve ρ ε hε b hb hh hH2 t = (forcedSolutionOn ρ ε hε b hb hh hH2 T hT) ⟨t, ht⟩

On [0, T] the solution curve is the solution on [0, T].

theorem CKN.Leray.forcedSolutionCurve_of_nonpos (ρ : 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 : t ≤ 0) : forcedSolutionCurve ρ ε hε b hb hh hH2 t = forcedSolutionCurve ρ ε hε b hb hh hH2 0

At negative times the solution curve takes its initial value.

theorem CKN.Leray.continuous_forcedSolutionCurve (ρ : 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) : Continuous (forcedSolutionCurve ρ ε hε b hb hh hH2)

theorem CKN.Leray.forcedSolutionCurve_mild (ρ : 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) : forcedSolutionCurve ρ ε hε b hb hh hH2 t = forcedMildRHS b h (fun (s : ℝ) => regularizedMildTensor ρ ε hε (forcedSolutionCurve ρ ε hε b hb hh hH2 s)) t ht

The solution curve solves eq:reg-mild-forced at every nonnegative time.

theorem CKN.Leray.forcedForceDuhamel_zero_time (h : ℝ → ↥RealVectorL2) : forcedForceDuhamel h 0 = 0

theorem CKN.Leray.forcedSolutionCurve_zero (ρ : 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) : forcedSolutionCurve ρ ε hε b hb hh hH2 0 = b

The solution curve starts at the datum.

theorem CKN.Leray.forcedSolutionCurve_mildJData (ρ : 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) : RegularizedMildJData (forcedSolutionCurve ρ ε hε b hb hh hH2 t)

The solution curve takes values in the divergence-free space.

theorem CKN.Leray.forcedSolutionCurve_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) : ∃ (v : ℝ → ↥ComplexVectorL2), (∀ s ∈ RegularizedMildTimeInterval T, realPartVectorL2 (v s) = forcedSolutionCurve ρ ε hε b hb hh hH2 s) ∧ (∀ᵐ (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 ∧ ∀ τ ∈ RegularizedMildTimeInterval T, ‖forcedSolutionCurve ρ ε hε b hb hh hH2 τ‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 τ, forcedFourierDissipation (v s) ≤ ‖b‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 τ, inner ℝ (forcedSolutionCurve ρ ε hε b hb hh hH2 s) (h s)

The energy inequality eq:reg-energy-forced for the solution curve on [0, T].