The standing parameters of Section 5

This file records the numerical choices made once and for all at the start of paper/ckn.tex, Section 5, in the convention conv:step-params with its displayed equation eq:standing:

• the velocity exponent τ₂ = 25/3, the gradient exponent τ₃ with 1/τ₃ = 1/τ₂ + 1/5 by arithmetic from the definitions, and the pressure exponent τ_p = 25/8;
• the integrability parameter σ = 3 - 5/q attached to the force exponent q;
• the Hölder exponent γ₀(q) = min {2 - 5/q, 1/5} of eq:gamma-value;
• the Morrey exponents θ₀, θ₁ of eq:q0q1.

The exponent ε = 2/5 of eq:standing is not redefined here: it is the established constant CKN.iterationEpsilon from CKN.Core.Iteration.Arithmetic. The file proves the numerical inequalities those constants are introduced to supply: 5 < τ₂ and τ₃ > 5/2 (the two inequalities Steps 3 and 4 consume), the bootstrap condition eq:bootstrap-cond at the exponent τ = τ₂ actually used in Corollary cor:one-round, the positivity and upper bound 0 < γ₀(q) ≤ 1/5 for q > 5/2, the lower bound σ > 1 for q > 5/2, and the exponent identities 2 - 5/θ₀ = 1 - 5/θ₁ = γ of eq:q0q1.

The exponents τ₂, τ₃, τ_p of eq:standing

noncomputable def CKN.stepTau₂ : ℝ

The velocity Morrey exponent τ₂ = 5/(1 - ε) = 25/3 of eq:standing; its fixed value is given by stepTau₂, with ε = 2/5 recorded in iterationEpsilon_eq.

Equations

• CKN.stepTau₂ = 25 / 3

noncomputable def CKN.stepTau₃ : ℝ

The gradient Morrey exponent τ₃ of eq:standing, taken at the value τ₃ = 25/8 by stepTau₃; the bootstrap range using its reciprocal is recorded in bootstrap_condition_iff.

Equations

• CKN.stepTau₃ = 25 / 8

noncomputable def CKN.stepTauP : ℝ

The pressure Morrey exponent τ_p = 25/8 of eq:standing, equal to τ₃; see Remark rem:LR-pressure for why it is not consumed downstream.

Equations

• CKN.stepTauP = 25 / 8

noncomputable def CKN.stepVarpi : ℝ

The bootstrap gain ϖ = 1/5 - 1/τ₂ of eq:bootstrap-gain.

Equations

• CKN.stepVarpi = 1 / 5 - 1 / CKN.stepTau₂

theorem CKN.stepVarpi_eq : stepVarpi = iterationEpsilon / 5

eq:bootstrap-gain states ϖ = ε/5 with ε = 2/5.

theorem CKN.stepVarpi_eq_two_twentyfifths : stepVarpi = 2 / 25

The numerical value of the gain: ϖ = 2/25.

theorem CKN.bootstrap_gain_at_tau₂ : 1 / stepTau₂ - stepVarpi = 1 / 25

The gain computation of Corollary cor:one-round: 1/τ₂ - ϖ = 1/25 (the reciprocal of the exponent τ₄ = 25 appearing there).

The parameter σ of eq:standing

noncomputable def CKN.stepSigma (q : ℝ) : ℝ

The integrability parameter σ = 3 - 5/q of eq:standing, a function of the force exponent q.

Equations

• CKN.stepSigma q = 3 - 5 / q

theorem CKN.one_lt_stepSigma {q : ℝ} (hq : 5 / 2 < q) : 1 < stepSigma q

eq:standing records σ = 3 - 5/q > 1 under q > 5/2.

theorem CKN.iterationEpsilon_lt_stepSigma {q : ℝ} (hq : 5 / 2 < q) : iterationEpsilon < stepSigma q

conv:step-params uses ε < σ with ε = 2/5; under q > 5/2 this holds for σ = 3 - 5/q.

The Hölder exponent γ₀ of eq:gamma-value

noncomputable def CKN.stepGamma₀ (q : ℝ) : ℝ

The Hölder exponent γ₀(q) = min {2 - 5/q, 1/5} of eq:gamma-value in Theorem thm:endgame.

Equations

• CKN.stepGamma₀ q = min (2 - 5 / q) (1 / 5)

theorem CKN.stepGamma₀_pos {q : ℝ} (hq : 5 / 2 < q) : 0 < stepGamma₀ q

eq:gamma-value records γ₀ > 0 because q > 5/2.

theorem CKN.stepGamma₀_le_fifth (q : ℝ) : stepGamma₀ q ≤ 1 / 5

The upper bound γ₀(q) ≤ 1/5 of eq:gamma-value.

theorem CKN.stepGamma₀_lt_one (q : ℝ) : stepGamma₀ q < 1

Since γ₀(q) ≤ 1/5 < 1, the Hölder exponent lies in (0,1) when q > 5/2, as prop:heat-morrey-hoelder requires.

The exponents θ₀, θ₁ of eq:q0q1

noncomputable def CKN.stepTheta₀ (γ : ℝ) : ℝ

The Morrey exponent θ₀ = 5/(2 - γ) of eq:q0q1, as a function of the Hölder exponent γ.

Equations

• CKN.stepTheta₀ γ = 5 / (2 - γ)

noncomputable def CKN.stepTheta₁ (γ : ℝ) : ℝ

The Morrey exponent θ₁ = 5/(1 - γ) of eq:q0q1, as a function of the Hölder exponent γ.

Equations

• CKN.stepTheta₁ γ = 5 / (1 - γ)

theorem CKN.stepTheta₀_inv (γ : ℝ) : 1 / stepTheta₀ γ = (2 - γ) / 5

The first identity of eq:q0q1: 1/θ₀ = (2 - γ)/5.

theorem CKN.stepTheta₁_inv (γ : ℝ) : 1 / stepTheta₁ γ = (1 - γ) / 5

The second identity of eq:q0q1: 1/θ₁ = (1 - γ)/5.

theorem CKN.stepTheta₀_gt_half {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) : 5 / 2 < stepTheta₀ γ

eq:q0q1 records θ₀ = 5/(2 - γ) > 5/2 for γ ∈ (0,1).

theorem CKN.stepTheta₁_gt_five {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) : 5 < stepTheta₁ γ

eq:q0q1 records θ₁ = 5/(1 - γ) > 5 for γ ∈ (0,1).