MahlerMeasure

📁 Source: Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Statistics

Metric	Count
Definitions `logMahlerMeasure`, `mahlerMeasure`	2
Theorems `intervalIntegrable_mahlerMeasure`, `leading_coeff_le_mahlerMeasure`, `logMahlerMeasure_C_mul`, `logMahlerMeasure_C_mul_X_add_C`, `logMahlerMeasure_X`, `logMahlerMeasure_X_add_C`, `logMahlerMeasure_X_sub_C`, `logMahlerMeasure_const`, `logMahlerMeasure_def`, `logMahlerMeasure_eq_log_MahlerMeasure`, `logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots`, `logMahlerMeasure_monomial`, `logMahlerMeasure_mul_eq_add_logMahelerMeasure`, `logMahlerMeasure_mul_eq_add_logMahlerMeasure`, `logMahlerMeasure_of_degree_eq_one`, `logMahlerMeasure_one`, `logMahlerMeasure_zero`, `mahlerMeasure_C_mul_X_add_C`, `mahlerMeasure_X_add_C`, `mahlerMeasure_X_sub_C`, `mahlerMeasure_const`, `mahlerMeasure_def_of_ne_zero`, `mahlerMeasure_eq_leadingCoeff_mul_prod_roots`, `mahlerMeasure_eq_zero_iff`, `mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm`, `mahlerMeasure_le_sum_norm_coeff`, `mahlerMeasure_mul`, `mahlerMeasure_nonneg`, `mahlerMeasure_of_degree_eq_one`, `mahlerMeasure_one`, `mahlerMeasure_pos_of_ne_zero`, `mahlerMeasure_zero`, `norm_coeff_le_choose_mul_mahlerMeasure`, `one_le_prod_max_one_norm_roots`, `prod_mahlerMeasure_eq_mahlerMeasure_prod`, `prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff`, `supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure`	37
Total	39

Polynomial

Definitions

Name	Category	Theorems
`logMahlerMeasure` 📖	CompOp	15 math math: `logMahlerMeasure_one`, `logMahlerMeasure_C_mul`, `logMahlerMeasure_of_degree_eq_one`, `logMahlerMeasure_mul_eq_add_logMahelerMeasure`, `logMahlerMeasure_mul_eq_add_logMahlerMeasure`, `logMahlerMeasure_X_sub_C`, `logMahlerMeasure_X_add_C`, `logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots`, `logMahlerMeasure_def`, `logMahlerMeasure_X`, `logMahlerMeasure_eq_log_MahlerMeasure`, `logMahlerMeasure_zero`, `logMahlerMeasure_const`, `logMahlerMeasure_monomial`, `logMahlerMeasure_C_mul_X_add_C`
`mahlerMeasure` 📖	CompOp	25 math math: `mahlerMeasure_const`, `mahlerMeasure_def_of_ne_zero`, `mahlerMeasure_eq_leadingCoeff_mul_prod_roots`, `mahlerMeasure_nonneg`, `mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm`, `mahlerMeasure_eq_zero_iff`, `mahlerMeasure_C_mul_X_add_C`, `prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff`, `one_le_mahlerMeasure_of_ne_zero`, `mahlerMeasure_pos_of_ne_zero`, `mahlerMeasure_X_add_C`, `mahlerMeasure_mul`, `prod_mahlerMeasure_eq_mahlerMeasure_prod`, `logMahlerMeasure_eq_log_MahlerMeasure`, `mahlerMeasure_X_sub_C`, `mahlerMeasure_one`, `mahlerMeasure_zero`, `leading_coeff_le_mahlerMeasure`, `supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure`, `mahlerMeasure_of_degree_eq_one`, `cyclotomic_mahlerMeasure_eq_one`, `norm_coeff_le_choose_mul_mahlerMeasure`, `finite_mahlerMeasure_le`, `mahlerMeasure_le_sum_norm_coeff`, `card_mahlerMeasure_le_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intervalIntegrable_mahlerMeasure` 📖	mathematical	—	`IntervalIntegrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `eval` `Complex.instSemiring` `circleMap` `Complex.instZero` `Real.instOne` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `circleIntegrable_def` `circleIntegrable_log_norm_meromorphicOn` `AnalyticOnNhd.meromorphicOn` `AnalyticOnNhd.aeval_polynomial` `analyticOnNhd_id`
`leading_coeff_le_mahlerMeasure` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `leadingCoeff` `Complex.instSemiring` `mahlerMeasure`	—	`mul_one` `instIsDomain` `mahlerMeasure_eq_leadingCoeff_mul_prod_roots` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `one_le_prod_max_one_norm_roots` `norm_nonneg`
`logMahlerMeasure_C_mul` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real` `Real.instAdd` `Real.log` `Norm.norm` `Complex.instNorm`	—	`logMahlerMeasure_mul_eq_add_logMahlerMeasure` `instNoZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `nontrivial` `Complex.instNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `logMahlerMeasure_const`
`logMahlerMeasure_C_mul_X_add_C` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `Real` `Real.instAdd` `Real.log` `Norm.norm` `Complex.instNorm` `Real.posLog` `Complex.instMul` `Complex.instInv`	—	`mul_add` `Distrib.leftDistribClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_inv_cancel_left₀` `logMahlerMeasure_C_mul` `X_add_C_ne_zero` `Complex.instNontrivial` `logMahlerMeasure_X_add_C`
`logMahlerMeasure_X` 📖	mathematical	—	`logMahlerMeasure` `X` `Complex` `Complex.instSemiring` `Real` `Real.instZero`	—	`eval_X` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `norm_circleMap_zero` `abs_one` `Real.instIsOrderedRing` `Real.log_one` `intervalIntegral.integral_zero` `MulZeroClass.mul_zero`
`logMahlerMeasure_X_add_C` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real.posLog` `Norm.norm` `Complex.instNorm`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `logMahlerMeasure_X_sub_C` `norm_neg`
`logMahlerMeasure_X_sub_C` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instSub` `Complex.instRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real.posLog` `Norm.norm` `Complex.instNorm`	—	`eval_sub` `eval_X` `eval_C` `circleAverage_log_norm_sub_const_eq_posLog`
`logMahlerMeasure_const` 📖	mathematical	—	`logMahlerMeasure` `DFunLike.coe` `RingHom` `Complex` `Polynomial` `Complex.instSemiring` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real.log` `Norm.norm` `Complex.instNorm`	—	`eval_C` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_zero` `mul_assoc` `inv_mul_cancel_left₀` `RCLike.charZero_rclike`
`logMahlerMeasure_def` 📖	mathematical	—	`logMahlerMeasure` `Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `eval` `Complex.instSemiring` `Complex.instZero` `Real.instOne`	—	—
`logMahlerMeasure_eq_log_MahlerMeasure` 📖	mathematical	—	`logMahlerMeasure` `Real.log` `mahlerMeasure`	—	`mahlerMeasure.eq_1` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `Real.log_exp` `eval_zero` `norm_zero` `Real.log_zero` `intervalIntegral.integral_zero` `MulZeroClass.mul_zero`
`logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots` 📖	mathematical	—	`logMahlerMeasure` `Real` `Real.instAdd` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `leadingCoeff` `Complex.instSemiring` `Multiset.sum` `Real.instAddCommMonoid` `Multiset.map` `Real.posLog` `roots` `Complex.commRing` `instIsDomain` `Field.toSemifield` `Complex.instField`	—	`instIsDomain` `logMahlerMeasure_zero` `norm_zero` `Real.log_zero` `Multiset.map_congr` `roots.congr_simp` `roots_zero` `add_zero` `Splits.eq_prod_roots` `IsAlgClosed.splits` `Complex.isAlgClosed` `logMahlerMeasure_mul_eq_add_logMahlerMeasure` `instNoZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `nontrivial` `Complex.instNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `logMahlerMeasure_eq_log_MahlerMeasure` `mahlerMeasure_const` `prod_mahlerMeasure_eq_mahlerMeasure_prod` `Multiset.map_map` `mahlerMeasure_X_sub_C` `Real.log_multiset_prod` `Real.posLog_eq_log_max_one`
`logMahlerMeasure_monomial` 📖	mathematical	—	`logMahlerMeasure` `DFunLike.coe` `LinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Real.log` `Norm.norm` `Complex.instNorm`	—	`eval_monomial` `Complex.norm_mul` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `norm_circleMap_zero` `abs_one` `Real.instIsOrderedRing` `one_pow` `mul_one` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_zero` `mul_assoc` `inv_mul_cancel_left₀` `RCLike.charZero_rclike`
`logMahlerMeasure_mul_eq_add_logMahelerMeasure` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instMul` `Real` `Real.instAdd`	—	`logMahlerMeasure_mul_eq_add_logMahlerMeasure`
`logMahlerMeasure_mul_eq_add_logMahlerMeasure` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instMul` `Real` `Real.instAdd`	—	`logMahlerMeasure_eq_log_MahlerMeasure` `mahlerMeasure_mul` `Real.log_mul` `instNoZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`logMahlerMeasure_of_degree_eq_one` 📖	mathematical	`degree` `Complex` `Complex.instSemiring` `WithBot` `WithBot.one` `Nat.instOne`	`logMahlerMeasure` `Real` `Real.instAdd` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `coeff` `Complex.instSemiring` `Real.posLog` `Complex.instMul` `Complex.instInv`	—	`eq_X_add_C_of_degree_le_one` `le_of_eq` `logMahlerMeasure_C_mul_X_add_C` `coeff_ne_zero_of_eq_degree` `Complex.norm_mul` `norm_inv` `coeff_add` `coeff_mul_X` `coeff_C_zero` `coeff_C_succ` `add_zero` `mul_coeff_zero` `coeff_X_zero` `MulZeroClass.mul_zero` `zero_add`
`logMahlerMeasure_one` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instOne` `Real` `Real.instZero`	—	`eval_one` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `Real.log_one` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `intervalIntegral.integral_zero` `MulZeroClass.mul_zero`
`logMahlerMeasure_zero` 📖	mathematical	—	`logMahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instZero` `Real` `Real.instZero`	—	`eval_zero` `norm_zero` `Real.log_zero` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `intervalIntegral.integral_zero` `MulZeroClass.mul_zero`
`mahlerMeasure_C_mul_X_add_C` 📖	mathematical	—	`mahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `Real` `Real.instMax` `Norm.norm` `Complex.instNorm`	—	`mul_add` `Distrib.leftDistribClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_inv_cancel_left₀` `mahlerMeasure_mul` `mahlerMeasure_const` `mahlerMeasure_X_add_C` `Nat.cast_one` `nnnorm_mul` `NormedDivisionRing.toNormMulClass` `nnnorm_inv` `mul_max` `NNReal.mulLeftMono` `mul_one`
`mahlerMeasure_X_add_C` 📖	mathematical	—	`mahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real` `Real.instMax` `Real.instOne` `Norm.norm` `Complex.instNorm`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `mahlerMeasure_X_sub_C` `norm_neg`
`mahlerMeasure_X_sub_C` 📖	mathematical	—	`mahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instSub` `Complex.instRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real` `Real.instMax` `Real.instOne` `Norm.norm` `Complex.instNorm`	—	`logMahlerMeasure_X_sub_C` `Real.exp_log` `lt_of_lt_of_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `le_max_left` `mahlerMeasure_pos_of_ne_zero` `X_sub_C_ne_zero` `Complex.instNontrivial` `Real.posLog_eq_log_max_one` `norm_nonneg` `logMahlerMeasure_eq_log_MahlerMeasure`
`mahlerMeasure_const` 📖	mathematical	—	`mahlerMeasure` `DFunLike.coe` `RingHom` `Complex` `Polynomial` `Complex.instSemiring` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Norm.norm` `Complex.instNorm`	—	`nontrivial` `Complex.instNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `logMahlerMeasure_const` `norm_zero` `Real.exp_log`
`mahlerMeasure_def_of_ne_zero` 📖	mathematical	—	`mahlerMeasure` `Real.exp` `Real` `Real.instMul` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `intervalIntegral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `eval` `Complex.instSemiring` `circleMap` `Complex.instZero` `Real.instOne` `Real.instZero` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev`
`mahlerMeasure_eq_leadingCoeff_mul_prod_roots` 📖	mathematical	—	`mahlerMeasure` `Real` `Real.instMul` `Norm.norm` `Complex` `Complex.instNorm` `leadingCoeff` `Complex.instSemiring` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `Real.instMax` `Real.instOne` `roots` `Complex.commRing` `instIsDomain` `Field.toSemifield` `Complex.instField`	—	`instIsDomain` `mahlerMeasure_zero` `norm_zero` `Multiset.map_congr` `roots.congr_simp` `roots_zero` `mul_one` `logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots` `Real.exp_log` `norm_pos_iff` `leadingCoeff_ne_zero` `mahlerMeasure_pos_of_ne_zero` `Real.exp_add` `logMahlerMeasure_eq_log_MahlerMeasure` `Real.posLog_eq_log_max_one` `Real.exp_multiset_sum` `Multiset.map_map` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`mahlerMeasure_eq_zero_iff` 📖	mathematical	—	`mahlerMeasure` `Real` `Real.instZero` `Polynomial` `Complex` `Complex.instSemiring` `instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Nat.instAtLeastTwoHAddOfNat` `mahlerMeasure_def_of_ne_zero` `mul_inv_rev` `mahlerMeasure_zero`
`mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm` 📖	mathematical	—	`Real` `Real.instLE` `mahlerMeasure` `Real.instMul` `Real.sqrt` `Real.instAdd` `Real.instNatCast` `natDegree` `Complex` `Complex.instSemiring` `Real.instOne` `supNorm` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.uIoc_of_le` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.pi_pos` `Real.isFiniteMeasure_restrict_Ioc` `Real.volume_uIoc` `sub_zero` `abs_mul` `Nat.abs_ofNat` `ENNReal.ofReal_mul` `ENNReal.ofReal_ofNat` `ENNReal.instNoZeroDivisors` `ENNReal.instCharZero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mahlerMeasure_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_add` `Real.sqrt_one` `supNorm_zero` `MulZeroClass.mul_zero` `instReflLe` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `measurableSet_uIoc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Set.Finite.measure_zero` `Set.Finite.of_finite_image` `Set.Finite.subset` `instIsDomain` `Multiset.finite_toSet` `mem_roots` `Set.InjOn.mono` `injOn_circleMap_of_abs_sub_le` `one_ne_zero` `NeZero.charZero_one` `zero_sub` `abs_neg` `abs_of_pos` `Real.noAtoms_volume` `Filter.mp_mem` `Filter.univ_mem'` `Real.exp_log` `Continuous.norm` `Continuous.comp'` `continuous` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_circleMap` `Real.circleAverage_eq_intervalAverage` `ConvexOn.map_average_le` `Real.instCompleteSpace` `MeasureTheory.Measure.restrict.neZero` `convexOn_exp` `Real.continuousOn_exp` `isClosed_univ` `circleIntegrable_log_norm_meromorphicOn` `AnalyticOnNhd.meromorphicOn` `AnalyticOnNhd.aeval_polynomial` `analyticOnNhd_id` `MeasureTheory.integrable_congr` `Continuous.integrableOn_uIoc` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.average_congr` `Real.sqrt_sq` `MeasureTheory.integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `norm_nonneg` `Real.sqrt_monotone` `convexOn_pow` `continuousOn_pow` `IsTopologicalSemiring.toContinuousMul` `instIsTopologicalRingReal` `isClosed_Ici` `MeasureTheory.IntegrableOn.mono_set` `Continuous.integrableOn_Icc` `Set.Ioc_subset_Icc_self` `Continuous.comp` `continuous_pow` `sum_sq_norm_coeff_eq_circleAverage` `LE.le.trans` `Finset.sum_le_card_nsmul` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `le_supNorm` `nsmul_eq_mul` `mul_le_mul_of_nonneg_right` `Nat.cast_one` `Real.instZeroLEOneClass` `card_supp_le_succ_natDegree` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `Real.sqrt_mul` `Right.add_pos_of_nonneg_of_pos` `Nat.cast_nonneg'` `supNorm_nonneg`
`mahlerMeasure_le_sum_norm_coeff` 📖	mathematical	—	`Real` `Real.instLE` `mahlerMeasure` `sum` `Complex` `Complex.instSemiring` `Real.instAddCommMonoid` `Norm.norm` `Complex.instNorm`	—	`mahlerMeasure_zero` `sum_zero_index` `instReflLe` `Finset.sum_pos'` `Real.instIsOrderedCancelAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_nonneg` `Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_zero` `mul_assoc` `inv_mul_cancel_left₀` `RCLike.charZero_rclike` `Real.exp_log` `mahlerMeasure_def_of_ne_zero` `Real.circleAverage_def` `smul_eq_mul` `Real.exp_monotone` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `intervalIntegral.integral_mono_ae_restrict` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.pi_pos` `intervalIntegrable_mahlerMeasure` `Real.locallyFinite_volume` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyLE.eq_1` `Filter.eventually_iff_exists_mem` `MeasureTheory.mem_ae_iff` `Set.compl_def` `MeasureTheory.Measure.restrict_apply'` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Set.Finite.measure_zero` `Set.Finite.of_diff` `Set.inter_diff_assoc` `Set.Icc_diff_right` `Set.setOf_inter_eq_sep` `Set.Finite.of_finite_image` `Set.Finite.subset` `instIsDomain` `Multiset.finite_toSet` `injOn_circleMap_of_abs_sub_le'` `one_ne_zero` `NeZero.charZero_one` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `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.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `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.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_zero_add` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Set.finite_singleton` `Real.noAtoms_volume` `Real.log_le_log` `norm_pos_iff` `eval_eq_sum` `norm_sum_le_of_le` `Complex.norm_mul` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `norm_circleMap_zero` `abs_one` `one_pow` `mul_one` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`mahlerMeasure_mul` 📖	mathematical	—	`mahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instMul` `Real` `Real.instMul`	—	`mahlerMeasure_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `mul_eq_zero` `instNoZeroDivisors` `Nat.instAtLeastTwoHAddOfNat` `eval_mul` `Complex.norm_mul` `mul_inv_rev` `Real.exp_add` `left_distrib` `Distrib.leftDistribClass` `intervalIntegral.integral_add` `intervalIntegrable_mahlerMeasure` `intervalIntegral.integral_congr_ae` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_iff` `Set.Finite.measure_zero` `Set.Finite.of_finite_image` `Set.Finite.subset` `instIsDomain` `Multiset.finite_toSet` `Mathlib.Tactic.Contrapose.contrapose₂` `Real.log_mul` `Set.InjOn.mono` `injOn_circleMap_of_abs_sub_le` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `zero_sub` `abs_neg` `abs_mul` `Real.instIsOrderedRing` `Nat.abs_ofNat` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `Real.instIsOrderedAddMonoid` `Real.noAtoms_volume`
`mahlerMeasure_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `mahlerMeasure`	—	`mahlerMeasure_zero` `instReflLe` `Nat.instAtLeastTwoHAddOfNat` `mahlerMeasure_def_of_ne_zero` `mul_inv_rev`
`mahlerMeasure_of_degree_eq_one` 📖	mathematical	`degree` `Complex` `Complex.instSemiring` `WithBot` `WithBot.one` `Nat.instOne`	`mahlerMeasure` `Real` `Real.instMax` `Norm.norm` `Complex` `Complex.instNorm` `coeff` `Complex.instSemiring`	—	`eq_X_add_C_of_degree_le_one` `le_of_eq` `mahlerMeasure_C_mul_X_add_C` `coeff_ne_zero_of_eq_degree` `coeff_add` `coeff_mul_X` `coeff_C_zero` `coeff_C_succ` `add_zero` `mul_coeff_zero` `coeff_X_zero` `MulZeroClass.mul_zero` `zero_add`
`mahlerMeasure_one` 📖	mathematical	—	`mahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instOne` `Real` `Real.instOne`	—	`NeZero.charZero_one` `charZero` `Complex.instCharZero` `logMahlerMeasure_one` `Real.exp_zero`
`mahlerMeasure_pos_of_ne_zero` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `mahlerMeasure`	—	—
`mahlerMeasure_zero` 📖	mathematical	—	`mahlerMeasure` `Polynomial` `Complex` `Complex.instSemiring` `instZero` `Real` `Real.instZero`	—	—
`norm_coeff_le_choose_mul_mahlerMeasure` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `coeff` `Complex.instSemiring` `Real.instMul` `Real.instNatCast` `Nat.choose` `natDegree` `mahlerMeasure`	—	`norm_zero` `mahlerMeasure_zero` `MulZeroClass.mul_zero` `instReflLe` `lt_or_ge` `coeff_eq_zero_of_natDegree_lt` `Nat.choose_eq_zero_of_lt` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.zero_mul` `instIsDomain` `mahlerMeasure_eq_leadingCoeff_mul_prod_roots` `mul_left_comm` `coeff_eq_esymm_roots_of_card` `splits_iff_card_roots` `IsAlgClosed.splits` `Complex.isAlgClosed` `mul_assoc` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `norm_neg` `NormOneClass.norm_one` `one_pow` `one_mul` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `leadingCoeff_ne_zero` `Multiset.esymm.eq_1` `Finset.sum_multiset_map_count` `le_trans` `norm_sum_le` `Finset.sum_congr` `nsmul_eq_mul` `norm_natCast` `RCLike.instNormSMulClassInt` `Finset.prod_le_prod` `Real.instZeroLEOneClass` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `norm_nonneg` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `le_max_right` `Finset.prod_congr` `Nat.cast_one` `Finset.prod_le_prod_of_subset_of_one_le'` `NNReal.mulLeftMono` `Multiset.toFinset_subset` `Multiset.subset_of_le` `Multiset.mem_powersetCard` `Multiset.mem_toFinset` `one_le_pow₀` `le_max_left` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `lt_max_of_lt_left` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `pow_le_pow_right₀` `Multiset.count_le_of_le` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `Finset.prod_multiset_map_count` `Finset.prod_multiset_count` `norm_prod` `Nat.cast_nonneg'` `Finset.sum_mul` `Multiset.sum_count_eq_card` `Multiset.card_powersetCard` `Nat.choose_symm`
`one_le_prod_max_one_norm_roots` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `Complex` `Real.instMax` `Norm.norm` `Complex.instNorm` `roots` `Complex.commRing` `instIsDomain` `Field.toSemifield` `Complex.instField`	—	—
`prod_mahlerMeasure_eq_mahlerMeasure_prod` 📖	mathematical	—	`mahlerMeasure` `Multiset.prod` `Polynomial` `Complex` `Complex.instSemiring` `CommRing.toCommMonoid` `commRing` `Complex.commRing` `Real` `Real.instCommMonoid` `Multiset.map`	—	`Multiset.induction_on` `mahlerMeasure_one` `Multiset.prod_cons` `mahlerMeasure_mul` `Multiset.map_cons`
`prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Norm.norm` `Complex` `Complex.instNorm` `leadingCoeff` `Complex.instSemiring`	`Real` `Real.instLE` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `Complex` `Real.instMax` `Real.instOne` `Norm.norm` `Complex.instNorm` `roots` `Complex.commRing` `instIsDomain` `Field.toSemifield` `Complex.instField` `mahlerMeasure`	—	`instIsDomain` `one_mul` `mahlerMeasure_eq_leadingCoeff_mul_prod_roots` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `LE.le.trans` `zero_le_one` `Real.instZeroLEOneClass` `one_le_prod_max_one_norm_roots`
`supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure` 📖	mathematical	—	`Real` `Real.instLE` `supNorm` `Complex` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Real.instMul` `Real.instNatCast` `Nat.choose` `natDegree` `Complex.instSemiring` `mahlerMeasure`	—	`exists_eq_supNorm` `norm_coeff_le_choose_mul_mahlerMeasure` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.choose_le_middle` `mahlerMeasure_nonneg`

---

← Back to Index