Poincare Sobolev L1 Slice Basic

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.lpNorm_tendsto_of_diff {μ : MeasureTheory.Measure Foundation.Parabolic.Vec3} {p : ENNReal} (hp : 1 ≤ p) {f : Foundation.Parabolic.Vec3 → ℝ} {g : ℕ → Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p μ) (hg : ∀ (n : ℕ), MeasureTheory.MemLp (g n) p μ) (hsub : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => g n x - f x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.lpNorm (g n) p μ) Filter.atTop (nhds (MeasureTheory.lpNorm f p μ))

theorem CKN.continuous_vec3EuclideanNorm : Continuous Foundation.Parabolic.vec3EuclideanNorm

theorem CKN.eLpNorm_vec3_le_sum {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {μ : MeasureTheory.Measure Foundation.Parabolic.Vec3} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm f 2 μ ≤ ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f x i) 2 μ

theorem CKN.vec3Ball_eq_euclideanBall' {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : Foundation.Parabolic.vec3Ball x₀ r = euclideanBall x₀ r

theorem CKN.native_euclidean_norm_add_le (x y : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm (x + y) ≤ Foundation.Parabolic.vec3EuclideanNorm x + Foundation.Parabolic.vec3EuclideanNorm y

theorem CKN.native_norm_le_euclidean_norm (x : Foundation.Parabolic.Vec3) : ‖x‖ ≤ Foundation.Parabolic.vec3EuclideanNorm x

theorem CKN.native_euclidean_norm_le_sqrt_three_norm (x : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm x ≤ √3 * ‖x‖