Canonical scalar scales in the Section 2 regularity induction.

def AVenhance.Infra.Construction.section2Radius {β : ℝ} (I : Ingredients β) : ℕ → ℝ

The radius sequence in e.recurrence, with its source initial value.

Equations

• AVenhance.Infra.Construction.section2Radius I 0 = 1
• AVenhance.Infra.Construction.section2Radius I m.succ = 9 / 4 * AVenhance.Infra.Construction.section2Radius I m + 2 ^ 7 * (AVenhance.epsilon β I.Λ (m + 1))⁻¹

def AVenhance.Infra.Construction.section2Amplitude {β : ℝ} (I : Ingredients β) : ℕ → ℝ

The amplitude sequence in e.recurrence, with its source initial value.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Construction.section2Amplitude I 0 = 1

theorem AVenhance.Infra.Construction.section2Scales_canonical {β : ℝ} (I : Ingredients β) : Section2Scales I (section2Radius I) (section2Amplitude I)

The source-defined radius and amplitude sequences satisfy the induction scale data used by the stream-regularity proof.