The clamped tensor paths for the local mild map

These extensions let the translated Stokes integral use a fixed time interval while agreeing with the trajectory on its lifespan.

def CKN.Leray.regularizedMildTimeClamp (T : ℝ) (hT : 0 ≤ T) : ℝ → ↑(RegularizedMildTimeInterval T)

Clamp real time to the closed interval on which a mild trajectory is defined.

Equations

• CKN.Leray.regularizedMildTimeClamp T hT s = ⟨min T (max 0 s), ⋯⟩

theorem CKN.Leray.regularizedMildTimeClamp_continuous (T : ℝ) (hT : 0 ≤ T) : Continuous (regularizedMildTimeClamp T hT)

The clamping map is continuous.

theorem CKN.Leray.regularizedMildTimeClamp_eq_of_mem (T : ℝ) (hT : 0 ≤ T) {s : ℝ} (hs : s ∈ RegularizedMildTimeInterval T) : regularizedMildTimeClamp T hT s = ⟨s, hs⟩

Clamping does not change a time already in the trajectory interval.

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

Extend a trajectory's regularized tensor to every real time by clamping its argument to the interval.

Equations

• CKN.Leray.regularizedMildClampedTensorTrajectory ρ ε hε T hT u s = CKN.Leray.regularizedMildTensor ρ ε hε (u (CKN.Leray.regularizedMildTimeClamp T hT s))

theorem CKN.Leray.regularizedMildClampedTensorTrajectory_continuous (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) : Continuous (regularizedMildClampedTensorTrajectory ρ ε hε T hT u)

The clamped tensor path is continuous.

theorem CKN.Leray.regularizedMildClampedTensorTrajectory_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (R : ℝ) (hR : 0 ≤ R) (hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R) (s : ℝ) : ‖regularizedMildClampedTensorTrajectory ρ ε hε T hT u s‖ ≤ regularizedMildMollifierConstant ρ ε * R ^ 2

A uniform trajectory bound gives the source quadratic tensor bound on the clamped path.

theorem CKN.Leray.regularizedMildClampedTensorTrajectory_sub_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (u v : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (R : ℝ) (hR : 0 ≤ R) (hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R) (hv : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖v t‖ ≤ R) (s : ℝ) : ‖regularizedMildClampedTensorTrajectory ρ ε hε T hT u s - regularizedMildClampedTensorTrajectory ρ ε hε T hT v s‖ ≤ regularizedMildMollifierConstant ρ ε * (2 * R) * ‖u - v‖

The difference of two clamped tensor paths is controlled by the supremum-norm distance between their trajectories on a common ball.

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

The right-hand side of the mild equation, written with the translated integral over the fixed interval [0,T].

Equations

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

theorem CKN.Leray.regularizedMildLocalMap_eq_shifted (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (t : ↑(RegularizedMildTimeInterval T)) : (regularizedMildLocalMap ρ ε hε b T hT u) t = realHeatOperator ↑t ⋯ b - ∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand (regularizedMildClampedTensorTrajectory ρ ε hε T hT u) (↑t) τ

The value of the local map is the heat evolution minus the translated Stokes integral.

theorem CKN.Leray.regularizedMildLocalMap_eq_rightHandSide (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (t : ↑(RegularizedMildTimeInterval T)) : (regularizedMildLocalMap ρ ε hε b T hT u) t = regularizedMildRightHandSide b (fun (s : ℝ) => if hs : s ∈ RegularizedMildTimeInterval T then regularizedMildTensor ρ ε hε (u ⟨s, hs⟩) else 0) ↑t ⋯

The local map agrees with the mild equation eq:reg-mild on the trajectory interval.

theorem CKN.Leray.regularizedMildLocalMap_isInJ (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) (u : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (t : ↑(RegularizedMildTimeInterval T)) : RegularizedMildJData ((regularizedMildLocalMap ρ ε hε b T hT u) t)

The local mild map takes values in the closed Leray data space.