Documentation Verification Report

Bertrand

📁 Source: Mathlib/NumberTheory/Bertrand.lean

Statistics

Metric	Count
Definitions	0
Theorems `real_main_inequality`, `bertrand`, `exists_prime_lt_and_le_two_mul`, `exists_prime_lt_and_le_two_mul_eventually`, `exists_prime_lt_and_le_two_mul_succ`, `bertrand_main_inequality`, `centralBinom_factorization_small`, `centralBinom_le_of_no_bertrand_prime`	8
Total	8

Bertrand

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`real_main_inequality` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.instPow` `Real.sqrt` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `Real.rpow_pos_of_pos` `two_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `four_pos` `zero_lt_two'` `Real.log_div` `LT.lt.ne'` `Real.log_mul` `Real.log_rpow` `zero_lt_four` `mul_div_right_comm` `mul_div` `mul_comm` `lt_of_lt_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `div_le_one` `div_div_eq_mul_div` `Real.rpow_sub` `mul_div_left_comm` `mul_one_sub` `Mathlib.Meta.NormNum.isNNRat_eq_true` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `mul_one_div` `Real.log_nonpos_iff` `LT.lt.le` `ConcaveOn.sub` `ConcaveOn.add` `ConcaveOn.subset` `StrictConcaveOn.concaveOn` `strictConcaveOn_log_Ioi` `Set.Ioi_subset_Ioi` `Mathlib.Meta.NormNum.isRat_le_true` `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.natPow_one` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero` `convex_Ioi` `Real.instIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule` `Algebra.to_smulCommClass` `Set.ext` `mul_lt_mul_iff_right₀` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `ConcaveOn.comp_linearMap` `strictConcaveOn_sqrt_mul_log_Ioi` `ConvexOn.smul` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `div_nonneg` `Real.log_nonneg` `Mathlib.Meta.NormNum.isNat_le_true` `convexOn_id` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Real.sqrt_eq_iff_mul_self_eq_of_pos` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `Real.log_nonneg_iff` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `one_le_div` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNat.rpow_eq_pow` `Nat.cast_ofNat` `Real.rpow_natCast` `pow_mul` `pow_add` `Real.rpow_two` `Real.rpow_mul` `Real.rpow_le_rpow_of_exponent_le` `Mathlib.Meta.NormNum.isNat_add` `LE.le.trans` `ConcaveOn.right_le_of_le_left''` `LT.lt.trans_le` `LT.lt.trans`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bertrand` 📖	mathematical	—	`Prime`	—	`exists_prime_lt_and_le_two_mul`
`exists_prime_lt_and_le_two_mul` 📖	mathematical	—	`Prime`	—	`lt_or_ge` `exists_prime_lt_and_le_two_mul_eventually` `LE.le.trans_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `exists_prime_lt_and_le_two_mul_succ` `Mathlib.Meta.NormNum.isNat_prime_2` `Mathlib.Meta.NormNum.isNat_minFac_4` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.minFacHelper_2` `Mathlib.Meta.NormNum.not_prime_mul_of_ble` `Mathlib.Meta.NormNum.minFacHelper_3` `Mathlib.Meta.NormNum.minFacHelper_0` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `prime_two`
`exists_prime_lt_and_le_two_mul_eventually` 📖	mathematical	—	`Prime`	—	`four_pow_lt_mul_centralBinom` `le_trans` `Mathlib.Meta.NormNum.isNat_le_true` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `centralBinom_le_of_no_bertrand_prime` `lt_of_lt_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `instCharZero` `le_imp_le_of_le_of_le` `mul_le_mul_right` `instMulLeftMono` `le_refl` `mul_assoc` `bertrand_main_inequality`
`exists_prime_lt_and_le_two_mul_succ` 📖	—	`Prime`	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bertrand_main_inequality` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_mul` `Nat.cast_pow` `trans` `instIsTransLe` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mul_le_mul_of_nonneg_left` `Real.rpow_le_rpow_of_exponent_le` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `lt_of_lt_of_le` `Nat.cast_one` `Real.nat_sqrt_le_real_sqrt` `le_of_lt` `Nat.cast_pos'` `NeZero.charZero_one` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.instAtLeastTwo` `LE.le.trans` `Nat.cast_div_le` `Real.instIsStrictOrderedRing` `le_refl` `Real.rpow_pos_of_pos` `Real.instNontrivial` `IsStrictOrderedRing.toPosMulStrictMono` `Bertrand.real_main_inequality`
`centralBinom_factorization_small` 📖	mathematical	—	`Nat.centralBinom` `Finset.prod` `Nat.instCommMonoid` `Finset.range` `Monoid.toNatPow` `Nat.instMonoid` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	`Finset.prod_subset` `Mathlib.Tactic.GCongr.rel_imp_rel` `Finset.instIsTransSubset` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `subset_refl` `Finset.instReflSubset` `LE.le.not_gt` `Finset.mem_range` `Nat.factorization_eq_zero_of_not_prime` `Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul` `Nat.instAtLeastTwoHAddOfNat` `mul_comm` `three_pos` `Nat.instZeroLEOneClass` `not_le` `Nat.prod_pow_factorization_centralBinom`
`centralBinom_le_of_no_bertrand_prime` 📖	mathematical	—	`Nat.centralBinom` `Monoid.toNatPow` `Nat.instMonoid`	—	`LE.le.trans_lt` `mul_pos` `Nat.instAtLeastTwoHAddOfNat` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `zero_lt_two'` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.prod_filter_of_ne` `Mathlib.Tactic.Contrapose.contrapose₂` `Nat.factorization_eq_zero_of_not_prime` `pow_zero` `centralBinom_factorization_small` `Finset.prod_filter_mul_prod_filter_not` `mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `LE.le.trans` `Finset.prod_le_prod'` `Nat.pow_factorization_choose_le` `two_pos` `Nat.card_Icc` `Finset.prod_const` `pow_right_mono₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Finset.card_le_card` `Finset.mem_filter` `Finset.mem_Icc` `LT.lt.le` `Nat.Prime.one_lt` `Eq.le` `le_trans` `Nat.factorization_choose_le_one` `Nat.sqrt_lt'` `not_le` `pow_one` `Finset.prod_le_prod_of_subset_of_one_le'` `Finset.filter_subset` `primorial_le_4_pow`

---

← Back to Index