CircleMap

📁 Source: Mathlib/Analysis/SpecialFunctions/Complex/CircleMap.lean

Statistics

Metric	Count
Definitions circleMap	1
Theorems preimage_circleMap, circleMap_eq_center_iff, circleMap_eq_circleMap_iff, circleMap_mem_closedBall, circleMap_mem_sphere, circleMap_mem_sphere', circleMap_ne_center, circleMap_ne_mem_ball, circleMap_neg_pi_div_two, circleMap_notMem_ball, circleMap_pi_div_two, circleMap_sub_center, circleMap_zero, circleMap_zero_div, circleMap_zero_inv, circleMap_zero_mul, circleMap_zero_pow, circleMap_zero_radius, circleMap_zero_zpow, eq_of_circleMap_eq, injOn_circleMap_of_abs_sub_le, injOn_circleMap_of_abs_sub_le', norm_circleMap_zero, periodic_circleMap	24
Total	25

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_circleMap 📖	mathematical	—	Set.Countable Real Set.preimage Complex circleMap	—	preimage preimage_cexp add_right_injective AddLeftCancelSemigroup.toIsLeftCancelAdd mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Complex.ofReal_ne_zero mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero Complex.I_ne_zero Complex.ofReal_injective

(root)

Definitions

Name	Category	Theorems
circleMap 📖	CompOp	47 math math: Polynomial.mahlerMeasure_def_of_ne_zero, Complex.circleTransformDeriv_eq, range_circleMap, circleIntegral_def_Icc, circleIntegrable_iff, circleMap_neg_pi_div_two, analyticOnNhd_circleMap, circleMap_zero_inv, circleMap_sub_center, image_circleMap_Ioc, circleMap_eq_circleMap_iff, norm_circleMap_zero, contDiff_circleMap, measurable_circleMap, injOn_circleMap_of_abs_sub_le', circleMap_pi_div_two, norm_cauchyPowerSeries_le, Polynomial.intervalIntegrable_mahlerMeasure, lipschitzWith_circleMap, circleMap_notMem_ball, continuous_circleMap, Real.circleAverage_def, Real.circleAverage_eq_integral_add, periodic_circleMap, circleMap_mem_sphere, circleMap_preimage_codiscrete, circleMap_mem_closedBall, hasDerivAt_circleMap, circleMap_neg_radius, circleMap_zero, deriv_circleMap, circleMap_zero_mul, Complex.continuousOn_prod_circle_transform_function, circleMap_zero_div, injOn_circleMap_of_abs_sub_le, circleMap_eq_center_iff, Set.Countable.preimage_circleMap, Real.circleAverage_eq_intervalAverage, circleIntegrable_def, circleMap_zero_radius, circleMap_zero_pow, CircleIntegrable.out, deriv_circleMap_eq_zero_iff, circleMap_mem_sphere', continuous_circleMap_inv, differentiable_circleMap, circleMap_zero_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleMap_eq_center_iff 📖	mathematical	—	circleMap Real Real.instZero	—	AddLeftCancelSemigroup.toIsLeftCancelAdd NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
circleMap_eq_circleMap_iff 📖	mathematical	—	circleMap Complex Complex.instMul Complex.ofReal Complex.I Complex.instAdd Complex.instIntCast instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	AddLeftCancelSemigroup.toIsLeftCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Complex.norm_exp_ofReal_mul_I Complex.norm_real norm_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Complex.arg_zero Nat.instAtLeastTwoHAddOfNat div_self NeZero.charZero_one Complex.instCharZero one_mul
circleMap_mem_closedBall 📖	mathematical	Real Real.instLE Real.instZero	Complex Set Set.instMembership Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField circleMap	—	Metric.sphere_subset_closedBall circleMap_mem_sphere
circleMap_mem_sphere 📖	mathematical	Real Real.instLE Real.instZero	Complex Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField circleMap	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid circleMap_mem_sphere'
circleMap_mem_sphere' 📖	mathematical	—	Complex Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField abs Real Real.lattice Real.instAddGroup circleMap	—	circleMap_sub_center norm_circleMap_zero
circleMap_ne_center 📖	—	—	—	—	circleMap_eq_center_iff
circleMap_ne_mem_ball 📖	—	Complex Set Set.instMembership Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	—	circleMap_notMem_ball
circleMap_neg_pi_div_two 📖	mathematical	—	circleMap Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex Complex.instSub Complex.instMul Complex.ofReal Complex.I	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_div Complex.ofReal_neg Complex.exp_neg_pi_div_two_mul_I mul_neg sub_eq_add_neg
circleMap_notMem_ball 📖	mathematical	—	Complex Set Set.instMembership Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField circleMap	—	circleMap_sub_center norm_circleMap_zero
circleMap_pi_div_two 📖	mathematical	—	circleMap Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex Complex.instAdd Complex.instMul Complex.ofReal Complex.I	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_div Complex.exp_pi_div_two_mul_I
circleMap_sub_center 📖	mathematical	—	Complex Complex.instSub circleMap Complex.instZero	—	add_sub_cancel_left zero_add
circleMap_zero 📖	mathematical	—	circleMap Complex Complex.instZero Complex.instMul Complex.ofReal Complex.exp Complex.I	—	zero_add
circleMap_zero_div 📖	mathematical	—	Complex DivInvMonoid.toDiv Complex.instDivInvMonoid circleMap Complex.instZero Real Real.instDivInvMonoid Real.instSub	—	circleMap_zero Complex.ofReal_div Complex.ofReal_sub sub_mul Complex.exp_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.zero_mul Mathlib.Tactic.Ring.div_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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw
circleMap_zero_inv 📖	mathematical	—	Complex Complex.instInv circleMap Complex.instZero Real Real.instInv Real.instNeg	—	circleMap_zero mul_comm mul_inv_rev Complex.ofReal_inv Complex.ofReal_neg mul_neg Complex.exp_neg
circleMap_zero_mul 📖	mathematical	—	Complex Complex.instMul circleMap Complex.instZero Real Real.instMul Real.instAdd	—	circleMap_zero Complex.ofReal_mul Complex.ofReal_add add_mul Distrib.rightDistribClass Complex.exp_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.zero_mul
circleMap_zero_pow 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring circleMap Complex.instZero Real Real.instMonoid Real.instMul Real.instNatCast	—	circleMap_zero mul_pow Complex.ofReal_pow Complex.ofReal_mul
circleMap_zero_radius 📖	mathematical	—	circleMap Real Real.instZero Complex	—	circleMap_eq_center_iff
circleMap_zero_zpow 📖	mathematical	—	Complex DivInvMonoid.toZPow Complex.instDivInvMonoid circleMap Complex.instZero Real Real.instDivInvMonoid Real.instMul Real.instIntCast	—	circleMap_zero mul_zpow Complex.ofReal_zpow Complex.ofReal_mul
eq_of_circleMap_eq 📖	—	Real Real.instLT abs Real.lattice Real.instAddGroup Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi circleMap	—	—	Nat.instAtLeastTwoHAddOfNat circleMap_eq_circleMap_iff Int.cast_ofNat Int.cast_mul Complex.ofReal_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.mul_pf_left Mathlib.Tactic.Ring.one_mul Distrib.rightDistribClass IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Int.abs_lt_one_iff Nat.cast_one Real.instIsStrictOrderedRing Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsStrictOrderedRing.toMulPosStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE mul_pos IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Real.pi_pos mul_assoc add_sub_cancel_left abs_mul Nat.abs_ofNat abs_of_pos MulZeroClass.zero_mul Int.cast_zero add_zero
injOn_circleMap_of_abs_sub_le 📖	mathematical	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	Set.InjOn Complex circleMap Set.uIoc Real.linearOrder	—	Nat.instAtLeastTwoHAddOfNat eq_of_circleMap_eq abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr 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 Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt sub_eq_zero_of_eq max_sub_min_eq_abs' Mathlib.Tactic.Linarith.add_nonpos
injOn_circleMap_of_abs_sub_le' 📖	mathematical	Real Real.instLE Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	Set.InjOn Complex circleMap Set.Ico Real.instPreorder	—	Nat.instAtLeastTwoHAddOfNat eq_of_circleMap_eq abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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.atom_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.add_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt
norm_circleMap_zero 📖	mathematical	—	Norm.norm Complex Complex.instNorm circleMap Complex.instZero abs Real Real.lattice Real.instAddGroup	—	zero_add Complex.norm_mul Complex.norm_real Complex.norm_exp_ofReal_mul_I mul_one
periodic_circleMap 📖	mathematical	—	Function.Periodic Real Complex Real.instAdd circleMap Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_add Complex.ofReal_mul add_mul Distrib.rightDistribClass Complex.exp_periodic

---

← Back to Index