FirstMainTheorem

📁 Source: Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_characteristic_sub_characteristic_shift_eqO, abs_characteristic_sub_characteristic_shift_le, characteristic_sub_characteristic_inv, characteristic_sub_characteristic_inv_at_zero, characteristic_sub_characteristic_inv_le, characteristic_sub_characteristic_inv_of_ne_zero, isBigO_characteristic_sub_characteristic_inv, isBigO_characteristic_sub_characteristic_shift	8
Total	8

ValueDistribution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_characteristic_sub_characteristic_shift_eqO 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField	Asymptotics.IsBigO Real Real.norm Filter.atTop Real.instPreorder Pi.instSub Real.instSub characteristic Top.top WithTop WithTop.top SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Pi.instOne Real.instOne	—	isBigO_characteristic_sub_characteristic_shift
abs_characteristic_sub_characteristic_shift_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instSub characteristic Top.top WithTop WithTop.top SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instAdd Real.posLog Norm.norm NormedAddCommGroup.toNorm Real.log instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	circleIntegrable_posLog_norm_meromorphicOn Meromorphic.meromorphicOn MeromorphicOn.sub MeromorphicOn.const Nat.instAtLeastTwoHAddOfNat Pi.sub_apply characteristic_sub_characteristic_eq_proximity_sub_proximity Real.circleAverage_sub le_trans Real.abs_circleAverage_le_circleAverage_abs Real.circleAverage_mono_on_of_le_circle IntervalIntegrable.abs IntervalIntegrable.sub abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AddGroup.toOrderedSub covariant_swap_add_of_covariant_add add_comm sub_add_cancel Real.posLog_norm_add_le abs_of_nonpos le_of_not_ge neg_sub norm_neg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.termg_eq one_zsmul add_zero
characteristic_sub_characteristic_inv 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.instSub Real Real.instSub characteristic Top.top WithTop WithTop.top Pi.instInv Complex.instInv Real.circleAverage Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex.instNorm Complex.instZero DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike Function.locallyFinsuppWithin.logCounting Complex.instProperSpace MeromorphicOn.divisor	—	Complex.instProperSpace 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 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 proximity_sub_proximity_inv_eq_circleAverage logCounting_inv log_counting_zero_sub_logCounting_top
characteristic_sub_characteristic_inv_at_zero 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Real Real.instSub characteristic Top.top WithTop WithTop.top Real.instZero Pi.instInv Complex.instInv Real.log Norm.norm Complex.instNorm Complex.instZero	—	Complex.instProperSpace characteristic_sub_characteristic_inv Pi.sub_apply Real.circleAverage_zero Real.instCompleteSpace Function.locallyFinsuppWithin.logCounting_eval_zero sub_zero
characteristic_sub_characteristic_inv_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instSub characteristic Top.top WithTop WithTop.top Pi.instInv Complex.instInv Real.instMax Real.log Norm.norm Complex.instNorm Complex.instZero meromorphicTrailingCoeffAt	—	characteristic_sub_characteristic_inv_at_zero characteristic_sub_characteristic_inv_of_ne_zero
characteristic_sub_characteristic_inv_of_ne_zero 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Real Real.instSub characteristic Top.top WithTop WithTop.top Pi.instInv Complex.instInv Real.log Norm.norm Complex.instNorm meromorphicTrailingCoeffAt Complex.instZero	—	Complex.instProperSpace characteristic_sub_characteristic_inv Pi.sub_apply MeromorphicOn.circleAverage_log_norm Meromorphic.meromorphicOn MeromorphicOn.divisor_restrict dist_zero_right Int.cast_ite Int.cast_zero zero_sub norm_neg ite_mul MulZeroClass.zero_mul dist_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add add_sub_cancel_left
isBigO_characteristic_sub_characteristic_inv 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Asymptotics.IsBigO Real Real.norm Filter.atTop Real.instPreorder Pi.instSub Real.instSub characteristic Top.top WithTop WithTop.top Pi.instInv Complex.instInv Pi.instOne Real.instOne	—	Asymptotics.isBigO_of_le' CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass mul_one characteristic_sub_characteristic_inv_le
isBigO_characteristic_sub_characteristic_shift 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField	Asymptotics.IsBigO Real Real.norm Filter.atTop Real.instPreorder Pi.instSub Real.instSub characteristic Top.top WithTop WithTop.top SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Pi.instOne Real.instOne	—	Asymptotics.isBigO_of_le' Nat.instAtLeastTwoHAddOfNat CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass mul_one abs_characteristic_sub_characteristic_shift_le

---

← Back to Index