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 Complex 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 Complex Complex.instNormedAddCommGroup 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 Complex Complex.instNormedAddCommGroup 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Top.top WithTop WithTop.top AddMonoid.toNSMul 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring WithTop WithTop.zero Complex.instZero AddMonoid.toNSMul 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 Complex Complex.instNormedAddCommGroup Top.top WithTop WithTop.top Pi.instInv Complex.instInv Real.circleAverage Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 Complex 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 Complex Complex.instNormedAddCommGroup 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 Complex Complex.instNormedAddCommGroup 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