Componentwise norm estimates used by Caccioppoli finiteness arguments.
theorem
CKN.caccioppoli_l2_component_bound
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
{u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{i : Fin 3}
(hu :
AEMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x i)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r)))
(humeas :
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r)))
:
(lpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) fun (x : Vec 3) => u x i) ≤ (∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u x)) ^ 2) ^ (1 / 2)
theorem
CKN.caccioppoli_gradient_component_bound
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
{g : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3}
{i : Fin 3}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r)))
:
(weakGradientLpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) fun (x : Vec 3) => g x i) ≤ (∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ENNReal.ofReal (∑ k : Fin 3, ∑ j : Fin 3, g x k j ^ 2)) ^ (1 / 2)
theorem
CKN.caccioppoli_eLpNorm_cube_eq_lintegral_abs_cube
{s : Set Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict s))
:
MeasureTheory.eLpNorm f 3 (MeasureTheory.volume.restrict s) ^ 3 = ∫⁻ (x : Foundation.Parabolic.Vec3) in s, ENNReal.ofReal |f x| ^ 3