Compactness Weak Core

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.instFactLeENNRealOfNat_leanPool : Fact (1 ≤ 2)

theorem CKN.Leray.instFactNeENNRealOfNatTop_leanPool : Fact (2 ≠ ⊤)

def CKN.Leray.smoothCompactLpSet : Set ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)

The set of L² classes with a smooth compactly supported representative.

Equations

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

theorem CKN.Leray.exists_countable_dense_smooth_compact_vector_tests : ∃ (ψ : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3), (∀ (n : ℕ), HasCompactSupport (ψ n) ∧ ContDiff ℝ (↑⊤) (ψ n)) ∧ ∃ (hψ : ∀ (n : ℕ), MeasureTheory.MemLp (ψ n) 2 MeasureTheory.volume), DenseRange fun (n : ℕ) => MeasureTheory.MemLp.toLp (ψ n) ⋯

A countable family of smooth compactly supported vector fields is dense in global spatial L². It supplies the test family used for weak slice convergence in lem:compactness.

theorem CKN.Leray.exists_strictMono_tendsto_forall_of_isCompact_closure_range {ι : Type u_1} {β : ι → Type u_2} [Countable ι] [(i : ι) → TopologicalSpace (β i)] [∀ (i : ι), FirstCountableTopology (β i)] (f : ℕ → (i : ι) → β i) (hcompact : ∀ (i : ι), IsCompact (closure (Set.range fun (n : ℕ) => f n i))) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∃ (g : (i : ι) → β i), ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => f (ψ n) i) Filter.atTop (nhds (g i))

A countable family of relatively compact scalar sequences has one common subsequence on which every coordinate converges. This is the diagonal step in lem:compactness.

theorem CKN.Leray.isCompact_closure_range_of_equicontinuous {X : Type u_1} {β : Type u_2} [TopologicalSpace X] [CompactlyCoherentSpace X] [UniformSpace β] [T2Space β] [CompleteSpace β] (f : ℕ → C(X, β)) (hequi : EquicontinuousOn (fun (g : ↑(Set.range f)) => ⇑↑g) Set.univ) (hvalues : ∀ (x : X), ∃ (K : Set β), IsCompact K ∧ ∀ (n : ℕ), (f n) x ∈ K) : IsCompact (closure (Set.range f))

A uniformly equicontinuous family of continuous scalar maps on a compact space, with pointwise relatively compact values, is relatively compact in the uniform topology. This supplies the fixed-test time compactness in lem:compactness.

theorem CKN.Leray.exists_common_subsequence_uniform_convergence {ι : Type u_1} [Countable ι] {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), CompactSpace (X i)] [∀ (i : ι), CompactlyCoherentSpace (X i)] (F : ℕ → (i : ι) → C(X i, ℝ)) (hequi : ∀ (i : ι), EquicontinuousOn (fun (g : ↑(Set.range fun (n : ℕ) => F n i)) => ⇑↑g) Set.univ) (hvalues : ∀ (i : ι) (x : X i), ∃ (K : Set ℝ), IsCompact K ∧ ∀ (n : ℕ), (F n i) x ∈ K) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∃ (G : (i : ι) → C(X i, ℝ)), ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => F (ψ n) i) Filter.atTop (nhds (G i))

One subsequence makes a countable family of bounded equicontinuous scalar pairings converge uniformly on their compact time sets. This is the diagonal extraction in lem:compactness.

theorem CKN.Leray.exists_limit_clm_of_tendsto_on_dense_range {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℕ → E →L[ℝ] ℝ) (C : ℝ) (hC : 0 ≤ C) (hF : ∀ (n : ℕ), ‖F n‖ ≤ C) (ψ : ℕ → E) (hψ : DenseRange ψ) (hconv : ∀ (m : ℕ), ∃ (a : ℝ), Filter.Tendsto (fun (n : ℕ) => (F n) (ψ m)) Filter.atTop (nhds a)) : ∃ (L : E →L[ℝ] ℝ), (∀ (x : E), Filter.Tendsto (fun (n : ℕ) => (F n) x) Filter.atTop (nhds (L x))) ∧ ∀ (x : E), ‖L x‖ ≤ C * ‖x‖

Uniformly bounded linear functionals that converge on a dense sequence converge pointwise everywhere. The limit is again a continuous linear functional. This is the extension step in the Riesz representation argument for lem:compactness.

theorem CKN.Leray.exists_weak_limit_of_tendsto_pairings_on_dense_range {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (u : ℕ → E) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n : ℕ), ‖u n‖ ≤ C) (ψ : ℕ → E) (hψ : DenseRange ψ) (hpair : ∀ (m : ℕ), ∃ (a : ℝ), Filter.Tendsto (fun (n : ℕ) => inner ℝ (u n) (ψ m)) Filter.atTop (nhds a)) : ∃ (v : E), ∀ (x : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (u n) x) Filter.atTop (nhds (inner ℝ v x))

A bounded sequence in a real Hilbert space has a weak limit when its pairings converge on a dense sequence. This is the slice representation step in lem:compactness.