Scalar two-level geometric amortization for the guarded controller

These lemmas are deliberately independent of the executable controller. They are the numerical engine used below: an inner radius-doubling geometric sum is paid by its last radius, and the outer scale-doubling sum is paid by its last scale. In particular no estimate of the form "number of trials times the last trial" occurs.

noncomputable def O3.WrapperExponent (p : ℝ) : ℝ

The exponent in all three wrapper regimes is strictly positive.

Equations

• O3.WrapperExponent p = if p ≤ 2 then 1 / 2 else O3.aboveAlpha p

theorem O3.wrapperExponent_pos {p : ℝ} : 0 < WrapperExponent p

noncomputable def O3.geometricAmortizationConstant (a : ℝ) : ℝ

A convenient geometric-amortization coefficient.

Equations

• O3.geometricAmortizationConstant a = 2 ^ a / (2 ^ a - 1)

theorem O3.two_rpow_gt_one {a : ℝ} (ha : 0 < a) : 1 < 2 ^ a

theorem O3.geometricAmortizationConstant_pos {a : ℝ} (ha : 0 < a) : 0 < geometricAmortizationConstant a

theorem O3.radius_geometric_sum_le_endpoint {a beta : ℝ} (ha : 0 < a) (hbeta : 0 ≤ beta) (J : ℕ) : ∑ j ∈ Finset.range (J + 1), (2 ^ j * beta) ^ a ≤ geometricAmortizationConstant a * (2 ^ J * beta) ^ a

Exact finite inner geometric summation, expressed through its endpoint.

theorem O3.scale_geometric_sum_le_endpoint {a k0 : ℝ} (ha : 0 < a) (hk0 : 0 ≤ k0) (S : ℕ) : ∑ s ∈ Finset.range (S + 1), (2 ^ s * k0) ^ a ≤ geometricAmortizationConstant a * (2 ^ S * k0) ^ a

The same genuine geometric sum across scale epochs.

noncomputable def O3.euclideanWrapperWeight (x : ℝ) : ℝ

The square-root cost weight used in the Euclidean controller analysis.

Equations

• O3.euclideanWrapperWeight x = √x

noncomputable def O3.aboveWrapperWeight (a x : ℝ) : ℝ

The power-law cost weight used for exponents above two.

Equations

• O3.aboveWrapperWeight a x = x ^ a

noncomputable def O3.belowWrapperWeight (x : ℝ) : ℝ

The square-root logarithmic cost weight used for exponents below two.

Equations

• O3.belowWrapperWeight x = √x * Real.log (Real.exp 1 + x)