Basic

📁 Source: Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean

Statistics

Metric	Count
Definitions proximity	1
Theorems proximity_add_top_le, proximity_coe, proximity_coe_eq_proximity_sub_const_zero, proximity_congr_codiscrete, proximity_congr_codiscreteWithin, proximity_const, proximity_even, proximity_inv, proximity_mul_top_le, proximity_mul_zero_le, proximity_nonneg, proximity_pow_top, proximity_pow_zero, proximity_sub_proximity_inv_eq_circleAverage, proximity_sum_top_le, proximity_top, proximity_top_mul_le, proximity_zero, proximity_zero_mul_le, proximity_zero_of_complexValued	20
Total	21

ValueDistribution

Definitions

Name	Category	Theorems
proximity 📖	CompOp	21 math math: proximity_zero, proximity_zero_mul_le, proximity_pow_zero, proximity_coe_eq_proximity_sub_const_zero, proximity_nonneg, proximity_inv, proximity_congr_codiscreteWithin, characteristic_sub_characteristic_eq_proximity_sub_proximity, proximity_sum_top_le, proximity_mul_zero_le, proximity_add_top_le, proximity_mul_top_le, proximity_zero_of_complexValued, proximity_const, proximity_congr_codiscrete, proximity_pow_top, proximity_even, proximity_top_mul_le, proximity_coe, proximity_top, proximity_sub_proximity_inv_eq_circleAverage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
proximity_add_top_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField	Pi.hasLe Real Real.instLE proximity Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top Real.instAdd Real.log instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_congr Fin.sum_univ_two Matrix.cons_val_fin_one Fintype.card_fin proximity_sum_top_le Fintype.complete
proximity_coe 📖	mathematical	—	proximity WithTop.some Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.posLog Real.instInv Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Complex Complex.instZero	—	—
proximity_coe_eq_proximity_sub_const_zero 📖	mathematical	—	proximity WithTop.some Pi.instSub Complex SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup WithTop WithTop.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	WithTop.untop₀_zero sub_zero
proximity_congr_codiscrete 📖	mathematical	Filter.EventuallyEq Complex Filter.codiscrete UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	proximity	—	proximity_congr_codiscreteWithin Filter.EventuallyEq.filter_mono Filter.codiscreteWithin.mono
proximity_congr_codiscreteWithin 📖	mathematical	Filter.EventuallyEq Complex Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Metric.sphere Complex.instZero abs Real Real.lattice Real.instAddGroup	proximity	—	Real.circleAverage_congr_codiscreteWithin Filter.mp_mem Filter.univ_mem'
proximity_const 📖	mathematical	—	proximity Top.top WithTop WithTop.top Real.posLog Norm.norm NormedAddCommGroup.toNorm	—	Real.circleAverage_const Real.instCompleteSpace
proximity_even 📖	mathematical	—	Function.Even Real Real.instNeg proximity	—	Real.circleAverage_neg_radius
proximity_inv 📖	mathematical	—	proximity Complex Complex.instNormedAddCommGroup Pi.instInv Complex.instInv Top.top WithTop WithTop.top WithTop.zero Complex.instZero	—	proximity_top norm_inv proximity_zero
proximity_mul_top_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.hasLe Real Real.instLE proximity Pi.instMul Complex.instMul Top.top WithTop WithTop.top Pi.instAdd Real.instAdd	—	Complex.norm_mul Real.circleAverage_mono NormedDivisionRing.toNormMulClass circleIntegrable_posLog_norm_meromorphicOn Meromorphic.meromorphicOn Meromorphic.fun_mul CircleIntegrable.add Real.posLog_mul Real.circleAverage_add
proximity_mul_zero_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.hasLe Real Real.instLE proximity Pi.instMul Complex.instMul WithTop WithTop.zero Complex.instZero Pi.instAdd Real.instAdd	—	proximity_inv mul_inv proximity_mul_top_le Meromorphic.inv
proximity_nonneg 📖	mathematical	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero proximity	—	Real.circleAverage_nonneg_of_nonneg Real.posLog_nonneg
proximity_pow_top 📖	mathematical	—	proximity Complex Complex.instNormedAddCommGroup Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Top.top WithTop WithTop.top AddMonoid.toNatSMul Pi.addMonoid Real Real.instAddMonoid	—	norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Real.posLog_pow Real.circleAverage_fun_smul NormedSpace.toNormSMulClass Algebra.to_smulCommClass nsmul_eq_mul
proximity_pow_zero 📖	mathematical	—	proximity Complex Complex.instNormedAddCommGroup Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring WithTop WithTop.zero Complex.instZero AddMonoid.toNatSMul Pi.addMonoid Real Real.instAddMonoid	—	proximity_inv inv_pow proximity_pow_top
proximity_sub_proximity_inv_eq_circleAverage 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.instSub Real Real.instSub proximity 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	—	norm_inv Real.circleAverage_sub circleIntegrable_posLog_norm_meromorphicOn Meromorphic.meromorphicOn Meromorphic.inv
proximity_sum_top_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField	Pi.hasLe Real Real.instLE proximity Finset.sum Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top Pi.instAdd Real.instAdd Real.instAddCommMonoid Real.log Real.instNatCast Finset.card	—	proximity_top Finset.sum_apply Finset.sum_congr circleIntegrable_posLog_norm_meromorphicOn Real.circleAverage_mono Meromorphic.meromorphicOn Meromorphic.fun_sum CircleIntegrable.add CircleIntegrable.fun_sum circleIntegrable_const add_comm Real.posLog_norm_sum_le Real.circleAverage_const Real.instCompleteSpace Real.circleAverage_sum Real.circleAverage_add CircleIntegrable.sum
proximity_top 📖	mathematical	—	proximity Top.top WithTop WithTop.top Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.posLog Norm.norm NormedAddCommGroup.toNorm Complex Complex.instZero	—	—
proximity_top_mul_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.hasLe Real Real.instLE proximity Pi.instMul Complex.instMul Top.top WithTop WithTop.top Pi.instAdd Real.instAdd	—	proximity_mul_top_le
proximity_zero 📖	mathematical	—	proximity WithTop WithTop.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.posLog Real.instInv Norm.norm NormedAddCommGroup.toNorm Complex Complex.instZero	—	WithTop.untop₀_zero sub_zero
proximity_zero_mul_le 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.hasLe Real Real.instLE proximity Pi.instMul Complex.instMul WithTop WithTop.zero Complex.instZero Pi.instAdd Real.instAdd	—	proximity_mul_zero_le
proximity_zero_of_complexValued 📖	mathematical	—	proximity Complex Complex.instNormedAddCommGroup WithTop WithTop.zero Complex.instZero Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.posLog Norm.norm Complex.instNorm Pi.instInv Complex.instInv	—	WithTop.untop₀_zero sub_zero norm_inv

---

← Back to Index