Normalizing the final introspection error

The paper's final soundness estimate absorbs any fixed concave power and constant multiple into a * (x^a * ε^b + x^(-b)). The coefficient and the new exponent are explicit here, including the normalization a ≥ 1, 0 < b ≤ 1. No induction estimate is assumed or encoded by the definitions in this file.

noncomputable def MIPRE.Introspection.errorProfile (a b x ε : ℝ) : ℝ

The two terms of the introspection soundness loss, with x = λ n.

Equations

• MIPRE.Introspection.errorProfile a b x ε = a * (x ^ a * ε ^ b + x ^ (-b))

theorem MIPRE.Introspection.errorProfile_nonneg {a b x ε : ℝ} (ha : 0 ≤ a) (hx : 0 ≤ x) (hε : 0 ≤ ε) : 0 ≤ errorProfile a b x ε

noncomputable def MIPRE.Introspection.powerCoefficient (C a r : ℝ) : ℝ

The coefficient prescribed by the paper, enlarged also to be at least one.

Equations

• MIPRE.Introspection.powerCoefficient C a r = max 1 (max (C * a ^ r) (a * r))

theorem MIPRE.Introspection.one_le_powerCoefficient (C a r : ℝ) : 1 ≤ powerCoefficient C a r

theorem MIPRE.Introspection.mul_rpow_le_powerCoefficient (C a r : ℝ) : C * a ^ r ≤ powerCoefficient C a r

theorem MIPRE.Introspection.mul_le_powerCoefficient (C a r : ℝ) : a * r ≤ powerCoefficient C a r

theorem MIPRE.Introspection.errorProfile_power {C a b r x ε : ℝ} (hC : 0 ≤ C) (ha : 0 ≤ a) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hx : 1 ≤ x) (hε : 0 ≤ ε) : C * errorProfile a b x ε ^ r ≤ errorProfile (powerCoefficient C a r) (b * r) x ε

A fixed concave power of the original soundness profile has the required final shape.

theorem MIPRE.Introspection.power_exponent_bounds {b r : ℝ} (hb0 : 0 < b) (hb1 : b ≤ 1) (hr0 : 0 < r) (hr1 : r ≤ 1) : 0 < b * r ∧ b * r ≤ 1

The new exponent is positive and at most one whenever the input exponent and power are.

theorem MIPRE.Introspection.exists_errorProfile_power {C a b r : ℝ} (hC : 0 ≤ C) (ha : 0 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) (hr0 : 0 < r) (hr1 : r ≤ 1) : ∃ (a' : ℝ) (b' : ℝ), 1 ≤ a' ∧ 0 < b' ∧ b' ≤ 1 ∧ ∀ (x ε : ℝ), 1 ≤ x → 0 ≤ ε → C * errorProfile a b x ε ^ r ≤ errorProfile a' b' x ε

Final error absorption, with all constants independent of x and ε.

noncomputable def MIPRE.Introspection.rootExponent (k : ℕ) : ℝ

The exponent after k square roots.

Equations

• MIPRE.Introspection.rootExponent k = (1 / 2) ^ k

theorem MIPRE.Introspection.rootExponent_pos (k : ℕ) : 0 < rootExponent k

theorem MIPRE.Introspection.rootExponent_le_one (k : ℕ) : rootExponent k ≤ 1

def MIPRE.Introspection.iteratedRoot : ℕ → ℝ → ℝ

Applying the square root a fixed finite number of times.

Equations

• MIPRE.Introspection.iteratedRoot 0 x✝ = x✝
• MIPRE.Introspection.iteratedRoot k.succ x✝ = √(MIPRE.Introspection.iteratedRoot k x✝)

theorem MIPRE.Introspection.iteratedRoot_eq_rpow (k : ℕ) {t : ℝ} (ht : 0 ≤ t) : iteratedRoot k t = t ^ rootExponent k

theorem MIPRE.Introspection.errorProfile_iteratedRoot {C a b x ε : ℝ} (k : ℕ) (hC : 0 ≤ C) (ha : 0 ≤ a) (hx : 1 ≤ x) (hε : 0 ≤ ε) : C * iteratedRoot k (errorProfile a b x ε) ≤ errorProfile (powerCoefficient C a (rootExponent k)) (b * rootExponent k) x ε

Every fixed stack of square roots is absorbed with explicit exponent b / 2^k.

theorem MIPRE.Introspection.errorProfile_power_of_le {C a b r x ε δ : ℝ} (hC : 0 ≤ C) (ha : 0 ≤ a) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hx : 1 ≤ x) (hε : 0 ≤ ε) (hδ0 : 0 ≤ δ) (hδ : δ ≤ errorProfile a b x ε) : C * δ ^ r ≤ errorProfile (powerCoefficient C a r) (b * r) x ε

A previously proved loss bound can be inserted into the fixed power estimate.

theorem MIPRE.Introspection.errorProfile_scale_input {a b c x ε : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hx : 0 ≤ x) (hε : 0 ≤ ε) : errorProfile a b x (c * ε) ≤ max 1 (c ^ b) * errorProfile a b x ε

Scaling the test error, as happens in detyping, changes only a fixed coefficient.

theorem MIPRE.Introspection.errorProfile_scaled_power {C a b c r x ε : ℝ} (hC : 0 ≤ C) (ha : 0 ≤ a) (hc : 0 ≤ c) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hx : 1 ≤ x) (hε : 0 ≤ ε) : C * errorProfile a b x (c * ε) ^ r ≤ errorProfile (powerCoefficient (C * max 1 (c ^ b) ^ r) a r) (b * r) x ε

Constant rescaling of the input error followed by a concave power is absorbed too.

theorem MIPRE.Introspection.state_transfer_loss_le_three_sqrt {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) : δ + 2 * √δ ≤ 3 * √δ

The state replacement cost used at the end of soundness remains a square-root loss.