Compactness Interval Bridge

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.compact_time_slice_bounds_of_interval_bounds {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : I.OrdConnected) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hbound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∃ M < ⊤, ∀ (n : ℕ), ∀ t ∈ Set.Icc a b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) (C : Set Foundation.Parabolic.Vec3) : IsCompact C → C ⊆ U → ∀ (T : Set ℝ), IsCompact T → T ⊆ I → ∃ M < ⊤, ∀ (n : ℕ), ∀ t ∈ T, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M

Uniform slice bounds on compact intervals extend to arbitrary compact time sets inside the same interval.

theorem CKN.Leray.compact_time_gradient_bounds_of_interval_bounds {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : I.OrdConnected) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (hbound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∃ G < ⊤, ∀ (n : ℕ), ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) (C : Set Foundation.Parabolic.Vec3) : IsCompact C → C ⊆ U → ∀ (T : Set ℝ), IsCompact T → T ⊆ I → ∃ G < ⊤, ∀ (n : ℕ), ∫⁻ (t : ℝ) in T, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G

Integrated gradient bounds on compact intervals extend to compact time sets by monotonicity of the outer integral.

theorem CKN.Leray.compact_time_pairing_modulus_of_interval_modulus {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : I.OrdConnected) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hmod : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3), ContDiff ℝ (↑⊤) w → HasCompactSupport w → tsupport w ⊆ C → ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ) (C : Set Foundation.Parabolic.Vec3) : IsCompact C → C ⊆ U → ∀ (T : Set ℝ), IsCompact T → T ⊆ I → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3), ContDiff ℝ (↑⊤) w → HasCompactSupport w → tsupport w ⊆ C → ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), s ∈ T → t ∈ T → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ

A pairing modulus on compact intervals restricts to each compact time set in the open interval.