The actual piecewise amplitude weights in l.V and their squared ratios. The theta base prefactor is handled by a common prefactor outside these weights; the weights themselves are the printed A_i.

noncomputable def AVenhance.Infra.Section4.iterateAmplitude (η : ℝ) (i : ℕ) : ℝ

The source amplitude, with eta its smallness parameter.

Equations

• AVenhance.Infra.Section4.iterateAmplitude η i = if i = 0 then 1 else if i ≤ 2 then η else η ^ (↑i / 2)

def AVenhance.Infra.Section4.iterateAmplitudeSq (η : ℝ) (i : ℕ) : ℝ

Squaring removes fractional powers from the induction bookkeeping.

Equations

• AVenhance.Infra.Section4.iterateAmplitudeSq η i = if i = 0 then 1 else if i ≤ 2 then η ^ 2 else η ^ i

theorem AVenhance.Infra.Section4.iterateAmplitude_square {η : ℝ} (hη : 0 ≤ η) (i : ℕ) : iterateAmplitude η i ^ 2 = iterateAmplitudeSq η i

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_pos {η : ℝ} (hη : 0 < η) (i : ℕ) : 0 < iterateAmplitudeSq η i

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_previous {η : ℝ} (hη1 : η ≤ 1) {i : ℕ} (hi : 2 ≤ i) : η * iterateAmplitudeSq η (i - 1) ≤ iterateAmplitudeSq η i

The preceding-increment material term costs one power of eta for i≥2.

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_two_previous {η : ℝ} (hη : 0 ≤ η) (hη1 : η ≤ 1) {i : ℕ} (hi : 2 ≤ i) : η ^ 2 * iterateAmplitudeSq η (i - 2) ≤ iterateAmplitudeSq η i

Two-increment terms cost two powers of eta; the exceptional early amplitudes are handled explicitly rather than replaced by a uniform power.

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_scaled_previous_ratio {C₀ ρ : ℝ} (hC : 0 < C₀) (hρ : 0 < ρ) (hsmall : C₀ * ρ ≤ 1) {i : ℕ} (hi : 2 ≤ i) : ρ * iterateAmplitudeSq (C₀ * ρ) (i - 1) / iterateAmplitudeSq (C₀ * ρ) i ≤ C₀⁻¹

Normalization of the one-increment material remainder for eta=C0*rho.

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_scaled_two_previous_ratio {C₀ ρ : ℝ} (hC : 0 < C₀) (hρ : 0 < ρ) (hsmall : C₀ * ρ ≤ 1) {i : ℕ} (hi : 2 ≤ i) : ρ ^ 2 * iterateAmplitudeSq (C₀ * ρ) (i - 2) / iterateAmplitudeSq (C₀ * ρ) i ≤ (C₀ ^ 2)⁻¹

Normalization of the two-increment material remainder, including i=2.

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_squared_previous {η : ℝ} (hη : 0 ≤ η) (hη1 : η ≤ 1) {i : ℕ} (hi : 1 ≤ i) : η ^ 2 * iterateAmplitudeSq η (i - 1) ≤ iterateAmplitudeSq η i

A squared gain controls the preceding amplitude even for the exceptional first increment. This is the gain furnished by the material estimates.

theorem AVenhance.Infra.Section4.iterateAmplitudeSq_scaled_squared_previous_ratio {C₀ ρ : ℝ} (hC : 0 < C₀) (hρ : 0 < ρ) (hsmall : C₀ * ρ ≤ 1) {i : ℕ} (hi : 1 ≤ i) : ρ ^ 2 * iterateAmplitudeSq (C₀ * ρ) (i - 1) / iterateAmplitudeSq (C₀ * ρ) i ≤ (C₀ ^ 2)⁻¹

Squared material smallness normalizes with C^-2 at every positive increment, preserving the exceptional first two source amplitudes.