Harmonic Part Bounds Helpers

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

Summation, normalization and localization helpers for the all-order harmonic pressure estimate: derivative bounds for finite sums of potentials and the annulus power normalizations used at each order.

theorem CKN.norm_iteratedFDeriv_sum_le {ι : Type u_1} {s : Finset ι} {P : ι → Foundation.Parabolic.Vec3 → ℝ} {U : Set Foundation.Parabolic.Vec3} {k : ℕ} (hU : IsOpen U) (hP : ∀ i ∈ s, ContDiffOn ℝ (↑k) (P i) U) {x : Foundation.Parabolic.Vec3} (hx : x ∈ U) : ‖iteratedFDeriv ℝ k (∑ i ∈ s, P i) x‖ ≤ ∑ i ∈ s, ‖iteratedFDeriv ℝ k (P i) x‖

theorem CKN.norm_iteratedFDeriv_fin3_sum_le {P : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {U : Set Foundation.Parabolic.Vec3} {k : ℕ} (hU : IsOpen U) (hP : ∀ (i : Fin 3), ContDiffOn ℝ (↑k) (P i) U) {x : Foundation.Parabolic.Vec3} (hx : x ∈ U) : ‖iteratedFDeriv ℝ k (∑ i : Fin 3, P i) x‖ ≤ ∑ i : Fin 3, ‖iteratedFDeriv ℝ k (P i) x‖

theorem CKN.annulus_power_normalize_potential {ρ : ℝ} (hρ : 0 < ρ) (k : ℕ) : ((3 * ρ / 20) ^ (1 + k))⁻¹ * (ρ ^ 2)⁻¹ * ρ = (3 / 20) ^ (-(1 + ↑k)) * ρ ^ (-(2 + ↑k))

theorem CKN.annulus_power_normalize_derivative {ρ : ℝ} (hρ : 0 < ρ) (k : ℕ) : ((3 * ρ / 20) ^ (2 + k))⁻¹ * (ρ ^ 1)⁻¹ * ρ = (3 / 20) ^ (-(2 + ↑k)) * ρ ^ (-(2 + ↑k))

theorem CKN.integral_abs_mul_le_ball_indicator {a b N : Foundation.Parabolic.Vec3 → ℝ} {A B : Set Foundation.Parabolic.Vec3} {K : ℝ} (hInt : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => a y * b y) MeasureTheory.volume) (hN : MeasureTheory.Integrable N (MeasureTheory.volume.restrict B)) (hN0 : ∀ (y : Foundation.Parabolic.Vec3), 0 ≤ N y) (hK : 0 ≤ K) (hB : MeasurableSet B) (hsub : A ⊆ B) (hA : ∀ (y : Foundation.Parabolic.Vec3), a y * b y ≠ 0 → y ∈ A) (ha : ∀ (y : Foundation.Parabolic.Vec3), |a y| ≤ K) (hb : ∀ (y : Foundation.Parabolic.Vec3), |b y| ≤ N y) : ∫ (y : Foundation.Parabolic.Vec3), |a y * b y| ≤ K * ∫ (y : Foundation.Parabolic.Vec3) in B, N y

theorem CKN.norm_iteratedFDeriv_add_le {f g : Foundation.Parabolic.Vec3 → ℝ} {k : ℕ} {x : Foundation.Parabolic.Vec3} (hf : ContDiffAt ℝ (↑k) f x) (hg : ContDiffAt ℝ (↑k) g x) : ‖iteratedFDeriv ℝ k (f + g) x‖ ≤ ‖iteratedFDeriv ℝ k f x‖ + ‖iteratedFDeriv ℝ k g x‖