Theorems · Theorem · real analysis
Real.sqrtTwoAddSeries_step_up
∀ (c d : ℕ) {a b n : ℕ} {z : ℝ},
(↑c / ↑d).sqrtTwoAddSeries n ≤ z →
0 < b → 0 < d → (2 * b + a) * d ^ 2 ≤ c ^ 2 * b → (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z- Defined in
- Mathlib.Analysis.Real.Pi.Bounds
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- le_transproof · cited by 985
- ne_of_gtproof · cited by 637
- pow_posproof · cited by 292
- Nat.cast_posproof · cited by 113
- Nat.cast_nonnegproof · cited by 109
- div_nonnegproof · cited by 103
- div_powproof · cited by 66
- Real.sqrtTwoAddSeriesstatement and proof · cited by 19
- div_le_div_iff₀proof · cited by 11
- Real.sqrt_le_leftproof · cited by 9
- add_div_eq_mul_add_divproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- Real.pi_gt_threeproof · cited by 6
- Real.pi_gt_d2proof · cited by 0
- Real.pi_gt_d20proof · cited by 0
- Real.pi_gt_d4proof · cited by 0
- Real.pi_gt_d6proof · cited by 0