Monotonicity of the scale quantities in the radius

This module formalizes Lemma lem:monotonicity of paper/ckn.tex. For a fixed centre z and radii 0 < r₁ ≤ r₂, the five quantities alpha, beta, gamma, delta and lambda of paper/ckn.tex grow at most like the powers of r₂ / r₁ printed in the lemma. The paper's statement of the fourth inequality is the squared form δ(z,r₁)² ≤ (r₂/r₁)^{4/3} δ(z,r₂)²; the companion Remark rem:kukavica-monotonicity also records the equivalent unsquared form with the exponent 2/3. The theorem delta_sq_mono_radius below proves the squared form used by the iteration estimates.

Each inequality has two ingredients. Enlarging the cylinder (or the time-slice domain) makes the underlying nonnegative integral, respectively time-slice essential supremum, monotone; this is supplied by the radius-monotonicity lemmas of the parabolic integration library. The remaining step is elementary real algebra with Real.rpow, isolated below as lemmas over abstract reals so that the rpow atoms stay opaque.

The definitions evaluate the underlying nonnegative integral with ENNReal.toReal, which sends ⊤ to 0. The paper's inequalities therefore require the relevant quantity at the larger radius to be finite: this is the hfin hypothesis below, and it holds for the suitable weak solutions considered in paper/ckn.tex.

theorem CKN.alpha_mono_radius (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hfin : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 r₂ fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) ≠ ⊤) : alpha u z r₁ ≤ (r₂ / r₁) ^ (1 / 2) * alpha u z r₂

Lemma lem:monotonicity of paper/ckn.tex for the velocity energy alpha: α(z,r₁) ≤ (r₂/r₁)^{1/2} α(z,r₂). The hypothesis hfin records that the time-slice energy at the larger radius is finite, as it is for the suitable weak solutions of the paper.

theorem CKN.beta_mono_radius (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal (spatialGradientSq u Du w) ≠ ⊤) : beta u Du z r₁ ≤ (r₂ / r₁) ^ (1 / 2) * beta u Du z r₂

Lemma lem:monotonicity of paper/ckn.tex for the gradient quantity beta: β(z,r₁) ≤ (r₂/r₁)^{1/2} β(z,r₂).

theorem CKN.gamma_mono_radius (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) : gamma u z r₁ ≤ (r₂ / r₁) ^ (2 / 3) * gamma u z r₂

Lemma lem:monotonicity of paper/ckn.tex for the velocity cubic quantity gamma: γ(z,r₁) ≤ (r₂/r₁)^{2/3} γ(z,r₂).

theorem CKN.delta_sq_mono_radius (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal |p w| ^ (3 / 2) ≠ ⊤) : delta p z r₁ ^ 2 ≤ (r₂ / r₁) ^ (4 / 3) * delta p z r₂ ^ 2

Lemma lem:monotonicity of paper/ckn.tex for the pressure quantity delta, in the squared form stated in the paper: δ(z,r₁)² ≤ (r₂/r₁)^{4/3} δ(z,r₂)².

theorem CKN.lambda_mono_radius (q : ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hq : 0 < q) (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≠ ⊤) : lambda q f z r₁ ≤ (r₁ / r₂) ^ (3 - 5 / q) * lambda q f z r₂

Lemma lem:monotonicity of paper/ckn.tex for the force quantity lambda: for q > 0, λ(z,r₁) ≤ (r₁/r₂)^{3-5/q} λ(z,r₂). Here 3 - 5/q is the exponent σ appearing in the paper.