EvenCorrection.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Endpoint control for the even-degree correction in the circuit rank estimate.

theorem OAI.Problem335.convexOn_affine_sub_log line 13
Source documentation
The logarithm of an exponential divided by its positive argument is convex.
```
theorem convexOn_affine_sub_log (A B : ℝ) :
    ConvexOn ℝ (Ioi 0) (fun x : ℝ => A * x + B - Real.log x) := by
…
```
theorem OAI.Problem335.rpow_affine_div_le_max_endpoints line 25
Source documentation
The quotient occurring in the even-degree error is bounded by its two endpoint values. No smallness assumption on q is needed for this fact.
```
theorem rpow_affine_div_le_max_endpoints {q a b z c : ℝ}
    (hq : 0 < q) (ha : 0 < a) (haz : a ≤ z) (hzb : z ≤ b) :
    q ^ (1 - c * z) / z ≤
      max (q ^ (1 - c * a) / a) (q ^ (1 - c * b) / b) := by
…
```

theorem OAI.Problem335.sum_rpow_affine_le_endpoint_mul_sum line 45

Source documentation

Summing the endpoint estimate charges each term by its degree, rather than by the number of factors. This avoids a constant loss per even degree.

theorem sum_rpow_affine_le_endpoint_mul_sum {ι : Type*} (s : Finset ι)
    (d : ι → ℝ) {q a b c : ℝ} (hq : 0 < q) (ha : 0 < a)
    (hd : ∀ i ∈ s, a ≤ d i ∧ d i ≤ b) :
    (∑ i ∈ s, q ^ (1 - c * d i)) ≤
      max (q ^ (1 - c * a) / a) (q ^ (1 - c * b) / b) * ∑ i ∈ s, d i := by
…

theorem OAI.Problem335.sum_rpow_affine_le_endpoint_mul line 59

Source documentation

A total degree bound turns the preceding weighted estimate into a bound independent of the number of terms.

theorem sum_rpow_affine_le_endpoint_mul {ι : Type*} (s : Finset ι)
    (d : ι → ℝ) {q a b c N : ℝ} (hq : 0 < q) (ha : 0 < a)
    (hd : ∀ i ∈ s, a ≤ d i ∧ d i ≤ b) (hs : (∑ i ∈ s, d i) ≤ N) :
    (∑ i ∈ s, q ^ (1 - c * d i)) ≤
      max (q ^ (1 - c * a) / a) (q ^ (1 - c * b) / b) * N := by
…

theorem OAI.Problem335.sum_rpow_affine_le_mul_sqrt line 70

Source documentation

The exact square-root error bound needed after estimating the two endpoint quotients by C / sqrt N.

theorem sum_rpow_affine_le_mul_sqrt {ι : Type*} (s : Finset ι)
    (d : ι → ℝ) {q a b c N C : ℝ} (hq : 0 < q) (ha : 0 < a)
    (hN : 0 < N) (hd : ∀ i ∈ s, a ≤ d i ∧ d i ≤ b)
    (hs : (∑ i ∈ s, d i) ≤ N)
    (hleft : q ^ (1 - c * a) / a ≤ C / Real.sqrt N)
    (hright : q ^ (1 - c * b) / b ≤ C / Real.sqrt N) :
    (∑ i ∈ s, q ^ (1 - c * d i)) ≤ C * Real.sqrt N := by
…

theorem OAI.Problem335.evenCorrection_left_endpoint line 89

Source documentation

The left endpoint correction is uniformly bounded.

theorem evenCorrection_left_endpoint {N s q : ℝ} (hN : 0 < N)
    (hs : 0 ≤ s) (hsN : s ≤ Real.sqrt N)
    (hqlo : (Real.sqrt N)⁻¹ ≤ q) (hqhi : q ≤ 2 / Real.sqrt N) :
    q ^ (1 - (s / N) * 2) / 2 ≤ Real.exp 2 / Real.sqrt N := by
…

theorem OAI.Problem335.evenCorrection_right_endpoint line 121

Source documentation

The right endpoint correction needs only q ≤ 1.

theorem evenCorrection_right_endpoint {N s q : ℝ} (hN : 0 < N)
    (hs : 0 < s) (hsN : s ≤ Real.sqrt N) (hq : 0 ≤ q) (hqone : q ≤ 1) :
    q ^ (1 - (s / N) * (N / (4 * s))) / (N / (4 * s)) ≤
      4 / Real.sqrt N := by
…

theorem OAI.Problem335.evenCorrection_sum_bound line 141

Source documentation

An explicit uniform square-root bound for the sum of all low-even-degree corrections. Only the numerical range of degrees is needed, not their parity.

theorem evenCorrection_sum_bound {ι : Type*} (I : Finset ι) (d : ι → ℝ)
    {N s q : ℝ} (hN : 0 < N) (hs : 0 < s) (hsN : s ≤ Real.sqrt N)
    (hqlo : (Real.sqrt N)⁻¹ ≤ q) (hqhi : q ≤ 2 / Real.sqrt N) (hqone : q ≤ 1)
    (hd : ∀ i ∈ I, 2 ≤ d i ∧ d i ≤ N / (4 * s))
    (hdsum : (∑ i ∈ I, d i) ≤ N) :
    (∑ i ∈ I, q ^ (1 - (s / N) * d i)) ≤
      (Real.exp 2 + 4) * Real.sqrt N := by
…

theorem OAI.Problem335.sum_low_even_corrections line 160

Source documentation

The correction bound specialized to the low even members of a list of positive integer degrees with bounded total degree.

theorem sum_low_even_corrections {ι : Type*} (I : Finset ι) (e : ι → ℕ)
    {N s q : ℝ} (hN : 0 < N) (hs : 0 < s) (hsN : s ≤ Real.sqrt N)
    (hqlo : (Real.sqrt N)⁻¹ ≤ q) (hqhi : q ≤ 2 / Real.sqrt N) (hqone : q ≤ 1)
    (he : ∀ i ∈ I, 0 < e i) (hsum : (∑ i ∈ I, (e i : ℝ)) ≤ N) :
    (∑ i ∈ I, if Even (e i) ∧ (e i : ℝ) < N / (4 * s)
      then 4 * q ^ (1 - (s / N) * e i) else 0) ≤
      (4 * (Real.exp 2 + 4)) * Real.sqrt N := by
…