PowerPerturbation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The small change in exponent from one to rho does not destroy the inverse-square-root scale of the rounded operator parameters.

def OAI.Problem335.PowerPerturbation.error line 14
Source documentation
An explicit error that tends to zero.
```
def error (n : ℝ) : ℝ := 2 * Real.log n / Real.sqrt n + 2 / n
```
lemma OAI.Problem335.PowerPerturbation.tendsto_error line 16
lemma OAI.Problem335.PowerPerturbation.eventually_error_le_log_two line 28

lemma OAI.Problem335.PowerPerturbation.rpow_mul_exp_le line 34

Source documentation

Deterministic perturbation estimate, with all rounding and exponent hypotheses explicit. The extra exp (1/n) allows a second ceiling error.

lemma rpow_mul_exp_le {n a e : ℝ} (hn : 1 ≤ n) (ha : 0 < a)
    (haUpper : a ≤ n ^ (-(1 / 2 : ℝ)) * Real.exp (1 / n))
    (he0 : 0 ≤ e) (he1 : e ≤ 1) (hgap : 1 - e ≤ 4 / Real.sqrt n) :
    a ^ e * Real.exp (1 / n) ≤
      n ^ (-(1 / 2 : ℝ)) * Real.exp (error n) := by
…

Mentions: OAI.Problem335.PowerPerturbation.error

lemma OAI.Problem335.PowerPerturbation.rpow_mul_exp_le_two line 60

theorem OAI.Problem335.PowerPerturbation.eventually_rpow_mul_exp_le_two line 76

Source documentation

Uniform in both the rounded parameter and the varying exponent.

theorem eventually_rpow_mul_exp_le_two :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → ∀ a e : ℝ,
      0 < a → a ≤ (n : ℝ) ^ (-(1 / 2 : ℝ)) * Real.exp (1 / (n : ℝ)) →
      0 ≤ e → e ≤ 1 → 1 - e ≤ 4 / Real.sqrt (n : ℝ) →
      a ^ e * Real.exp (1 / (n : ℝ)) ≤ 2 / Real.sqrt (n : ℝ) := by
…

theorem OAI.Problem335.PowerPerturbation.eventually_q_beta_bounds line 90

Source documentation

The exponent used for q is also covered by the uniform estimate.

theorem eventually_q_beta_bounds :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → ∀ a rho beta : ℝ,
      0 < a → a ≤ (n : ℝ) ^ (-(1 / 2 : ℝ)) * Real.exp (1 / (n : ℝ)) →
      0 ≤ rho → rho ≤ 1 → 1 - rho ≤ 4 / Real.sqrt (n : ℝ) →
      beta ≤ a ^ rho * Real.exp (1 / (n : ℝ)) →
      a ^ ((1 + rho) / 2) ≤ 2 / Real.sqrt (n : ℝ) ∧
      beta ≤ 2 / Real.sqrt (n : ℝ) := by
…

lemma OAI.Problem335.PowerPerturbation.inverse_sqrt_le_rpow line 111
theorem OAI.Problem335.PowerPerturbation.eventually_inverse_sqrt_bounds line 125
Source documentation
The inverse-square-root estimate implies both weaker bounds used in the circuit rank analysis after increasing the absolute threshold.
```
theorem eventually_inverse_sqrt_bounds :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
      2 / Real.sqrt (n : ℝ) ≤ (n : ℝ) ^ (-(2 / 5 : ℝ)) ∧
      2 / Real.sqrt (n : ℝ) ≤ 1 / 2 := by
…
```