Rellich Balls

Supporting estimates for the Navier–Stokes development.

theorem CKN.Foundation.exists_measurable_weights_for_finite_vec3_ball_cover {K : Set Parabolic.Vec3} (hK : IsCompact K) {ι : Type u_1} [Fintype ι] (c : ι → Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (hcover : K ⊆ ⋃ (i : ι), Parabolic.vec3Ball (c i) r) : ∃ (φ : ι → Parabolic.Vec3 → ℝ), (∀ (i : ι), Measurable (φ i)) ∧ (∀ (i : ι) (x : Parabolic.Vec3), 0 ≤ φ i x ∧ φ i x ≤ 1) ∧ (∀ x ∈ K, ∑ i : ι, φ i x = 1) ∧ (∀ (i : ι), ∀ x ∉ K, φ i x = 0) ∧ ∀ (i : ι), ∀ x ∈ K, φ i x ≠ 0 → x ∈ Parabolic.vec3Ball (c i) r

A finite cover of a compact set by equal-radius Euclidean balls admits measurable nonnegative weights summing to one, with each weight supported in its ball. These weights are used with the bounded-overlap ball cover in the spatial compactness argument for lem:compactness.

theorem CKN.Foundation.vec3EuclideanNorm_sq_weighted_sum_le {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (v : ι → Parabolic.Vec3) (hw : ∀ (i : ι), 0 ≤ w i) (hsum : ∑ i : ι, w i = 1) : Parabolic.vec3EuclideanNorm (∑ i : ι, w i • v i) ^ 2 ≤ ∑ i : ι, w i * Parabolic.vec3EuclideanNorm (v i) ^ 2

Squared Euclidean norm is convex under a finite partition of unity. This is the pointwise estimate used to combine the ball-average approximations in the local compactness argument.

theorem CKN.Foundation.sum_lintegral_le_of_finite_disjoint {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (t : Finset ι) (s : ι → Set α) (V : Set α) (f : α → ENNReal) (hdisj : (↑t).PairwiseDisjoint s) (hmeas : ∀ i ∈ t, MeasurableSet (s i)) (hsubset : ⋃ i ∈ t, s i ⊆ V) : ∑ i ∈ t, ∫⁻ (x : α) in s i, f x ∂μ ≤ ∫⁻ (x : α) in V, f x ∂μ

The integral of a nonnegative density over finitely many pairwise disjoint sets is bounded by its integral over any common containing set.