Compactness Exhaustion

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.Leray.compactExhaustionSubtypeVec3 (U : Set Foundation.Parabolic.Vec3) (hU : IsOpen U) : CompactExhaustion { x : Foundation.Parabolic.Vec3 // x ∈ U }

A compact exhaustion of the subtype of an open subset of a finite dimensional Euclidean space.

Equations

• CKN.Leray.compactExhaustionSubtypeVec3 U hU = CompactExhaustion.choice { x : CKN.Foundation.Parabolic.Vec3 // x ∈ U }

theorem CKN.Leray.exists_compact_exhaustion_of_open_vec3 (U : Set Foundation.Parabolic.Vec3) (hU : IsOpen U) : ∃ (K : ℕ → Set Foundation.Parabolic.Vec3), (∀ (n : ℕ), IsCompact (K n)) ∧ (∀ (n : ℕ), K n ⊆ U) ∧ (∀ (n : ℕ), K n ⊆ K (n + 1)) ∧ (∀ (n : ℕ), K n ⊆ interior (K (n + 1))) ∧ ⋃ (n : ℕ), K n = U

A compact exhaustion of an open Euclidean domain, written as compact ambient sets.

theorem CKN.Leray.exists_compact_exhaustion_cutoffs_vec3 (U : Set Foundation.Parabolic.Vec3) (hU : IsOpen U) : ∃ (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ), (∀ (n : ℕ), IsCompact (K n) ∧ K n ⊆ U ∧ K n ⊆ K (n + 1) ∧ K n ⊆ interior (K (n + 1))) ∧ ⋃ (n : ℕ), K n = U ∧ ∀ (n : ℕ), ContDiff ℝ (↑⊤) (χ n) ∧ HasCompactSupport (χ n) ∧ tsupport (χ n) ⊆ U ∧ (∀ (x : Foundation.Parabolic.Vec3), χ n x ∈ Set.Icc 0 1) ∧ ∀ x ∈ K n, χ n x = 1

Smooth compactly supported cutoffs equal to one on a compact exhaustion of an open spatial domain.

theorem CKN.Leray.compact_subset_eventually_in_exhaustion {U C : Set Foundation.Parabolic.Vec3} (hC : IsCompact C) (hCU : C ⊆ U) (K : ℕ → Set Foundation.Parabolic.Vec3) (hmono : ∀ (j : ℕ), K j ⊆ K (j + 1)) (hinner : ∀ (j : ℕ), K j ⊆ interior (K (j + 1))) (hcover : ⋃ (j : ℕ), K j = U) : ∃ (j : ℕ), C ⊆ K j

Every compact subset of an open domain lies in one member of an exhaustion whose successive members contain the previous ones in their interiors.

@[reducible, inline]

abbrev CKN.Leray.RationalCompactTimeWindow (I : Set ℝ) : Type

Rational closed intervals compactly contained in an open time domain.

Equations

• CKN.Leray.RationalCompactTimeWindow I = { p : ℚ × ℚ // ↑p.1 < ↑p.2 ∧ Set.Icc ↑p.1 ↑p.2 ⊆ I }

theorem CKN.Leray.exists_rational_compact_time_window_around {I : Set ℝ} (hI : IsOpen I) {t : ℝ} (ht : t ∈ I) : ∃ (p : RationalCompactTimeWindow I), t ∈ Set.Ioo ↑(↑p).1 ↑(↑p).2

Every time in an open domain lies in the interior of a rational compact time window contained in that domain.