The algebraic combination step of the combined decay inequality

This file formalizes the purely algebraic step in the proof of lem:theta-decay of paper/ckn.tex, the "Combined decay inequality". The paper combines three analytic estimates into the one-step decay of the combined quantity

θ(z,ρ) = α(z,ρ) + β(z,ρ) + κ⁻⁴δ(z,ρ)² (eq:theta)

at the smaller radius κρ, where κ ∈ (0,1/2] is the scale ratio. The three inputs, each carried here as a hypothesis, are the Caccioppoli inequality eq:caccioppoli, the pressure decay estimate eq:pressure-decay of thm:pressure-decay, and the Gagliardo–Nirenberg inequality eq:gagliardo of cor:gagliardo.

The conclusions formalized are the two displayed inequalities eq:theta-decay-1 and eq:theta-decay-2 of the lemma:

θ(κρ) ≤ C₂₇ κ^{2/3} θ(ρ) + C₂₇ κ^{-5}(β(ρ)^{1/2} + β(ρ)) θ(ρ) + C₂₈ κ^{-1/2} θ(ρ)^{1/2} λ(ρ)^{1/2} + C₂₈ κ^{-3} λ(ρ),

and, when θ(ρ) ≤ 1, the same with β(ρ)^{1/2} + β(ρ) replaced by 2 θ(ρ)^{1/2}. The constants C₂₇ and C₂₈ are the explicit combinations thetaDecayC₂₇ and thetaDecayC₂₈ of the input constants C₉, C₁₄, C₁₅, C₂₅, C₂₆ displayed at the end of the paper's proof.

No analytic content enters: every step is an elementary real inequality, using √β ≤ √θ from β ≤ θ, δ ≤ κ²√θ from κ⁻⁴δ² ≤ θ, the Young-type square-root bounds for √γ, and the power comparisons κ ≤ κ^{2/3} and κ⁻¹ ≤ κ^{-5} valid for 0 < κ ≤ 1/2.

The quantity and the constants of lem:theta-decay

noncomputable def CKN.thetaValue (κ α β δ : ℝ) : ℝ

The combined quantity θ = α + β + κ⁻⁴δ² of eq:theta.

The fourth power of the scale ratio enters as κ ^ (-4 : ℝ) so that the statement is uniform with the remaining real powers of κ in the decay estimates; for κ > 0 this is the paper's κ⁻⁴.

Equations

• CKN.thetaValue κ α β δ = α + β + κ ^ (-4) * δ ^ 2

noncomputable def CKN.thetaDecayC₂₇ (C₉ C₁₄ C₂₅ : ℝ) : ℝ

The absolute constant C₂₇ of eq:theta-decay-1, in terms of the input constants C₉ (Gagliardo–Nirenberg), C₁₄ (pressure) and C₂₅ (Caccioppoli): the paper's 3C₁₄² + C₂₅(1 + 2C₉^{1/2}) + 2C₂₅C₉^{1/2}.

Equations

• CKN.thetaDecayC₂₇ C₉ C₁₄ C₂₅ = 3 * C₁₄ ^ 2 + C₂₅ * (1 + 2 * √C₉) + 2 * C₂₅ * √C₉

noncomputable def CKN.thetaDecayC₂₈ (C₉ C₁₅ C₂₆ : ℝ) : ℝ

The constant C₂₈ = C₂₈(q) of eq:theta-decay-1, in terms of C₉, C₁₅ (pressure) and C₂₆ (Caccioppoli): the paper's 3C₁₅² + 2C₂₆C₉^{1/2}.

Equations

• CKN.thetaDecayC₂₈ C₉ C₁₅ C₂₆ = 3 * C₁₅ ^ 2 + 2 * C₂₆ * √C₉

Elementary real inequalities

The combination step

theorem CKN.thetaDecay_algebra {κ C₉ C₁₄ C₁₅ C₂₅ C₂₆ α β γ δ lam αr βr δr : ℝ} (hκ : 0 < κ) (hκhalf : κ ≤ 1 / 2) (hC₉ : 0 ≤ C₉) (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hlam : 0 ≤ lam) (hδr : 0 ≤ δr) (hA : αr + βr ≤ C₂₅ * κ * α + C₂₅ * κ⁻¹ * √α * √β * √γ + C₂₅ * κ⁻¹ * δ * √γ + C₂₆ * κ ^ (-1 / 2) * √γ * √lam) (hB : δr ≤ C₁₄ * κ ^ (-1 / 2) * √α * √β + C₁₄ * κ ^ (1 / 3) * δ + C₁₅ * κ ^ (1 / 2) * √lam) (hC : γ ≤ C₉ * √α * √β + C₉ * α) : thetaValue κ αr βr δr ≤ thetaDecayC₂₇ C₉ C₁₄ C₂₅ * κ ^ (2 / 3) * thetaValue κ α β δ + thetaDecayC₂₇ C₉ C₁₄ C₂₅ * κ ^ (-5) * (√β + β) * thetaValue κ α β δ + thetaDecayC₂₈ C₉ C₁₅ C₂₆ * κ ^ (-1 / 2) * √(thetaValue κ α β δ) * √lam + thetaDecayC₂₈ C₉ C₁₅ C₂₆ * κ ^ (-3) * lam

The combination step of lem:theta-decay. The three analytic inputs of the lemma — the Caccioppoli inequality eq:caccioppoli (constants C₂₅, C₂₆), the pressure decay estimate eq:pressure-decay (constants C₁₄, C₁₅), and the Gagliardo–Nirenberg inequality eq:gagliardo (constant C₉) — together imply the first displayed decay estimate eq:theta-decay-1 for θ = α + β + κ⁻⁴δ² at the ratio κ ∈ (0,1/2].

The hypotheses hA, hB, hC are exactly the paper's (A), (B), (C) at the radii r = κρ (left-hand quantities αr, βr, δr) and ρ (right-hand quantities α, β, γ, δ, λ); the conclusion carries the constants thetaDecayC₂₇ and thetaDecayC₂₈.

theorem CKN.thetaDecay_algebra_small {κ C₉ C₁₄ C₁₅ C₂₅ C₂₆ α β γ δ lam αr βr δr : ℝ} (hκ : 0 < κ) (hκhalf : κ ≤ 1 / 2) (hC₉ : 0 ≤ C₉) (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hlam : 0 ≤ lam) (hδr : 0 ≤ δr) (hθ : thetaValue κ α β δ ≤ 1) (hA : αr + βr ≤ C₂₅ * κ * α + C₂₅ * κ⁻¹ * √α * √β * √γ + C₂₅ * κ⁻¹ * δ * √γ + C₂₆ * κ ^ (-1 / 2) * √γ * √lam) (hB : δr ≤ C₁₄ * κ ^ (-1 / 2) * √α * √β + C₁₄ * κ ^ (1 / 3) * δ + C₁₅ * κ ^ (1 / 2) * √lam) (hC : γ ≤ C₉ * √α * √β + C₉ * α) : thetaValue κ αr βr δr ≤ thetaDecayC₂₇ C₉ C₁₄ C₂₅ * κ ^ (2 / 3) * thetaValue κ α β δ + 2 * thetaDecayC₂₇ C₉ C₁₄ C₂₅ * κ ^ (-5) * √(thetaValue κ α β δ) * thetaValue κ α β δ + thetaDecayC₂₈ C₉ C₁₅ C₂₆ * κ ^ (-1 / 2) * √(thetaValue κ α β δ) * √lam + thetaDecayC₂₈ C₉ C₁₅ C₂₆ * κ ^ (-3) * lam

The small-θ form of the combination step of lem:theta-decay. This is eq:theta-decay-2: under the additional hypothesis θ(ρ) ≤ 1 the second term of thetaDecay_algebra weakens, because β^{1/2} + β ≤ 2θ(ρ)^{1/2}. The analytic inputs hA, hB, hC are the same as in thetaDecay_algebra.