Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Step4.PressureGradientGluedTransferClause

The every-cell bound of the symmetric carrier, in its two regimes #

The uniform Route A gradient conclusion asks for one integrable weak pressure gradient on the inner parabolic ball whose Morrey cells are bounded at every centre and every positive radius by a single finite constant. That bound cannot be proved by one uniform argument: the slice estimate at a cell's own scale needs the doubled cell to stay inside the region where the solution is controlled, which fails once the cell is large compared with its distance to the boundary of the carrier.

The bound therefore has two regimes. Below the margin scale r₀ the cell is controlled at its own radius; at or above r₀ the cell power integral is at most the integral over the whole carrier, and since the growth exponent 5 (1 - (6/5)/κ) is nonnegative for 6/5 ≤ κ, that constant bound is itself of the required growth form, at the price of the explicit factor r₀ ^ (-(5 (1 - (6/5)/κ))).

The margin scale of this carrier is R / 3: a cell of radius at most R / 3 that meets the inner ball Metric.ball z₀ (R / 2) has its doubled parabolic cylinder inside Metric.ball z₀ (2 * R), which is the region the hypotheses control.

Pressure Gradient HGCloser Transfer #

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

Pressure-gradient Morrey membership for an identified field #

The cell estimate applies to the same integrable weak pressure gradient produced on the inner parabolic ball. Its finite bound is uniform over components, cell centres, and radii, but may depend on the solution.

theorem CKN.Core.Step4.routeA_gradient_of_glued_field_cell_bounds (hGlued : ∀ (q τ : ℝ), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ), 0 < R → Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I → morreyVecMem 3 τ (Metric.ball z₀ R) u → (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (R / 2) → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∃ (Ccell : ℝ), ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : { r : ℝ // 0 < r }), Foundation.Parabolic.Morrey.morreyCell (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z ↑r ≤ ENNReal.ofReal Ccell) :

Convert a glued integrable weak pressure gradient with bounds on every Morrey cell into the uniform Route A gradient conclusion.

The integral of a field over a measurable carrier is unchanged by restricting the field to that carrier.

theorem CKN.Core.Step4.exists_routeA_cell_constant_of_two_regime_bounds {z₀ : Foundation.Parabolic.ParabolicPoint} {R κ r₀ : ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {A B : ENNReal} (hκ : 6 / 5 ≤ κ) (hr₀ : 0 < r₀) (hA : A < ⊤) (hB : B < ⊤) (hsmall : ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → r ≤ r₀ → Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))) (hglobal : ∀ (i : Fin 3), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Metric.ball z₀ (R / 2), ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ B) :
∃ (Ccell : ℝ), ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : { r : ℝ // 0 < r }), Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z ↑r ≤ ENNReal.ofReal Ccell

The single finite every-cell constant of the uniform Route A conclusion, assembled from the margin-safe cells and the whole-carrier integral. The field is fixed before the two integral constants, and both constants are bound after it; nothing here quantifies a bound before the field.

theorem CKN.Core.Step4.routeA_gradient_of_two_regime_glued_field (hGlued : ∀ (q τ : ℝ), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ), 0 < R → Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I → morreyVecMem 3 τ (Metric.ball z₀ R) u → (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (R / 2) → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∃ (A : ENNReal) (B : ENNReal), A < ⊤ ∧ B < ⊤ ∧ (∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → r ≤ R / 3 → Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) ∧ ∀ (i : Fin 3), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Metric.ball z₀ (R / 2), ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ B) :

The uniform Route A gradient conclusion from a glued field whose every-cell bound is supplied in the two regimes. The field comes first; the two integral constants and their finiteness are bound after it, and every cell clause refers to that same field.

theorem CKN.Core.Step4.exists_routeA_cell_constant_of_small_cells_and_carrier_integral {z₀ : Foundation.Parabolic.ParabolicPoint} {R κ r₀ : ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {A B : ENNReal} (hκ : 6 / 5 ≤ κ) (hr₀ : 0 < r₀) (hA : A < ⊤) (hB : B < ⊤) (hsmall : ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → r ≤ r₀ → Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))) (hglobal : ∀ (i : Fin 3), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Metric.ball z₀ (R / 2), ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ B) :
∃ (Ccell : ℝ), ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : { r : ℝ // 0 < r }), Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z ↑r ≤ ENNReal.ofReal Ccell

The same every-cell constant, assembled from the two regimes separately: the small-cell growth bound below the margin scale, and the established large-cell normalization of the whole-carrier integral at or above it. This is the form in which the two halves are read off independently, and its constant is the sum of the two contributions rather than the power of a sum.