Documentation Verification Report

Bounds

📁 Source: Mathlib/Analysis/Real/Pi/Bounds.lean

Statistics

Metric	Count
Definitions `«tacticPi_lower_bound[_,,]»`, `«tacticPi_upper_bound[_,,]»`	2
Theorems `ceil_pi_eq_four`, `floor_pi_eq_three`, `pi_gt_d2`, `pi_gt_d20`, `pi_gt_d4`, `pi_gt_d6`, `pi_gt_sqrtTwoAddSeries`, `pi_gt_three`, `pi_lower_bound_start`, `pi_lt_d2`, `pi_lt_d20`, `pi_lt_d4`, `pi_lt_d6`, `pi_lt_four`, `pi_lt_sqrtTwoAddSeries`, `pi_upper_bound_start`, `round_pi_eq_three`, `sqrtTwoAddSeries_step_down`, `sqrtTwoAddSeries_step_up`	19
Total	21

Real

Definitions

Name	Category	Theorems
`«tacticPi_lower_bound[_,,]»` 📖	CompOp	—
`«tacticPi_upper_bound[_,,]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ceil_pi_eq_four` 📖	mathematical	—	`Int.ceil` `Real` `instRing` `linearOrder` `instFloorRing` `pi`	—	`Int.ceil_eq_iff` `Nat.cast_one` `Int.cast_one` `pi_gt_three` `LT.lt.le` `Nat.instAtLeastTwoHAddOfNat` `pi_lt_four`
`floor_pi_eq_three` 📖	mathematical	—	`Int.floor` `Real` `instRing` `linearOrder` `instFloorRing` `pi`	—	`Int.floor_eq_iff` `LT.lt.le` `Nat.instAtLeastTwoHAddOfNat` `pi_gt_three` `Nat.cast_one` `Int.cast_one` `Int.cast_natCast` `pi_lt_four`
`pi_gt_d2` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `pi`	—	`pi_lower_bound_start` `sqrtTwoAddSeries_step_up` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add`
`pi_gt_d20` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `pi`	—	`pi_lower_bound_start` `sqrtTwoAddSeries_step_up` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add`
`pi_gt_d4` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `pi`	—	`pi_lower_bound_start` `sqrtTwoAddSeries_step_up` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add`
`pi_gt_d6` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `pi`	—	`pi_lower_bound_start` `sqrtTwoAddSeries_step_up` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add`
`pi_gt_sqrtTwoAddSeries` 📖	mathematical	—	`Real` `instLT` `instMul` `Monoid.toNatPow` `instMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `sqrt` `instSub` `sqrtTwoAddSeries` `instZero` `pi`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instZeroLEOneClass` `Mathlib.Meta.NormNum.isNat_lt_true` `instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `sin_pi_over_two_pow_succ` `sin_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `pi_pos` `lt_of_le_of_lt` `le_of_eq` `pow_succ'` `mul_assoc` `div_mul_cancel₀` `mul_comm`
`pi_gt_three` 📖	mathematical	—	`Real` `instLT` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `pi`	—	`pi_lower_bound_start` `Nat.instAtLeastTwoHAddOfNat` `sqrtTwoAddSeries_step_up` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add`
`pi_lower_bound_start` 📖	mathematical	`Real` `instLE` `sqrtTwoAddSeries` `DivInvMonoid.toDiv` `instDivInvMonoid` `instNatCast` `instSub` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `instMonoid`	`instLT` `pi`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_of_le_of_lt` `mul_comm` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instZeroLEOneClass` `instIsOrderedRing` `instNontrivial` `le_sqrt_of_sq_le` `le_sub_comm` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Nat.cast_zero` `zero_div` `pi_gt_sqrtTwoAddSeries`
`pi_lt_d2` 📖	mathematical	—	`Real` `instLT` `pi` `NNRatCast.toOfScientific` `instNNRatCast`	—	`pi_upper_bound_start` `sqrtTwoAddSeries_step_down` `Nat.instAtLeastTwoHAddOfNat` `one_div` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one`
`pi_lt_d20` 📖	mathematical	—	`Real` `instLT` `pi` `NNRatCast.toOfScientific` `instNNRatCast`	—	`pi_upper_bound_start` `sqrtTwoAddSeries_step_down` `Nat.instAtLeastTwoHAddOfNat` `one_div` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one`
`pi_lt_d4` 📖	mathematical	—	`Real` `instLT` `pi` `NNRatCast.toOfScientific` `instNNRatCast`	—	`pi_upper_bound_start` `sqrtTwoAddSeries_step_down` `Nat.instAtLeastTwoHAddOfNat` `one_div` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one`
`pi_lt_d6` 📖	mathematical	—	`Real` `instLT` `pi` `NNRatCast.toOfScientific` `instNNRatCast`	—	`pi_upper_bound_start` `sqrtTwoAddSeries_step_down` `Nat.instAtLeastTwoHAddOfNat` `one_div` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one`
`pi_lt_four` 📖	mathematical	—	`Real` `instLT` `pi` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`pi_upper_bound_start` `Nat.instAtLeastTwoHAddOfNat` `sqrtTwoAddSeries_step_down` `pow_one` `one_div` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one` `Mathlib.Meta.NormNum.natPow_one`
`pi_lt_sqrtTwoAddSeries` 📖	mathematical	—	`Real` `instLT` `pi` `instAdd` `instMul` `Monoid.toNatPow` `instMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `sqrt` `instSub` `sqrtTwoAddSeries` `instZero` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `IsStrictOrderedRing.toPosMulStrictMono` `instIsOrderedRing` `instNontrivial` `sin_pi_over_two_pow_succ` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `sub_lt_comm` `sin_gt_sub_cube` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `pi_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `div_le_one_of_le₀` `instZeroLEOneClass` `pi_le_four` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `pow_le_pow_right₀` `IsOrderedRing.toPosMulMono` `Mathlib.Meta.NormNum.isNat_le_true` `Nat.cast_one` `add_le_add_left` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `Nat.instCanonicallyOrderedAdd` `le_of_lt` `div_le_div_of_nonneg_right` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `add_comm` `pow_add` `div_mul_eq_div_div` `one_div` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `inv_pow` `lt_of_lt_of_le` `le_of_eq` `add_mul` `Distrib.rightDistribClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.pow_one_cast` `div_div` `inv_mul_eq_iff_eq_mul₀` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.instCharZero` `Nat.cast_zero` `mul_inv_eq_iff_eq_mul₀` `add_assoc` `mul_comm`
`pi_upper_bound_start` 📖	mathematical	`Real` `instLE` `instSub` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `instMonoid` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `sqrtTwoAddSeries`	`instLT` `pi`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_of_lt_of_le` `pi_lt_sqrtTwoAddSeries` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `le_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `pow_pos` `instZeroLEOneClass` `zero_lt_two` `NeZero.charZero_one` `RCLike.charZero_rclike` `sqrt_le_left` `div_nonneg` `sub_nonneg` `pow_nonneg` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `le_of_lt` `sub_le_comm` `zero_div` `Nat.cast_zero`
`round_pi_eq_three` 📖	mathematical	—	`round` `Real` `instRing` `linearOrder` `instFloorRing` `pi`	—	`Nat.instAtLeastTwoHAddOfNat` `round_eq` `instIsStrictOrderedRing` `Int.floor_eq_iff` `lt_imp_lt_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `le_of_lt` `pi_lt_d2` `le_refl` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_add`
`sqrtTwoAddSeries_step_down` 📖	—	`Real` `instLE` `sqrtTwoAddSeries` `DivInvMonoid.toDiv` `instDivInvMonoid` `instNatCast` `Monoid.toNatPow` `Nat.instMonoid`	—	—	`le_trans` `Nat.instAtLeastTwoHAddOfNat` `sqrtTwoAddSeries_succ` `sqrtTwoAddSeries_monotone_left` `le_sqrt_of_sq_le` `Nat.cast_pos` `instIsOrderedRing` `instNontrivial` `div_pow` `add_div_eq_mul_add_div` `ne_of_gt` `div_le_div_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `pow_pos` `instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `RCLike.charZero_rclike`
`sqrtTwoAddSeries_step_up` 📖	—	`Real` `instLE` `sqrtTwoAddSeries` `DivInvMonoid.toDiv` `instDivInvMonoid` `instNatCast` `Monoid.toNatPow` `Nat.instMonoid`	—	—	`le_trans` `Nat.instAtLeastTwoHAddOfNat` `sqrtTwoAddSeries_succ` `sqrtTwoAddSeries_monotone_left` `Nat.cast_pos` `instIsOrderedRing` `instNontrivial` `sqrt_le_left` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `Nat.cast_nonneg` `div_pow` `add_div_eq_mul_add_div` `ne_of_gt` `div_le_div_iff₀` `pow_pos` `instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `RCLike.charZero_rclike`

---

← Back to Index