Bounds

📁 Source: Mathlib/NumberTheory/Harmonic/Bounds.lean

Statistics

Metric	Count
Definitions	0
Theorems harmonic_eq_sum_Icc, harmonic_floor_le_one_add_log, harmonic_le_one_add_log, log_add_one_le_harmonic, log_le_harmonic_floor	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonic_eq_sum_Icc 📖	mathematical	—	harmonic Finset.sum Rat.addCommMonoid Finset.Icc Nat.instPreorder Nat.instLocallyFiniteOrder	—	harmonic.eq_1 Finset.range_eq_Ico Finset.sum_Ico_add' Nat.instIsOrderedCancelAddMonoid StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Finset.sum_congr Finset.Ico_add_one_right_eq_Icc Nat.instNoMaxOrder
harmonic_floor_le_one_add_log 📖	mathematical	Real Real.instLE Real.instOne	Real.instRatCast harmonic Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Real.instAdd Real.log	—	LE.le.trans Real.instIsStrictOrderedRing harmonic_le_one_add_log add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.log_le_log Nat.cast_zero Real.instZeroLEOneClass RCLike.charZero_rclike Nat.floor_pos Nat.floor_le zero_le_one
harmonic_le_one_add_log 📖	mathematical	—	Real Real.instLE Real.instRatCast harmonic Real.instAdd Real.instOne Real.log Real.instNatCast	—	Rat.cast_zero CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike Real.log_zero add_zero Real.instZeroLEOneClass harmonic_eq_sum_Icc Rat.cast_sum Finset.sum_congr Rat.cast_inv Rat.cast_natCast Finset.sum_erase_add Finset.left_mem_Icc add_comm Nat.cast_one inv_one add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.Icc_erase_left Nat.instAtLeastTwoHAddOfNat Nat.cast_add add_sub_cancel_right AntitoneOn.sum_le_integral_Ico le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing sub_inv_antitoneOn_Icc_right PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.instAtLeastTwo intervalIntegral.integral_comp_sub_right div_one integral_inv Set.uIcc_of_le Real.instIsOrderedRing NeZero.charZero_one
log_add_one_le_harmonic 📖	mathematical	—	Real Real.instLE Real.log Real.instNatCast Real.instRatCast harmonic	—	Nat.cast_one integral_inv Nat.cast_add Set.uIcc_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Real.instIsOrderedRing Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike div_one AntitoneOn.integral_le_sum_Ico inv_antitoneOn_Icc_right PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing harmonic_eq_sum_Icc Rat.cast_sum Finset.sum_congr Rat.cast_inv Rat.cast_natCast
log_le_harmonic_floor 📖	mathematical	Real Real.instLE Real.instZero	Real.log Real.instRatCast harmonic Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing	—	Real.instIsStrictOrderedRing Real.log_zero Nat.floor_zero Rat.cast_zero Real.log_le_log lt_of_le_of_ne' LE.le.trans Nat.le_ceil IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Nat.ceil_le_floor_add_one log_add_one_le_harmonic

---

← Back to Index