Route AGradient Producer Uniform

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

The pressure-gradient producer at a free velocity exponent

The bootstrap of prop:bootstrap runs the velocity through the whole range τ ∈ [25/3, 25] of Morrey exponents, and each round needs the pressure gradient in M^{6/5, κ(τ)} with 1/κ(τ) = 1/τ + 1/τ₃ and τ₃ = 25/8, that is κ(τ) = (1/τ + 8/25)⁻¹. The symmetric-ball producer interfaces are stated here with τ free, and the established τ = 25/3 producers are identified as the base point of that family.

def CKN.Core.Step4.symmetricPressureGradientSliceProducerUniform : Prop

The slicewise L^{6/5} pressure-gradient production on the symmetric ball, with the incoming velocity Morrey exponent τ free. The conclusion does not mention τ: only the hypothesis on u does.

Equations

• One or more equations did not get rendered due to their size.

def CKN.Core.Step4.routeAGradientProducerUniform : Prop

The Route A pressure-gradient producer at a free velocity exponent. This is the statement consumed by the regularity provider for every τ that the bootstrap of prop:bootstrap visits.

Equations

• One or more equations did not get rendered due to their size.

The exponent τ = 25/3 instance. It identifies the established single-exponent slice interface as the base point of the uniform family.

theorem CKN.Core.Step4.symmetricPressureGradientSliceProducer_of_uniform (h : symmetricPressureGradientSliceProducerUniform) : symmetricPressureGradientSliceProducer

At τ = 25/3 the uniform slice producer is the established slice producer.

The slice production is exponent-generic for free: on a ball of finite radius the Morrey exponent can be lowered, so the established τ = 25/3 slice producer already yields the whole uniform family. The cell transfer is the only interface of the symmetric route that carries the exponent into its conclusion, so it is the one remaining τ-dependent analytic input.

theorem CKN.Core.Step4.symmetricPressureGradientSliceProducerUniform_of_base (h : symmetricPressureGradientSliceProducer) : symmetricPressureGradientSliceProducerUniform

The established slice producer gives the τ-uniform slice producer.