The three-term Morrey majorant of the centred source correction #

The centred correction splits pointwise into the divergence source on the source ball, the cutoff-derivative quadratic terms on the collar, and the mean-gradient terms on the collar. Each is measured on its own carrier, the last two by a Morrey Hölder product at the endpoint exponent, and the endpoint is transferred to the exponent-dependent one for free on a carrier of radius at most one.

source

theorem CKN.Core.Step4.originASlot_cutoff_zero_off_collar (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (x : Foundation.Parabolic.Vec3) :

x ∉ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4) → mollifiedBallCutoff x₀ hρ x = 0

The centred cutoff vanishes off the plateau-and-transition ball.

source

theorem CKN.Core.Step4.originASlot_dcutoff_zero_off_collar (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (k : Fin 3) (x : Foundation.Parabolic.Vec3) :

x ∉ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4) → spatialDeriv (mollifiedBallCutoff x₀ hρ) k x = 0

Every first spatial derivative of the centred cutoff vanishes off the plateau-and-transition ball.

source

|S.indicator (fun (v : Foundation.Parabolic.ParabolicPoint) => centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η dη (fun (y : Foundation.Parabolic.Vec3) => u' (y, v.2)) (fun (y : Foundation.Parabolic.Vec3) => f' (y, v.2)) (fun (y : Foundation.Parabolic.Vec3) => Du' (y, v.2)) (c v.2) j v.1) w| ≤ |S.indicator (fun (v : Foundation.Parabolic.ParabolicPoint) => ∑ k : Fin 3, Du' v j k * u' v k - f' v j) w| + Kη * ∑ k : Fin 3, |S₃.indicator (fun (v : Foundation.Parabolic.ParabolicPoint) => u' v j * (u' v k - c v.2 k)) w| + ∑ k : Fin 3, |S₃.indicator (fun (v : Foundation.Parabolic.ParabolicPoint) => Du' v j k * c v.2 k) w|

The carrier-restricted correction is dominated by the divergence source, the mean-free quadratic terms and the mean-gradient terms, each on its own carrier.

source

theorem CKN.Core.Step4.morreyNorm_abs_eq {p τ : ℝ} (hp : 0 ≤ p) (F : Foundation.Parabolic.ParabolicPoint → ℝ) :

(Foundation.Parabolic.Morrey.morreyNorm p τ fun (w : Foundation.Parabolic.ParabolicPoint) => |F w|) = Foundation.Parabolic.Morrey.morreyNorm p τ F

The parabolic Morrey seminorm is unchanged by taking absolute values.

source

theorem CKN.Core.Step4.morreyNorm_sum_three_abs_le {p τ : ℝ} (hp : 1 ≤ p) {g : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ∀ (k : Fin 3), AEMeasurable (g k) MeasureTheory.volume) :

(Foundation.Parabolic.Morrey.morreyNorm p τ fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ k : Fin 3, |g k w|) ≤ ∑ k : Fin 3, Foundation.Parabolic.Morrey.morreyNorm p τ (g k)

A three-term sum of absolute values has the sum of the seminorms.

source

theorem CKN.Core.Step4.morreyNorm_le_three_terms {p τ : ℝ} (hp : 1 ≤ p) {F A B C : Foundation.Parabolic.ParabolicPoint → ℝ} (hA : AEMeasurable A MeasureTheory.volume) (hB : AEMeasurable B MeasureTheory.volume) (hC : AEMeasurable C MeasureTheory.volume) (hdom : ∀ (w : Foundation.Parabolic.ParabolicPoint), |F w| ≤ |A w| + |B w| + |C w|) :

Foundation.Parabolic.Morrey.morreyNorm p τ F ≤ Foundation.Parabolic.Morrey.morreyNorm p τ A + Foundation.Parabolic.Morrey.morreyNorm p τ B + Foundation.Parabolic.Morrey.morreyNorm p τ C

A field dominated pointwise by three terms has the sum of their seminorms.

source

theorem CKN.Core.Step4.originASlot_endpoint_exponent_inv {τ : ℝ} (hτ : 25 / 3 ≤ τ) :

1 / (1 / τ + 8 / 25)⁻¹ = 1 / τ + 1 / (25 / 8)

The endpoint Morrey exponent splits as the velocity and gradient pair.

source

theorem CKN.Core.Step4.originASlot_product_morreyNorm_le {τ : ℝ} (hτ : 25 / 3 ≤ τ) {S T : Set Foundation.Parabolic.ParabolicPoint} {a b : Foundation.Parabolic.ParabolicPoint → ℝ} {KA KB : ENNReal} (hsub : S ⊆ T) (ham : AEMeasurable (S.indicator a) MeasureTheory.volume) (hbm : AEMeasurable (T.indicator b) MeasureTheory.volume) (ha : Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator a) ≤ KA) (hb : Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) (T.indicator b) ≤ KB) :

Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (1 / τ + 8 / 25)⁻¹ (S.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => a w * b w) ≤ KA * KB

The product of an L³ Morrey factor and an L² Morrey factor on nested carriers is an L^{6/5} Morrey object at the matched exponent.

source

theorem CKN.Core.Step4.originASlot_morreyNorm_endpoint_drop {τ q R : ℝ} (hτ : 25 / 3 ≤ τ) (hq : 5 / 2 < q) (hR : 0 < R) (hR1 : R ≤ 1) {F : Foundation.Parabolic.ParabolicPoint → ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} (hsupp : ∀ w ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, F w = 0) :

Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) F ≤ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (1 / τ + 8 / 25)⁻¹ F

On a carrier of radius at most one the exponent-dependent Morrey seminorm is below the endpoint one.

source

Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (S.indicator fun (v : Foundation.Parabolic.ParabolicPoint) => centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η dη (fun (y : Foundation.Parabolic.Vec3) => u' (y, v.2)) (fun (y : Foundation.Parabolic.Vec3) => f' (y, v.2)) (fun (y : Foundation.Parabolic.Vec3) => Du' (y, v.2)) (c v.2) j v.1) ≤ XA + ENNReal.ofReal Kη * (3 * (KU * Mfree)) + 3 * (KD * Mc)

The carrier-restricted centred correction has a Morrey majorant built from the divergence source, the mean-free quadratic budget and the mean-gradient budget.

Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Step4.PressureGradientOriginASlotM2Split

The three-term Morrey majorant of the centred source correction #