Compactness Weak

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.norm_le_of_weak_tendsto_of_uniform_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : ℕ → E} {v : E} {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (n : ℕ), ‖u n‖ ≤ C) (hweak : ∀ (x : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (u n) x) Filter.atTop (nhds (inner ℝ v x))) : ‖v‖ ≤ C

A uniform norm bound passes to a weak limit in a real Hilbert space.

theorem CKN.Leray.continuous_inner_of_dense_test_continuous {T : Type u_1} {E : Type u_2} [PseudoMetricSpace T] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : T → E) (ψ : ℕ → E) (hψ : DenseRange ψ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (t : T) (x : E), |inner ℝ (v t) x| ≤ C * ‖x‖) (hcontinuous : ∀ (m : ℕ), Continuous fun (t : T) => inner ℝ (v t) (ψ m)) (x : E) : Continuous fun (t : T) => inner ℝ (v t) x

Continuity of a uniformly bounded family of Hilbert pairings extends from a dense sequence of tests to every test.

theorem CKN.Leray.exists_common_subsequence_weak_pairings_on_compact_times {ι : Type u_1} [Countable ι] (T : ι → Type u_2) [(i : ι) → PseudoMetricSpace (T i)] [∀ (i : ι), CompactSpace (T i)] [∀ (i : ι), CompactlyCoherentSpace (T i)] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)] (u : ℕ → (i : ι) → T i → E i) (ψ : (i : ι) → ℕ → E i) (hψ : ∀ (i : ι), DenseRange (ψ i)) (C : ι → ℝ) (hC : ∀ (i : ι), 0 ≤ C i) (hbound : ∀ (n : ℕ) (i : ι) (t : T i), ‖u n i t‖ ≤ C i) (F : ℕ → (i : ι) → ℕ → C(T i, ℝ)) (hpair : ∀ (n : ℕ) (i : ι) (m : ℕ) (t : T i), (F n i m) t = inner ℝ (u n i t) (ψ i m)) (hequi : ∀ (i : ι) (m : ℕ), EquicontinuousOn (fun (g : ↑(Set.range fun (n : ℕ) => F n i m)) => ⇑↑g) Set.univ) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (v : (i : ι) → T i → E i), (∀ (i : ι) (t : T i) (x : E i), Filter.Tendsto (fun (n : ℕ) => inner ℝ (u (σ n) i t) x) Filter.atTop (nhds (inner ℝ (v i t) x))) ∧ (∀ (i : ι) (x : E i), Continuous fun (t : T i) => inner ℝ (v i t) x) ∧ (∀ (i : ι) (t : T i) (x : E i), |inner ℝ (v i t) x| ≤ C i * ‖x‖) ∧ ∃ (L : (i : ι) → ℕ → C(T i, ℝ)), (∀ (i : ι) (m : ℕ) (t : T i), (L i m) t = inner ℝ (v i t) (ψ i m)) ∧ ∀ (i : ι) (m : ℕ), Filter.Tendsto (fun (n : ℕ) => F (σ n) i m) Filter.atTop (nhds (L i m))

A single subsequence gives weakly convergent slices on every member of a countable family of compact time regions. Pairings with every Hilbert test are continuous on each region. This is the diagonal local form of the slice selection in lem:compactness.

theorem CKN.Leray.equicontinuous_of_two_term_time_modulus {T : Type u_1} [PseudoMetricSpace T] (F : ℕ → C(T, ℝ)) (C D θ : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hθ : 0 < θ) (hmod : ∀ (n : ℕ) (s t : T), |(F n) t - (F n) s| ≤ C * dist t s + D * dist t s ^ θ) : EquicontinuousOn (fun (g : ↑(Set.range F)) => ⇑↑g) Set.univ

A uniform two-term time modulus makes a sequence of real continuous maps equicontinuous. This converts the pairing estimate in lem:compactness into the input required for Arzelà--Ascoli.