Monotone

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean

Statistics

Metric	Count
Definitions	0
Theorems log_div_self_antitoneOn, log_div_self_rpow_antitoneOn, log_div_sqrt_antitoneOn, log_mul_self_monotoneOn	4
Total	4

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
log_div_self_antitoneOn 📖	mathematical	—	AntitoneOn Real instPreorder DivInvMonoid.toDiv instDivInvMonoid log setOf instLE exp instOne	—	LT.lt.trans_le exp_pos le_log_iff_exp_le le_sub_iff_add_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing zero_add one_mul div_le_iff₀ sub_le_sub_iff_right log_div LT.lt.ne' log_le_sub_one_of_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono le_mul_of_one_le_left IsOrderedRing.toMulPosMono instIsOrderedRing Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul
log_div_self_rpow_antitoneOn 📖	mathematical	Real instLT instZero	AntitoneOn instPreorder DivInvMonoid.toDiv instDivInvMonoid log instPow setOf instLE exp instOne	—	lt_of_lt_of_le exp_pos lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt rpow_one div_self ne_of_lt div_eq_mul_one_div rpow_mul LT.lt.le log_rpow rpow_pos_of_pos mul_div_assoc mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono one_div_pos PosMulReflectLE.toPosMulReflectLT log_div_self_antitoneOn exp_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.cast_pos Nat.cast_one rpow_le_rpow le_of_lt trans instIsTransLe
log_div_sqrt_antitoneOn 📖	mathematical	—	AntitoneOn Real instPreorder DivInvMonoid.toDiv instDivInvMonoid log sqrt setOf instLE exp instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sqrt_eq_rpow Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_mul Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNNRat_mul log_div_self_rpow_antitoneOn one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing
log_mul_self_monotoneOn 📖	mathematical	—	MonotoneOn Real instPreorder instMul log setOf instLE instOne	—	lt_of_lt_of_le zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mul_le_mul IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedRing.toMulPosMono log_le_log Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_of_lt le_log_iff_exp_le exp_zero

---

← Back to Index