ReciprocalPhasePreparation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.reciprocal_second_derivative_comparison line 10

Source documentation

The exact scale normalization used in the second derivative test.

theorem reciprocal_second_derivative_comparison (hs : List ℝ)
    (hhs : ∀ h ∈ hs, 0 < h) (Z : ℝ) {U x : ℝ}
    (hU : 0 < U) (hx : U ≤ x) (hxend : x + hs.sum ≤ 2 * U) :
    let k := hs.length + 2
…

theorem OAI.Problem337.reciprocal_terminal_error_bound line 34

Source documentation

Scalar terminal estimate for a second-derivative bound.

theorem reciprocal_terminal_error_bound {U a b Λ : ℝ} (hU : 1 ≤ U)
    (ha : 0 < a) (hb : 0 ≤ b)
    (hlower : a * U ^ (-(3 : ℝ) / 2) ≤ Λ)
    (hupper : Λ ≤ b * U ^ (-(2 : ℝ) / 5)) :
    U * Λ ^ ((1 : ℝ) / 2) + Λ ^ (-(1 : ℝ) / 2) + 1 ≤
      (b ^ ((1 : ℝ) / 2) + a ^ (-(1 : ℝ) / 2) + 1) * U ^ ((4 : ℝ) / 5) := by
…

theorem OAI.Problem337.reciprocal_second_derivative_comparison_general line 69
Source documentation
Flexible range factor in the normalized second-derivative comparison. Taking C=3 or C=4 accommodates endpoint samples without dropping terms.
```
theorem reciprocal_second_derivative_comparison_general (hs : List ℝ)
    (hhs : ∀ h ∈ hs, 0 < h) (Z C : ℝ) {U x : ℝ}
    (hU : 0 < U) (hx : U ≤ x) (hxend : x + hs.sum ≤ C * U) :
    let k := hs.length + 2
…
```