PhragmenLindelof

📁 Source: Mathlib/Analysis/Complex/PhragmenLindelof.lean

Statistics

Metric	Count
Definitions	0
Theorems eqOn_horizontal_strip, eqOn_quadrant_I, eqOn_quadrant_II, eqOn_quadrant_III, eqOn_quadrant_IV, eqOn_right_half_plane_of_superexponential_decay, eqOn_vertical_strip, eq_zero_on_horizontal_strip, eq_zero_on_quadrant_I, eq_zero_on_quadrant_II, eq_zero_on_quadrant_III, eq_zero_on_quadrant_IV, eq_zero_on_right_half_plane_of_superexponential_decay, eq_zero_on_vertical_strip, horizontal_strip, isBigO_sub_exp_exp, isBigO_sub_exp_rpow, quadrant_I, quadrant_II, quadrant_III, quadrant_IV, right_half_plane_of_bounded_on_real, right_half_plane_of_tendsto_zero_on_real, vertical_strip	24
Total	24

PhragmenLindelof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_horizontal_strip 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.preimage Real Complex.im Set.Ioo Real.instPreorder Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instSub Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Filter.comap abs Real.lattice Real.instAddGroup Complex.re Filter.atTop Filter.principal Real.exp Real.instMul	Set.EqOn Set.Icc	—	sub_eq_zero eq_zero_on_horizontal_strip DiffContOnCl.sub isBigO_sub_exp_exp
eqOn_quadrant_I 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Ioi Real Real.instPreorder Real.instZero Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal Complex.instMul Complex.I	Set.EqOn setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat sub_eq_zero eq_zero_on_quadrant_I DiffContOnCl.sub isBigO_sub_exp_rpow
eqOn_quadrant_II 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Iio Real Real.instPreorder Real.instZero Set.Ioi Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal Complex.instMul Complex.I	Set.EqOn setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat sub_eq_zero eq_zero_on_quadrant_II DiffContOnCl.sub isBigO_sub_exp_rpow
eqOn_quadrant_III 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Iio Real Real.instPreorder Real.instZero Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal Complex.instMul Complex.I	Set.EqOn setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat sub_eq_zero eq_zero_on_quadrant_III DiffContOnCl.sub isBigO_sub_exp_rpow
eqOn_quadrant_IV 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Ioi Real Real.instPreorder Real.instZero Set.Iio Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal Complex.instMul Complex.I	Set.EqOn setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat sub_eq_zero eq_zero_on_quadrant_IV DiffContOnCl.sub isBigO_sub_exp_rpow
eqOn_right_half_plane_of_superexponential_decay 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace setOf Real Real.instLT Real.instZero Complex.re instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Asymptotics.SuperpolynomialDecay UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instCommSemiring Filter.atTop Real.instPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Complex.ofReal Real.instLE Complex.instMul Complex.I	Set.EqOn	—	Nat.instAtLeastTwoHAddOfNat eq_zero_on_right_half_plane_of_superexponential_decay DiffContOnCl.sub isBigO_sub_exp_rpow norm_sub_le_of_le
eqOn_vertical_strip 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.preimage Real Complex.re Set.Ioo Real.instPreorder Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instSub Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Filter.comap abs Real.lattice Real.instAddGroup Complex.im Filter.atTop Filter.principal Real.exp Real.instMul	Set.EqOn Set.Icc	—	sub_eq_zero eq_zero_on_vertical_strip DiffContOnCl.sub isBigO_sub_exp_exp
eq_zero_on_horizontal_strip 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.preimage Real Complex.im Set.Ioo Real.instPreorder Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instSub Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Filter.comap abs Real.lattice Real.instAddGroup Complex.re Filter.atTop Filter.principal Real.exp Real.instMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Set.EqOn Pi.instZero Set.Icc	—	norm_le_zero_iff horizontal_strip Eq.le norm_zero
eq_zero_on_quadrant_I 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Ioi Real Real.instPreorder Real.instZero Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Complex.instMul Complex.I	Set.EqOn Pi.instZero setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat norm_le_zero_iff quadrant_I
eq_zero_on_quadrant_II 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Iio Real Real.instPreorder Real.instZero Set.Ioi Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Complex.instMul Complex.I	Set.EqOn Pi.instZero setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat norm_le_zero_iff quadrant_II
eq_zero_on_quadrant_III 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Iio Real Real.instPreorder Real.instZero Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Complex.instMul Complex.I	Set.EqOn Pi.instZero setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat norm_le_zero_iff quadrant_III
eq_zero_on_quadrant_IV 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Ioi Real Real.instPreorder Real.instZero Set.Iio Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Complex.ofReal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Complex.instMul Complex.I	Set.EqOn Pi.instZero setOf Real.instLE Complex.re Complex.im	—	Nat.instAtLeastTwoHAddOfNat norm_le_zero_iff quadrant_IV
eq_zero_on_right_half_plane_of_superexponential_decay 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace setOf Real Real.instLT Real.instZero Complex.re instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Asymptotics.SuperpolynomialDecay UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instCommSemiring Filter.atTop Real.instPreorder Complex.ofReal Real.instLE Complex.instMul Complex.I	Set.EqOn Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat norm_smul NormedSpace.toNormSMulClass norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Complex.norm_exp right_half_plane_of_tendsto_zero_on_real DiffContOnCl.smul IsScalarTower.left Differentiable.diffContOnCl Differentiable.pow Complex.differentiable_exp max_lt one_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Asymptotics.IsBigO.of_norm_left Asymptotics.IsBigO.trans Asymptotics.IsBigO.mul Asymptotics.isBigO_refl Asymptotics.IsBigO.norm_left Asymptotics.IsBigO.of_bound' Filter.mp_mem Filter.Eventually.filter_mono inf_le_left eventually_cobounded_le_norm Filter.univ_mem' Real.abs_exp add_mul Distrib.rightDistribClass Real.exp_monotone add_le_add covariant_swap_add_of_covariant_add mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Complex.re_le_norm Real.rpow_one Real.rpow_le_rpow_of_exponent_le le_max_right Nat.cast_nonneg' mul_le_mul IsOrderedRing.toMulPosMono le_max_left le_of_lt Real.rpow_pos_of_pos lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_max_of_le_right Mathlib.Meta.Positivity.nonneg_of_isNat Nat.cast_zero tendsto_zero_iff_norm_tendsto_zero Complex.re_ofReal_mul Complex.I_re MulZeroClass.mul_zero Real.exp_zero one_pow one_mul LT.lt.le Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually Filter.Tendsto.atTop_mul_const Real.instIsStrictOrderedRing norm_pos_iff tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean Real.one_lt_exp_iff Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Complex.closure_setOf_lt_re Set.EqOn.of_subset_closure TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace DiffContOnCl.continuousOn continuousOn_const subset_closure Set.Subset.rfl
eq_zero_on_vertical_strip 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.preimage Real Complex.re Set.Ioo Real.instPreorder Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instSub Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Filter.comap abs Real.lattice Real.instAddGroup Complex.im Filter.atTop Filter.principal Real.exp Real.instMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Set.EqOn Pi.instZero Set.Icc	—	norm_le_zero_iff vertical_strip Eq.le norm_zero
horizontal_strip 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.preimage Real Complex.im Set.Ioo Real.instPreorder Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instSub Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Filter.comap abs Real.lattice Real.instAddGroup Complex.re Filter.atTop Filter.principal Real.exp Real.instMul Real.instLE Norm.norm	—	—	le_iff_eq_or_lt Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add LT.lt.trans sub_eq_add_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_div_two_pos div_mul_eq_div_div two_mul add_sub_sub_cancel exists_between LinearOrderedSemiField.toDenselyOrdered max_lt lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' mul_neg_of_neg_of_pos Real.cos_pos_of_mem_Ioo abs_lt covariant_swap_add_of_covariant_add abs_of_pos mul_pos Complex.im_ofReal_mul Complex.sub_im Complex.mul_I_im Complex.ofReal_re abs_mul Real.instIsOrderedRing mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.dist_eq Metric.mem_closedBall Real.closedBall_eq_Icc le_of_lt Complex.re_ofReal_mul Complex.mul_I_re neg_zero sub_zero Complex.norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le LT.lt.le LE.le.trans Set.left_mem_Icc Set.right_mem_Icc Real.exp_le_one_iff mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono Real.exp_pos Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder Real.instArchimedean Filter.Eventually.and Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial Asymptotics.IsBigO.exists_pos Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul tendsto_inv_atTop_zero instOrderTopologyReal Real.tendsto_exp_atTop Filter.Tendsto.const_mul_atTop sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Filter.tendsto_id Filter.Tendsto.atBot_add add_mul Distrib.rightDistribClass mul_assoc sub_sub_cancel Filter.Tendsto.neg_mul_atTop add_zero MulZeroClass.mul_zero Filter.Tendsto.eventually ge_mem_nhds norm_smul NormedSpace.toNormSMulClass Real.exp_add Real.exp_log mul_comm mul_le_mul Set.Ioo_subset_Icc_self norm_nonneg LE.le.trans_lt abs_nonneg Differentiable.cexp Differentiable.const_mul Differentiable.add Differentiable.sub_const differentiable_id Differentiable.neg DiffContOnCl.mono DiffContOnCl.smul IsScalarTower.left Differentiable.diffContOnCl Set.inter_subset_right Complex.norm_le_of_forall_mem_frontier_norm_le Complex.instNontrivial Bornology.IsBounded.reProdIm Metric.isBounded_Ioo ConditionallyCompleteLinearOrder.toCompactIccSpace one_mul zero_le_one Real.instZeroLEOneClass frontier_Ioo neg_lt_self closure_Ioo LT.lt.ne Complex.frontier_reProdIm Set.eq_endpoints_or_mem_Ioo_of_mem_Icc abs_eq Complex.closure_reProdIm abs_le le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal nhdsLT_neBot instNoMinOrderOfNontrivial Filter.Tendsto.mono_left Continuous.tendsto' Continuous.norm Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.cexp Continuous.mul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.continuous_ofReal continuous_const MulZeroClass.zero_mul Complex.exp_zero one_smul nhdsWithin_le_nhds le_of_forall_gt_imp_ge_of_dense
isBigO_sub_exp_exp 📖	mathematical	Real Real.instLT Asymptotics.IsBigO Complex NormedAddCommGroup.toNorm Real.norm Real.exp Real.instMul abs Real.lattice Real.instAddGroup	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Real.abs_exp Real.exp_monotone mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono mul_le_mul_of_nonneg_right abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_of_lt Real.exp_pos max_lt Asymptotics.IsBigO.sub Asymptotics.IsBigO.trans_le le_max_left LE.le.trans le_max_right
isBigO_sub_exp_rpow 📖	mathematical	Real Real.instLT Asymptotics.IsBigO Complex NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Asymptotics.IsBigO.of_norm_eventuallyLE Filter.mp_mem Filter.Eventually.filter_mono inf_le_left eventually_cobounded_le_norm Filter.univ_mem' Real.abs_exp Real.exp_monotone mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Real.rpow_le_rpow_of_exponent_le le_of_lt Real.rpow_pos_of_pos lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one max_lt Asymptotics.IsBigO.sub Asymptotics.IsBigO.trans le_max_left LE.le.trans le_max_right
quadrant_I 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Ioi Real Real.instPreorder Real.instZero Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Real.instLE Complex.ofReal Complex.instMul Complex.I Complex.re Complex.im	—	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne le_rfl Complex.log_im Complex.arg_nonneg_iff Complex.arg_le_pi_div_two_iff Complex.exp_log Complex.mem_reProdIm Complex.exp_re Complex.exp_im Set.mem_Ioi Real.cos_pos_of_mem_Ioo lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.neg_congr Nat.cast_one Mathlib.Tactic.Ring.one_mul 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg CancelDenoms.sub_subst CancelDenoms.neg_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.sin_pos_of_mem_Ioo LT.lt.trans half_lt_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.pi_pos mul_pos Real.exp_pos horizontal_strip DiffContOnCl.comp Differentiable.diffContOnCl Complex.differentiable_exp sub_zero div_div_cancel₀ LT.lt.ne' Filter.comap_comap Filter.comap_abs_atTop Real.instIsOrderedAddMonoid Filter.comap_sup inf_sup_right Asymptotics.IsBigO.sup ContinuousWithinAt.mono DiffContOnCl.continuousOn Complex.closure_reProdIm closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered instNoMaxOrderOfNontrivial Real.instNontrivial subset_closure Asymptotics.IsBigO.trans Filter.Tendsto.isBigO_one NormedDivisionRing.to_normOneClass Filter.Tendsto.comp ContinuousWithinAt.tendsto Filter.Tendsto.inf Complex.tendsto_exp_comap_re_atBot Set.MapsTo.tendsto Asymptotics.isBigO_of_le NormOneClass.norm_one Real.norm_of_nonneg LT.lt.le Real.one_le_exp_iff mul_nonneg IsOrderedRing.toPosMulMono le_max_of_le_right Mathlib.Meta.Positivity.nonneg_of_isNat le_of_lt Asymptotics.IsBigO.comp_tendsto Complex.tendsto_exp_comap_re_atTop Asymptotics.IsBigO.of_norm_eventuallyLE Complex.norm_exp Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono mul_comm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono le_max_left CanLift.prf Complex.canLift Complex.ofReal_exp Complex.re_add_im Complex.exp_add_mul_I Complex.ofReal_cos Complex.ofReal_sin Real.cos_pi_div_two Real.sin_pi_div_two Complex.ofReal_zero Complex.ofReal_one one_mul zero_add
quadrant_II 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Iio Real Real.instPreorder Real.instZero Set.Ioi Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Real.instLE Complex.ofReal Complex.instMul Complex.I Complex.re Complex.im	—	—	Nat.instAtLeastTwoHAddOfNat div_mul_cancel₀ Complex.I_ne_zero Complex.mul_I_re IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Complex.mul_I_im quadrant_I DiffContOnCl.comp Differentiable.diffContOnCl Differentiable.mul_const differentiable_id norm_mul NormedDivisionRing.toNormMulClass Complex.norm_I mul_one Asymptotics.IsBigO.comp_tendsto Filter.Tendsto.inf Filter.tendsto_mul_right_cobounded Set.MapsTo.tendsto mul_assoc Complex.I_mul_I mul_neg_one Complex.ofReal_neg neg_nonpos
quadrant_III 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Iio Real Real.instPreorder Real.instZero Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Real.instLE Complex.ofReal Complex.instMul Complex.I Complex.re Complex.im	—	—	Nat.instAtLeastTwoHAddOfNat neg_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid quadrant_I DiffContOnCl.comp Differentiable.diffContOnCl differentiable_neg norm_neg Asymptotics.IsBigO.comp_tendsto Filter.Tendsto.inf Filter.tendsto_neg_cobounded Set.MapsTo.tendsto Complex.ofReal_neg neg_nonpos neg_mul
quadrant_IV 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.reProdIm Set.Ioi Real Real.instPreorder Real.instZero Set.Iio Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Real.instLE Complex.ofReal Complex.instMul Complex.I Complex.re Complex.im	—	—	Nat.instAtLeastTwoHAddOfNat neg_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid quadrant_II DiffContOnCl.comp Differentiable.diffContOnCl differentiable_neg norm_neg Asymptotics.IsBigO.comp_tendsto Filter.Tendsto.inf Filter.tendsto_neg_cobounded Set.MapsTo.tendsto Complex.ofReal_neg neg_nonneg neg_mul neg_nonpos
right_half_plane_of_bounded_on_real 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace setOf Real Real.instLT Real.instZero Complex.re instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Filter.IsBoundedUnder Real.instLE Filter.atTop Real.instPreorder Complex.ofReal Complex.instMul Complex.I	—	—	Nat.instAtLeastTwoHAddOfNat Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' DiffContOnCl.smul IsScalarTower.left Differentiable.diffContOnCl Differentiable.cexp Differentiable.const_mul differentiable_id norm_smul NormedSpace.toNormSMulClass Complex.norm_exp Complex.re_ofReal_mul right_half_plane_of_tendsto_zero_on_real Asymptotics.IsBigO.trans Asymptotics.IsBigO.of_bound' Filter.eventually_inf_principal Filter.Eventually.of_forall mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg Real.exp_le_one_iff mul_nonpos_of_nonpos_of_nonneg LT.lt.le le_of_lt Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.Tendsto.neg_mul_atTop Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_const_nhds Filter.tendsto_id Filter.Tendsto.zero_smul_isBoundedUnder_le Complex.I_re MulZeroClass.mul_zero Real.exp_zero one_mul le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid nhdsLT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instNontrivial Filter.Tendsto.mono_left Continuous.tendsto' Continuous.norm Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.cexp Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_id' continuous_const Complex.continuous_ofReal MulZeroClass.zero_mul Complex.exp_zero one_smul nhdsWithin_le_nhds
right_half_plane_of_tendsto_zero_on_real 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace setOf Real Real.instLT Real.instZero Complex.re instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.principal Real.exp Real.instMul Real.instPow Norm.norm Complex.instNorm Filter.Tendsto Complex.ofReal Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instLE Complex.instMul Complex.I	—	—	Nat.instAtLeastTwoHAddOfNat ContinuousOn.comp DiffContOnCl.continuousOn Continuous.continuousOn Complex.continuous_ofReal Complex.closure_setOf_lt_re le_rfl le_refl Mathlib.Tactic.Push.not_forall_eq norm_zero norm_pos_iff cocompact_eq_atBot_atTop instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMinOrderOfNontrivial HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal inf_sup_right Disjoint.eq_bot Filter.disjoint_atBot_principal_Ici instNoBotOrderOfNoMinOrder bot_sup_eq Filter.Eventually.filter_mono inf_le_left Filter.Tendsto.eventually Filter.Tendsto.norm ge_mem_nhds ContinuousOn.exists_isMaxOn' instClosedIciTopology ContinuousOn.norm isClosed_Ici le_or_gt max_eq_left le_total quadrant_IV DiffContOnCl.mono Asymptotics.IsBigO.mono inf_le_inf_left Filter.principal_mono LE.le.trans le_max_right le_max_left quadrant_I max_eq_right LT.lt.le Complex.norm_eq_norm_of_isMaxOn_of_ball_subset Set.mem_setOf_eq Mathlib.Tactic.Contrapose.contrapose₁ le_sub_self_iff IsOrderedAddMonoid.toAddLeftMono le_abs_self Complex.sub_re Complex.ofReal_re abs_sub_comm Complex.abs_re_le_norm Complex.norm_of_nonneg Complex.dist_eq dist_zero_left Metric.mem_ball LT.lt.not_ge MulZeroClass.zero_mul
vertical_strip 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.preimage Real Complex.re Set.Ioo Real.instPreorder Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instSub Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter Filter.instInf Filter.comap abs Real.lattice Real.instAddGroup Complex.im Filter.atTop Filter.principal Real.exp Real.instMul Real.instLE Norm.norm	—	—	mul_neg MulZeroClass.mul_zero mul_one zero_sub neg_neg horizontal_strip DiffContOnCl.comp Differentiable.diffContOnCl Differentiable.mul_const differentiable_id Filter.Tendsto.inf Filter.tendsto_comap_iff add_zero abs_neg Filter.tendsto_comap Set.MapsTo.tendsto Asymptotics.IsBigO.comp_tendsto mul_assoc Complex.I_mul_I

---

← Back to Index