Compactness Modulus

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.continuous_of_two_term_time_modulus {T : Type u_1} [PseudoMetricSpace T] (F : T → ℝ) (C D θ : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hθ : 0 < θ) (hmod : ∀ (s t : T), |F t - F s| ≤ C * dist t s + D * dist t s ^ θ) : Continuous F

A two-term power modulus makes a real-valued map continuous.

def CKN.Leray.continuousMapOfTwoTermTimeModulus {T : Type u_1} [PseudoMetricSpace T] (F : T → ℝ) (C D θ : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hθ : 0 < θ) (hmod : ∀ (s t : T), |F t - F s| ≤ C * dist t s + D * dist t s ^ θ) : C(T, ℝ)

The two-term time modulus supplies continuous scalar pairing maps on each compact time window.

Equations

• CKN.Leray.continuousMapOfTwoTermTimeModulus F C D θ hC hD hθ hmod = { toFun := F, continuous_toFun := ⋯ }

theorem CKN.Leray.exists_common_subsequence_weak_pairings_of_two_term_moduli {ι : 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) (hmod : ∀ (i : ι) (m : ℕ), ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : T i), |inner ℝ (u n i t) (ψ i m) - inner ℝ (u n i s) (ψ i m)| ≤ A * dist t s + B * dist t s ^ θ) : ∃ (F : ℕ → (i : ι) → ℕ → C(T i, ℝ)), (∀ (n : ℕ) (i : ι) (m : ℕ) (t : T i), (F n i m) t = inner ℝ (u n i t) (ψ i m)) ∧ ∃ (σ : ℕ → ℕ), 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))

Countably many compact-time Hilbert families admit one weakly convergent subsequence when each dense-test pairing has a uniform two-term modulus.