Time masses of slice majorants for prop:bootstrap

The whole-carrier 6/5 time mass of the localized pressure source in eq:pressure-gradient-decomposition is controlled by three slice integrals: the cube of the velocity slice norm, the square of the gradient slice norm, and the q-th power of the force slice norm. This file isolates the measure-theoretic step that converts those three integrals into the 6/5 mass of a majorant of the shape c₁ * (a * d) + c₂ * a ^ 2 + c₃ * F.

Every constant here is explicit, and no estimate below depends on the solution.

Pressure Gradient Origin BSlot Energy Holder

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

theorem CKN.Core.Step4.three_add_rpow_six_fifths_le (a b c : ENNReal) : (a + b + c) ^ (6 / 5) ≤ 4 * (a ^ (6 / 5) + b ^ (6 / 5) + c ^ (6 / 5))

The subadditivity of the power 6/5 for three terms, with the explicit constant 4: the 6/5-th power of a + b + c is bounded by four times the sum of the 6/5-th powers. It is obtained from (x + y) ^ p ≤ 2 ^ (p - 1) * (x ^ p + y ^ p) applied twice, together with the numerical bound 2 ^ (6/5 - 1) ≤ 2.

theorem CKN.Core.Step4.lintegral_rpow_le_measure_add_lintegral_rpow {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (h : α → ENNReal) {r t : ℝ} (hr : 0 ≤ r) (hrt : r ≤ t) : ∫⁻ (x : α), h x ^ r ∂μ ≤ μ Set.univ + ∫⁻ (x : α), h x ^ t ∂μ

A lower power of a nonnegative function costs only the total mass: the elementary split at the level one, used throughout prop:bootstrap.

theorem CKN.Core.Step4.rpow_mul_rpow_le_add (x y : ENNReal) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ ≤ 1) : x ^ θ * y ^ (1 - θ) ≤ x + y

Young's inequality in ℝ≥0∞: an interpolated product never exceeds the sum of its two endpoints.

theorem CKN.Core.Step4.lintegral_mul_six_fifths_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {a b : α → ENNReal} (ha : AEMeasurable a μ) (hb : AEMeasurable b μ) : ∫⁻ (x : α), (a x * b x) ^ (6 / 5) ∂μ ≤ (∫⁻ (x : α), a x ^ 3 ∂μ) ^ (2 / 5) * (∫⁻ (x : α), b x ^ 2 ∂μ) ^ (3 / 5)

Hölder's inequality at the exponents of eq:pressure-gradient-decomposition: the 6/5 mass of a product is controlled by the cube and the square masses.

theorem CKN.Core.Step4.slice_majorant_time_mass_le {J : Set ℝ} {M a d F : ℝ → ENNReal} {c₁ c₂ c₃ : ENNReal} {qq : ℝ} (ha : AEMeasurable a (MeasureTheory.volume.restrict J)) (hd : AEMeasurable d (MeasureTheory.volume.restrict J)) (hF : AEMeasurable F (MeasureTheory.volume.restrict J)) (hq : 6 / 5 ≤ qq) (hM : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, M s ≤ c₁ * (a s * d s) + c₂ * a s ^ 2 + c₃ * F s) {Ea Ed Ef : ENNReal} (hEa : ∫⁻ (s : ℝ) in J, a s ^ 3 ≤ Ea) (hEd : ∫⁻ (s : ℝ) in J, d s ^ 2 ≤ Ed) (hEf : ∫⁻ (s : ℝ) in J, F s ^ qq ≤ Ef) : ∫⁻ (s : ℝ) in J, M s ^ (6 / 5) ≤ 4 * (c₁ ^ (6 / 5) * (Ea + Ed) + c₂ ^ (6 / 5) * (MeasureTheory.volume J + Ea) + c₃ ^ (6 / 5) * (MeasureTheory.volume J + Ef))

The three-term majorant of eq:pressure-gradient-decomposition has an explicit 6/5 time mass built from the three slice integrals.