VaughanCutoff.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.Vaughan.optimizedCutoff line 10
Source documentation
The conventional balanced natural cutoff for Vaughan's identity.
```
def optimizedCutoff (X : ℝ) : ℕ := ⌊X ^ (2 / 5 : ℝ)⌋₊
```
theorem OAI.Problem337.Vaughan.optimizedCutoff_le line 12
theorem OAI.Problem337.Vaughan.optimizedCutoff_lower line 16
theorem OAI.Problem337.Vaughan.optimizedCutoff_pos line 22
theorem OAI.Problem337.Vaughan.optimizedCutoff_sq_le line 27
theorem OAI.Problem337.Vaughan.optimizedCutoff_le_four_fifths line 36
theorem OAI.Problem337.Vaughan.div_sqrt_optimizedCutoff_le line 43
Source documentation
The reciprocal square-root loss from a long-variable cutoff has precisely the required four-fifths power, with a harmless explicit constant.
```
theorem div_sqrt_optimizedCutoff_le (X : ℝ) (hX : 0 < X)
    (hpow : 2 ≤ X ^ (2 / 5 : ℝ)) :
    X / Real.sqrt (optimizedCutoff X : ℝ) ≤ 2 * X ^ (4 / 5 : ℝ) := by
…
```
Mentions: OAI.Problem337.Vaughan.optimizedCutoff

theorem OAI.Problem337.Vaughan.optimizedCutoff_error_le line 66

Source documentation

A concrete scalar optimization of the cutoff-dependent error terms.

theorem optimizedCutoff_error_le (X : ℝ) (hX : 1 ≤ X)
    (hpow : 2 ≤ X ^ (2 / 5 : ℝ)) :
    (optimizedCutoff X : ℝ) + (optimizedCutoff X : ℝ) ^ 2 +
        X / Real.sqrt (optimizedCutoff X : ℝ) ≤ 4 * X ^ (4 / 5 : ℝ) := by
…

Mentions: OAI.Problem337.Vaughan.optimizedCutoff

theorem OAI.Problem337.Vaughan.optimizedCutoff_log_le line 76

Source documentation

The short initial segment is also absorbed by the four-fifths budget.

theorem optimizedCutoff_log_le (X : ℝ) (hX : 1 ≤ X)
    (hpow : 2 ≤ X ^ (2 / 5 : ℝ)) :
    (optimizedCutoff X : ℝ) * Real.log (optimizedCutoff X : ℝ) ≤
      X ^ (4 / 5 : ℝ) * Real.log X := by
…

Mentions: OAI.Problem337.Vaughan.optimizedCutoff

theorem OAI.Problem337.Vaughan.optimizedCutoff_standard_envelope line 93

Source documentation

Scalar normalization to the usual three-term Vaughan envelope. The Diophantine denominator only needs the ordinary range 1 ≤ q ≤ X.

theorem optimizedCutoff_standard_envelope (X q : ℝ) (hX : 1 ≤ X)
    (hq : 1 ≤ q) (hqX : q ≤ X) (hpow : 2 ≤ X ^ (2 / 5 : ℝ)) :
    X / q + ((optimizedCutoff X : ℝ) + (optimizedCutoff X : ℝ) ^ 2 +
        X / Real.sqrt (optimizedCutoff X : ℝ)) + q ≤
      4 * (X / Real.sqrt q + X ^ (4 / 5 : ℝ) + Real.sqrt (X * q)) := by
…

Mentions: OAI.Problem337.Vaughan.optimizedCutoff

theorem OAI.Problem337.Vaughan.sqrt_optimizedCutoff_envelope_le line 113

Source documentation

Optimization of the square-root expression arising from a Type II block. Both long-variable cutoffs are the same balanced natural cutoff.

theorem sqrt_optimizedCutoff_envelope_le (X q : ℝ) (hX : 1 ≤ X)
    (hq : 0 < q) (hpow : 2 ≤ X ^ (2 / 5 : ℝ)) :
    Real.sqrt (X * (X / q + X / (optimizedCutoff X : ℝ) +
        X / (optimizedCutoff X : ℝ) + q)) ≤
      3 * (X / Real.sqrt q + X ^ (4 / 5 : ℝ) + Real.sqrt (X * q)) := by
…

Mentions: OAI.Problem337.Vaughan.optimizedCutoff

theorem OAI.Problem337.Vaughan.optimizedCutoff_squared_budget line 142

Source documentation

The precise squared Type II block budget transfers to the standard Vaughan envelope after choosing both cutoffs as optimizedCutoff X.

theorem optimizedCutoff_squared_budget (X q C R : ℝ) (hX : 1 ≤ X)
    (hq : 0 < q) (hC : 0 ≤ C) (hpow : 2 ≤ X ^ (2 / 5 : ℝ))
    (hbound : R ^ 2 ≤ C * X * (1 + Real.log (2 * X)) ^ 6 *
      (X / q + X / (optimizedCutoff X : ℝ) + X / (optimizedCutoff X : ℝ) + q)) :
    R ≤ 3 * Real.sqrt C * (1 + Real.log (2 * X)) ^ 3 *
      (X / Real.sqrt q + X ^ (4 / 5 : ℝ) + Real.sqrt (X * q)) := by
…

Mentions: OAI.Problem337.Vaughan.optimizedCutoff

theorem OAI.Problem337.Vaughan.eventually_optimizedCutoff_bounds line 174

Source documentation

All cutoff inequalities hold simultaneously beyond one real threshold.

theorem eventually_optimizedCutoff_bounds :
    ∀ᶠ X : ℝ in atTop,
      0 < optimizedCutoff X ∧
      X ^ (2 / 5 : ℝ) / 2 ≤ (optimizedCutoff X : ℝ) ∧
      (optimizedCutoff X : ℝ) ≤ X ^ (2 / 5 : ℝ) ∧
      (optimizedCutoff X : ℝ) ^ 2 ≤ X ^ (4 / 5 : ℝ) ∧
      X / Real.sqrt (optimizedCutoff X : ℝ) ≤ 2 * X ^ (4 / 5 : ℝ) := by
…

Mentions: OAI.Problem337.Vaughan.optimizedCutoff