PosLog

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

Statistics

Metric	Count
Definitions posLog, «termLog⁺»	2
Theorems half_mul_log_add_log_abs, log_of_nat_eq_posLog, monotoneOn_posLog, posLog_abs, posLog_add, posLog_def, posLog_eq_log, posLog_eq_log_max_one, posLog_eq_zero_iff, posLog_le_posLog, posLog_mul, posLog_nat_mul, posLog_neg, posLog_nonneg, posLog_norm_add_le, posLog_norm_sum_le, posLog_one, posLog_pow, posLog_prod, posLog_sub_posLog_inv, posLog_sum, posLog_zero	22
Total	24

Real

Definitions

Name	Category	Theorems
posLog 📖	CompOp	39 math math: ValueDistribution.proximity_zero, posLog_norm_add_le, monotoneOn_posLog, Polynomial.logMahlerMeasure_of_degree_eq_one, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, Polynomial.logMahlerMeasure_X_sub_C, circleIntegrable_posLog_norm_meromorphicOn, Polynomial.logMahlerMeasure_X_add_C, posLog_sub_posLog_inv, posLog_neg, posLog_eq_log, posLog_eq_zero_iff, Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots, posLog_le_posLog, posLog_abs, posLog_def, circleAverage_log_norm_add_const_eq_posLog, intervalIntegrable_posLog_norm_meromorphicOn, posLog_zero, posLog_prod, ValueDistribution.proximity_zero_of_complexValued, ValueDistribution.proximity_const, circleAverage_log_norm_sub_const_eq_posLog, posLog_one, Polynomial.logMahlerMeasure_C_mul_X_add_C, posLog_eq_log_max_one, half_mul_log_add_log_abs, posLog_nonneg, circleIntegrable_posLog_norm_meromorphicOn_of_nonneg, log_of_nat_eq_posLog, posLog_pow, ValueDistribution.proximity_coe, posLog_sum, ValueDistribution.abs_characteristic_sub_characteristic_shift_le, ValueDistribution.proximity_top, posLog_nat_mul, posLog_mul, posLog_norm_sum_le, posLog_add
«termLog⁺» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
half_mul_log_add_log_abs 📖	mathematical	—	Real instMul instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd log abs lattice instAddGroup posLog	—	Nat.instAtLeastTwoHAddOfNat abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sup_of_le_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul abs_of_nonpos LT.lt.le add_neg_cancel MulZeroClass.mul_zero sup_of_le_left
log_of_nat_eq_posLog 📖	mathematical	—	posLog Real instNatCast log	—	CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike log_zero max_self posLog_eq_log Nat.abs_cast instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass
monotoneOn_posLog 📖	mathematical	—	MonotoneOn Real instPreorder posLog Set.Ici instZero	—	log_le_log lt_trans zero_lt_one log_pos_iff le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_lt 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_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le
posLog_abs 📖	mathematical	—	posLog abs Real lattice instAddGroup	—	log_abs
posLog_add 📖	mathematical	—	Real instLE posLog instAdd log instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_congr Fin.sum_univ_two Matrix.cons_val_fin_one add_assoc Fintype.card_fin posLog_sum
posLog_def 📖	mathematical	—	posLog Real instMax instZero log	—	—
posLog_eq_log 📖	mathematical	Real instLE instOne abs lattice instAddGroup	posLog log	—	log_abs log_nonneg
posLog_eq_log_max_one 📖	mathematical	Real instLE instZero	posLog log instMax instOne	—	—
posLog_eq_zero_iff 📖	mathematical	—	posLog Real instZero instLE abs lattice instAddGroup instOne	—	posLog_abs log_nonpos_iff abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add log_abs
posLog_le_posLog 📖	mathematical	Real instLE instZero	posLog	—	monotoneOn_posLog LE.le.trans
posLog_mul 📖	mathematical	—	Real instLE posLog instMul instAdd	—	MulZeroClass.zero_mul log_zero max_self zero_add MulZeroClass.mul_zero add_zero log_mul max_add_add_le_max_add_max IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
posLog_nat_mul 📖	mathematical	—	Real instLE posLog instMul instNatCast instAdd log	—	log_of_nat_eq_posLog posLog_mul
posLog_neg 📖	mathematical	—	posLog Real instNeg	—	log_neg_eq_log
posLog_nonneg 📖	mathematical	—	Real instLE instZero posLog	—	—
posLog_norm_add_le 📖	mathematical	—	Real instLE posLog Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instAdd log instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	le_imp_le_of_le_of_le Nat.instAtLeastTwoHAddOfNat posLog_le_posLog norm_nonneg norm_add_le le_refl posLog_add add_rotate
posLog_norm_sum_le 📖	mathematical	—	Real instLE posLog Norm.norm SeminormedAddCommGroup.toNorm Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instAdd log instNatCast Finset.card instAddCommMonoid	—	le_imp_le_of_le_of_le posLog_le_posLog norm_nonneg norm_sum_le le_refl posLog_sum
posLog_one 📖	mathematical	—	posLog Real instOne instZero	—	log_one max_self
posLog_pow 📖	mathematical	—	posLog Real Monoid.toNatPow instMonoid instMul instNatCast	—	pow_zero posLog_one CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.zero_mul posLog_eq_zero_iff abs_pow instIsOrderedRing IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add MulZeroClass.mul_zero instZeroLEOneClass LT.lt.le not_le posLog_eq_log log_pow
posLog_prod 📖	mathematical	—	Real instLE posLog Finset.prod instCommMonoid Finset.sum instAddCommMonoid	—	Finset.induction log_one max_self Finset.sum_congr Finset.prod_insert posLog_mul add_le_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_refl Finset.sum_insert
posLog_sub_posLog_inv 📖	mathematical	—	Real instSub posLog instInv log	—	posLog_def log_inv sup_of_le_right sup_of_le_left IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sub_zero neg_nonneg Left.nonneg_neg_iff LT.lt.le sub_neg_eq_add zero_add
posLog_sum 📖	mathematical	—	Real instLE posLog Finset.sum instAddCommMonoid instAdd log instNatCast Finset.card	—	Finset.sum_congr log_zero max_self CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike add_zero Finset.exists_max_image posLog_abs monotoneOn_posLog IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_const nsmul_eq_mul mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing Nat.cast_nonneg' instZeroLEOneClass abs_nonneg Finset.sum_le_sum posLog_nat_mul add_le_add_right Finset.single_le_sum posLog_nonneg
posLog_zero 📖	mathematical	—	posLog Real instZero	—	log_zero max_self

---

← Back to Index