Compactness Uniform

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.eventually_uniform_pairing_convergence_of_dense_tests {T : Type u_1} {E : Type u_2} [PseudoMetricSpace T] [CompactSpace T] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : ℕ → T → E) (v : T → E) (ψ : ℕ → E) (hψ : DenseRange ψ) (C : ℝ) (hC : 0 ≤ C) (hubound : ∀ (n : ℕ) (t : T), ‖u n t‖ ≤ C) (hvbound : ∀ (t : T) (x : E), |inner ℝ (v t) x| ≤ C * ‖x‖) (F : ℕ → ℕ → C(T, ℝ)) (L : ℕ → C(T, ℝ)) (hpair : ∀ (n m : ℕ) (t : T), (F n m) t = inner ℝ (u n t) (ψ m)) (hLval : ∀ (m : ℕ) (t : T), (L m) t = inner ℝ (v t) (ψ m)) (hLconv : ∀ (m : ℕ), Filter.Tendsto (fun (n : ℕ) => F n m) Filter.atTop (nhds (L m))) (x : E) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : T), dist (inner ℝ (u n t) x) (inner ℝ (v t) x) < ε

Uniform convergence of pairings on a dense test sequence extends to every Hilbert-space test under a common slice bound. Ball averages are particular tests to which this conclusion applies.