The truncated forced mild map on a bounded interval

The right-hand side of eq:reg-mild-forced, with the regularized tensor of the radially truncated velocity, defines a map on continuous L² curves over [0, T]. The Abel kernel paired with an exponential weight has integral of order λ^{-1/2}, which makes the map a contraction in an exponentially weighted norm; this gives existence and uniqueness of the truncated solution on the whole interval, as in lem:regularised-forced.

theorem CKN.Leray.integral_abelKernel_exp_le {lam t : ℝ} (hlam : 0 < lam) (ht : 0 ≤ t) : ∫ (s : ℝ) in Set.Ioc 0 t, (t - s) ^ (-(1 / 2)) * Real.exp (-lam * (t - s)) ≤ lam ^ (-(1 / 2)) * Real.Gamma (1 / 2)

The weighted Abel kernel has integral at most λ^{-1/2} Γ(1/2).

theorem CKN.Leray.continuous_forcedTruncTensor (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (hR : 0 ≤ R) : Continuous (forcedTruncTensor ρ ε hε R)

noncomputable def CKN.Leray.forcedTensorCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (R T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : ℝ → ↥RealTensorL2

The truncated tensor curve of a trajectory on [0, T], clamped to all real times.

Equations

• CKN.Leray.forcedTensorCurve ρ ε hε R T hT u s = CKN.Leray.forcedTruncTensor ρ ε hε R (u (CKN.Leray.regularizedMildTimeClamp T hT s))

theorem CKN.Leray.continuous_forcedTensorCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (hR : 0 ≤ R) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : Continuous (forcedTensorCurve ρ ε hε R T hT u)

theorem CKN.Leray.norm_forcedTensorCurve_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (hR : 0 ≤ R) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (s : ℝ) : ‖forcedTensorCurve ρ ε hε R T hT u s‖ ≤ regularizedMildMollifierConstant ρ ε * R ^ 2

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

The truncated forced mild map on continuous curves over [0, T].

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.forcedMildMap_apply (ρ : 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)) (t : ↑(RegularizedMildTimeInterval T)) : (forcedMildMap ρ ε hε b hh hH hR T hT u) t = forcedMildRHS b h (forcedTensorCurve ρ ε hε R T hT u) ↑t ⋯

theorem CKN.Leray.integrableOn_regularizedMildStokesIntegrand {F : ℝ → ↥RealTensorL2} (hF : MeasureTheory.StronglyMeasurable F) {t C : ℝ} (ht : 0 ≤ t) (hFC : ∀ s ∈ Set.Ioc 0 t, ‖F s‖ ≤ C) : MeasureTheory.IntegrableOn (regularizedMildStokesIntegrand F t) (Set.Ioc 0 t) MeasureTheory.volume

The Stokes Duhamel integrand of a bounded tensor curve is integrable.

theorem CKN.Leray.norm_regularizedMildStokesIntegral_sub_le {F₁ F₂ : ℝ → ↥RealTensorL2} (hF₁ : MeasureTheory.StronglyMeasurable F₁) (hF₂ : MeasureTheory.StronglyMeasurable F₂) {t C M lam : ℝ} (ht : 0 ≤ t) (hFC₁ : ∀ s ∈ Set.Ioc 0 t, ‖F₁ s‖ ≤ C) (hFC₂ : ∀ s ∈ Set.Ioc 0 t, ‖F₂ s‖ ≤ C) (hdiff : ∀ s ∈ Set.Ioc 0 t, ‖F₁ s - F₂ s‖ ≤ M * Real.exp (lam * s)) : ‖regularizedMildStokesIntegral F₁ t - regularizedMildStokesIntegral F₂ t‖ ≤ M / √(2 * Real.exp 1) * ∫ (s : ℝ) in Set.Ioc 0 t, (t - s) ^ (-(1 / 2)) * Real.exp (lam * s)

The difference of Stokes Duhamel integrals of two tensor curves whose difference grows at most exponentially is bounded by the weighted Abel integral.

noncomputable def CKN.Leray.forcedExpWeight (lam T : ℝ) (v : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)

Multiplication of a curve on [0, T] by the exponential weight e^{λt}.

Equations

• CKN.Leray.forcedExpWeight lam T v = { toFun := fun (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)) => Real.exp (lam * ↑t) • v t, continuous_toFun := ⋯ }

theorem CKN.Leray.forcedExpWeight_apply (lam T : ℝ) (v : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (t : ↑(RegularizedMildTimeInterval T)) : (forcedExpWeight lam T v) t = Real.exp (lam * ↑t) • v t

theorem CKN.Leray.forcedExpWeight_neg_cancel (lam T : ℝ) (v : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : forcedExpWeight (-lam) T (forcedExpWeight lam T v) = v

theorem CKN.Leray.forcedExpWeight_cancel_neg (lam T : ℝ) (v : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : forcedExpWeight lam T (forcedExpWeight (-lam) T v) = v

theorem CKN.Leray.norm_forcedMildMap_weighted_sub_le (ρ : 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) {lam : ℝ} (hlam : 0 < lam) (v₁ v₂ : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (t : ↑(RegularizedMildTimeInterval T)) : ‖(forcedExpWeight (-lam) T (forcedMildMap ρ ε hε b hh hH hR T hT (forcedExpWeight lam T v₁))) t - (forcedExpWeight (-lam) T (forcedMildMap ρ ε hε b hh hH hR T hT (forcedExpWeight lam T v₂))) t‖ ≤ 4 * regularizedMildMollifierConstant ρ ε * R / √(2 * Real.exp 1) * (lam ^ (-(1 / 2)) * Real.Gamma (1 / 2)) * ‖v₁ - v₂‖

The weighted Lipschitz estimate for the truncated forced mild map.

theorem CKN.Leray.exists_forcedWeight (A : ℝ) : ∃ (lam : ℝ), 0 < lam ∧ A * lam ^ (-(1 / 2)) ≤ 1 / 2

A weight exponent making the weighted map a contraction with constant 1/2.

theorem CKN.Leray.forcedMildMap_existsUnique_fixedPoint (ρ : 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)), forcedMildMap ρ ε hε b hh hH hR T hT u = u ∧ ∀ (u' : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)), forcedMildMap ρ ε hε b hh hH hR T hT u' = u' → u' = u

The truncated forced mild map has a unique fixed point among continuous curves on [0, T].