BinaryEntropy

📁 Source: Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

Statistics

Metric	Count
Definitions binEntropy, qaryEntropy	2
Theorems binEntropy_continuous, binEntropy_eq_log_two, binEntropy_eq_negMulLog_add_negMulLog_one_sub, binEntropy_eq_negMulLog_add_negMulLog_one_sub', binEntropy_eq_zero, binEntropy_le_log_two, binEntropy_lt_log_two, binEntropy_neg_of_neg, binEntropy_neg_of_one_lt, binEntropy_nonneg, binEntropy_nonpos_of_nonpos, binEntropy_nonpos_of_one_le, binEntropy_one, binEntropy_one_sub, binEntropy_pos, binEntropy_strictAntiOn, binEntropy_strictMonoOn, binEntropy_two_inv, binEntropy_two_inv_add, binEntropy_zero, deriv2_binEntropy, deriv2_qaryEntropy, deriv_binEntropy, deriv_qaryEntropy, differentiableAt_binEntropy, differentiableAt_binEntropy_iff_ne_zero_one, differentiableAt_qaryEntropy, hasDerivAt_binEntropy, hasDerivAt_qaryEntropy, not_continuousAt_deriv_qaryEntropy_one, not_continuousAt_deriv_qaryEntropy_zero, qaryEntropy_continuous, qaryEntropy_neg_of_neg, qaryEntropy_nonneg, qaryEntropy_nonpos_of_nonpos, qaryEntropy_one, qaryEntropy_pos, qaryEntropy_strictAntiOn, qaryEntropy_strictMonoOn, qaryEntropy_two, qaryEntropy_zero, strictConcaveOn_qaryEntropy, strictConcave_binEntropy	43
Total	45

Real

Definitions

Name	Category	Theorems
binEntropy 📖	CompOp	27 math math: deriv_binEntropy, binEntropy_continuous, binEntropy_nonneg, qaryEntropy_two, binEntropy_neg_of_neg, binEntropy_nonpos_of_nonpos, hasDerivAt_binEntropy, deriv2_binEntropy, binEntropy_zero, binEntropy_neg_of_one_lt, binEntropy_one, binEntropy_pos, binEntropy_eq_negMulLog_add_negMulLog_one_sub', binEntropy_one_sub, binEntropy_eq_log_two, binEntropy_two_inv_add, differentiableAt_binEntropy, binEntropy_lt_log_two, strictConcave_binEntropy, binEntropy_le_log_two, binEntropy_strictAntiOn, binEntropy_two_inv, differentiableAt_binEntropy_iff_ne_zero_one, binEntropy_nonpos_of_one_le, binEntropy_eq_negMulLog_add_negMulLog_one_sub, binEntropy_eq_zero, binEntropy_strictMonoOn
qaryEntropy 📖	CompOp	17 math math: qaryEntropy_two, qaryEntropy_nonneg, qaryEntropy_continuous, hasDerivAt_qaryEntropy, deriv_qaryEntropy, qaryEntropy_strictAntiOn, qaryEntropy_nonpos_of_nonpos, qaryEntropy_strictMonoOn, qaryEntropy_neg_of_neg, not_continuousAt_deriv_qaryEntropy_zero, deriv2_qaryEntropy, qaryEntropy_zero, differentiableAt_qaryEntropy, qaryEntropy_pos, not_continuousAt_deriv_qaryEntropy_one, qaryEntropy_one, strictConcaveOn_qaryEntropy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binEntropy_continuous 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace binEntropy	—	binEntropy_eq_negMulLog_add_negMulLog_one_sub' Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_negMulLog Continuous.comp' Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const continuous_id'
binEntropy_eq_log_two 📖	mathematical	—	binEntropy log Real instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instInv	—	Nat.instAtLeastTwoHAddOfNat LE.le.not_lt_iff_eq binEntropy_le_log_two binEntropy_lt_log_two not_ne_iff
binEntropy_eq_negMulLog_add_negMulLog_one_sub 📖	mathematical	—	binEntropy Real instAdd negMulLog instSub instOne	—	log_inv mul_neg neg_sub
binEntropy_eq_negMulLog_add_negMulLog_one_sub' 📖	mathematical	—	binEntropy Real instAdd negMulLog instSub instOne	—	binEntropy_eq_negMulLog_add_negMulLog_one_sub
binEntropy_eq_zero 📖	mathematical	—	binEntropy Real instZero instOne	—	Mathlib.Tactic.Contrapose.contrapose₁ Ne.lt_or_gt LT.lt.ne binEntropy_neg_of_neg binEntropy_neg_of_one_lt LT.lt.ne' binEntropy_pos binEntropy_zero binEntropy_one
binEntropy_le_log_two 📖	mathematical	—	Real instLE binEntropy log instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne binEntropy_two_inv LT.lt.le binEntropy_lt_log_two
binEntropy_lt_log_two 📖	mathematical	—	Real instLT binEntropy log instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat binEntropy_two_inv le_or_gt LE.le.trans_lt binEntropy_nonpos_of_nonpos log_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass RCLike.charZero_rclike sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add LT.lt.trans Mathlib.Meta.NormNum.isNNRat_lt_true instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one strictConcaveOn_log_Ioi inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_comm add_sub_cancel mul_inv_cancel₀ ne_of_gt one_add_one_eq_two sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul lt_of_not_ge lt_or_gt_of_ne Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.one_mul 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt 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_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le CancelDenoms.derive_trans CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le binEntropy_one_sub LT.lt.ne
binEntropy_neg_of_neg 📖	mathematical	Real instLT instZero	binEntropy	—	log_inv log_neg_eq_log log_lt_log Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_of_not_ge 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 Nat.cast_one 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt log_pos_of_lt_neg_one mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_of_not_gt log_neg_of_lt_zero Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.add_lt_of_le_of_neg log_one MulZeroClass.mul_zero Mathlib.Tactic.Linarith.add_nonpos log_pos
binEntropy_neg_of_one_lt 📖	mathematical	Real instLT instOne	binEntropy instZero	—	binEntropy_one_sub binEntropy_neg_of_neg sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
binEntropy_nonneg 📖	mathematical	Real instLE instZero instOne	binEntropy	—	LE.le.eq_or_lt binEntropy_zero binEntropy_one LT.lt.le binEntropy_pos
binEntropy_nonpos_of_nonpos 📖	mathematical	Real instLE instZero	binEntropy	—	LE.le.eq_or_lt binEntropy_zero LT.lt.le binEntropy_neg_of_neg
binEntropy_nonpos_of_one_le 📖	mathematical	Real instLE instOne	binEntropy instZero	—	binEntropy_one_sub binEntropy_nonpos_of_nonpos sub_nonpos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
binEntropy_one 📖	mathematical	—	binEntropy Real instOne instZero	—	inv_one log_one MulZeroClass.mul_zero sub_self inv_zero log_zero add_zero
binEntropy_one_sub 📖	mathematical	—	binEntropy Real instSub instOne	—	log_inv mul_neg sub_sub_cancel add_comm
binEntropy_pos 📖	mathematical	Real instLT instZero instOne	binEntropy	—	sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_pos one_lt_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing sub_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd add_pos' mul_pos
binEntropy_strictAntiOn 📖	mathematical	—	StrictAntiOn Real instPreorder binEntropy Set.Icc instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul qaryEntropy_two Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNat_natCast qaryEntropy_strictAntiOn le_refl
binEntropy_strictMonoOn 📖	mathematical	—	StrictMonoOn Real instPreorder binEntropy Set.Icc instZero instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat qaryEntropy_two qaryEntropy_strictMonoOn le_refl
binEntropy_two_inv 📖	mathematical	—	binEntropy Real instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat one_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add
binEntropy_two_inv_add 📖	mathematical	—	binEntropy Real instAdd instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub	—	Nat.instAtLeastTwoHAddOfNat binEntropy_one_sub Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.inv_congr 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.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one add_zero Mathlib.Tactic.RingNF.add_neg
binEntropy_zero 📖	mathematical	—	binEntropy Real instZero	—	inv_zero log_zero MulZeroClass.mul_zero sub_zero inv_one log_one add_zero
deriv2_binEntropy 📖	mathematical	—	Nat.iterate deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace binEntropy DivInvMonoid.toDiv instDivInvMonoid instNeg instOne instMul instSub	—	deriv2_qaryEntropy qaryEntropy_two
deriv2_qaryEntropy 📖	mathematical	—	Nat.iterate deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace qaryEntropy DivInvMonoid.toDiv instDivInvMonoid instNeg instOne instMul instSub	—	Filter.mp_mem eventually_ne_nhds T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Filter.univ_mem' deriv_qaryEntropy Filter.EventuallyEq.deriv_eq deriv_fun_sub DifferentiableAt.add DifferentiableAt.log DifferentiableAt.const_sub differentiableAt_id sub_ne_zero differentiableAt_log deriv.log differentiableAt_fun_id deriv_id'' one_div deriv_const_sub deriv_fun_add sub_ne_zero_of_ne deriv_const' zero_add Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval 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.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg mul_neg Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add deriv_zero_of_not_differentiableAt DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul sub_zero div_zero sub_self MulZeroClass.mul_zero
deriv_binEntropy 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace binEntropy instSub log instOne	—	binEntropy_eq_negMulLog_add_negMulLog_one_sub' deriv_fun_add differentiableAt_negMulLog DifferentiableAt.fun_comp' sub_ne_zero DifferentiableAt.const_sub differentiableAt_id deriv_comp_const_sub deriv_negMulLog Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add deriv_zero_of_not_differentiableAt Iff.not differentiableAt_binEntropy_iff_ne_zero_one Mathlib.Tactic.Push.not_and_or_eq sub_zero log_one log_zero sub_self
deriv_qaryEntropy 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace qaryEntropy instSub instAdd log instNatCast instOne	—	deriv_fun_add DifferentiableAt.mul_const differentiableAt_id differentiableAt_binEntropy Int.cast_sub Int.cast_natCast Int.cast_one deriv_mul_const deriv_id'' one_mul deriv_binEntropy add_sub_assoc
differentiableAt_binEntropy 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace binEntropy	—	log_inv mul_neg DifferentiableAt.fun_add DifferentiableAt.fun_neg DifferentiableAt.fun_mul differentiableAt_id DifferentiableAt.log DifferentiableAt.const_sub sub_ne_zero
differentiableAt_binEntropy_iff_ne_zero_one 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace binEntropy	—	log_inv mul_neg DifferentiableAt.fun_add_iff_left DifferentiableAt.fun_mul DifferentiableAt.const_sub differentiableAt_id DifferentiableAt.log DifferentiableAt.fun_inv sub_zero NeZero.charZero_one RCLike.charZero_rclike inv_one sub_sub_cancel sub_self differentiableAt_iff_comp_const_sub DifferentiableAt.fun_add_iff_right differentiableAt_binEntropy
differentiableAt_qaryEntropy 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace qaryEntropy	—	DifferentiableAt.fun_add DifferentiableAt.mul_const differentiableAt_id differentiableAt_binEntropy
hasDerivAt_binEntropy 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal binEntropy instSub log instOne	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal DifferentiableAt.hasDerivAt differentiableAt_binEntropy deriv_binEntropy
hasDerivAt_qaryEntropy 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal qaryEntropy instSub instAdd log instNatCast instOne	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal DifferentiableAt.hasDerivAt differentiableAt_qaryEntropy deriv_qaryEntropy
not_continuousAt_deriv_qaryEntropy_one 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace qaryEntropy instOne	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Filter.tendsto_atBot_add_const_left instIsOrderedAddMonoid not_continuousAt_of_tendsto Filter.Tendsto.congr' Filter.mp_mem Nat.instAtLeastTwoHAddOfNat Ioo_mem_nhdsLT instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Mathlib.Meta.NormNum.isNNRat_lt_true instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Filter.univ_mem' deriv_qaryEntropy Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt 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_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true sub_eq_zero_of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq neg_eq_zero nhdsLT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial instNontrivial nhdsWithin_le_nhds instNoBotOrderOfNoMinOrder
not_continuousAt_deriv_qaryEntropy_zero 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace qaryEntropy instZero	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Filter.tendsto_atTop_add_const_left instIsOrderedAddMonoid not_continuousAt_of_tendsto Filter.Tendsto.congr' Filter.mp_mem Nat.instAtLeastTwoHAddOfNat Ioo_mem_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Mathlib.Meta.NormNum.isNNRat_lt_true instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Filter.univ_mem' deriv_qaryEntropy Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_add_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.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Linarith.add_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true neg_eq_zero nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial instNontrivial nhdsWithin_le_nhds instNoTopOrderOfNoMaxOrder
qaryEntropy_continuous 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace qaryEntropy	—	Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fun_mul IsTopologicalSemiring.toContinuousMul continuous_id' continuous_const binEntropy_continuous
qaryEntropy_neg_of_neg 📖	mathematical	Real instLT instZero	qaryEntropy	—	add_neg_of_nonpos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono instIsOrderedRing LT.lt.le log_intCast_nonneg binEntropy_neg_of_neg
qaryEntropy_nonneg 📖	mathematical	Real instLE instZero instOne	qaryEntropy	—	LE.le.eq_or_lt qaryEntropy_zero one_mul binEntropy_one add_zero log_intCast_nonneg LT.lt.le qaryEntropy_pos
qaryEntropy_nonpos_of_nonpos 📖	mathematical	Real instLE instZero	qaryEntropy	—	add_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono instIsOrderedRing log_intCast_nonneg binEntropy_nonpos_of_nonpos
qaryEntropy_one 📖	mathematical	—	qaryEntropy Real instOne log instIntCast	—	Int.cast_sub Int.cast_natCast Int.cast_one one_mul binEntropy_one add_zero
qaryEntropy_pos 📖	mathematical	Real instLT instZero instOne	qaryEntropy	—	binEntropy_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing le_of_lt log_intCast_nonneg
qaryEntropy_strictAntiOn 📖	mathematical	—	StrictAntiOn Real instPreorder qaryEntropy Set.Icc instSub instOne DivInvMonoid.toDiv instDivInvMonoid instNatCast	—	strictAntiOn_of_deriv_neg convex_Icc instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing Continuous.continuousOn qaryEntropy_continuous Nat.instAtLeastTwoHAddOfNat Nat.ofNat_le_cast IsOrderedAddMonoid.toAddLeftMono instZeroLEOneClass RCLike.charZero_rclike inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_not_ge 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 Nat.cast_one 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.Meta.NormNum.instAtLeastTwo 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 Mathlib.Meta.NormNum.IsNat.to_raw_eq 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_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered instNoMinOrderOfNontrivial instNontrivial instNoMaxOrderOfNontrivial deriv_qaryEntropy Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat 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_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst Mathlib.Tactic.Linarith.sub_neg_of_lt one_div sub_eq_zero_of_eq ne_of_gt lt_add_neg_iff_lt log_mul Mathlib.Tactic.Linarith.add_lt_of_le_of_neg strictMonoOn_log Set.mem_Ioi Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_of_lt Nat.cast_pos' NeZero.charZero_one lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.add_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono inv_mul_cancel₀ LT.lt.ne'
qaryEntropy_strictMonoOn 📖	mathematical	—	StrictMonoOn Real instPreorder qaryEntropy Set.Icc instZero instSub instOne DivInvMonoid.toDiv instDivInvMonoid instNatCast	—	strictMonoOn_of_deriv_pos convex_Icc instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing Continuous.continuousOn qaryEntropy_continuous Nat.instAtLeastTwoHAddOfNat Nat.ofNat_le_cast IsOrderedAddMonoid.toAddLeftMono instZeroLEOneClass RCLike.charZero_rclike inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_pos' NeZero.charZero_one lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add one_div interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered instNoMinOrderOfNontrivial instIsOrderedRing instNontrivial instNoMaxOrderOfNontrivial 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.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_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 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.mul_add Mathlib.Tactic.Ring.add_pf_add_zero 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le deriv_qaryEntropy Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq ne_of_gt lt_add_neg_iff_lt log_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Linarith.add_lt_of_le_of_neg strictMonoOn_log Set.mem_Ioi mul_sub mul_one IsUnit.mul_inv_cancel mul_lt_mul_of_pos_left Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one
qaryEntropy_two 📖	mathematical	—	qaryEntropy binEntropy	—	Int.cast_one log_one MulZeroClass.mul_zero zero_add
qaryEntropy_zero 📖	mathematical	—	qaryEntropy Real instZero	—	Int.cast_sub Int.cast_natCast Int.cast_one MulZeroClass.zero_mul binEntropy_zero add_zero
strictConcaveOn_qaryEntropy 📖	mathematical	—	StrictConcaveOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc instPreorder instZero instOne qaryEntropy	—	strictConcaveOn_of_deriv2_neg convex_Icc instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing Continuous.continuousOn qaryEntropy_continuous deriv2_qaryEntropy div_neg_of_neg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.NormNum.isInt_lt_true instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_zero interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered instNoMinOrderOfNontrivial instNoMaxOrderOfNontrivial IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
strictConcave_binEntropy 📖	mathematical	—	StrictConcaveOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc instPreorder instZero instOne binEntropy	—	strictConcaveOn_qaryEntropy qaryEntropy_two

---

← Back to Index