Documentation Verification Report

FunctionsBoundedAtInfty

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

Statistics

Metric	Count
Definitions `IsZeroAtImInfty`, `atImInfty`, `boundedAtImInftySubalgebra`, `zeroAtImInftySubmodule`	4
Theorems `isBoundedAtImInfty`, `atImInfty_basis`, `atImInfty_mem`, `instNeBotAtImInfty`, `isBoundedAtImInfty_iff`, `isZeroAtImInfty_iff`, `tendsto_coe_atImInfty`, `tendsto_comap_im_ofComplex`, `tendsto_smul_atImInfty`, `zero_form_isBoundedAtImInfty`	10
Total	14

UpperHalfPlane

Definitions

Name	Category	Theorems
`IsZeroAtImInfty` 📖	MathDef	8 math math: `OnePoint.isZeroAt_iff_exists_SL2Z`, `OnePoint.isZeroAt_infty_iff`, `CuspFormClass.zero_at_infty`, `OnePoint.isZeroAt_iff_forall_SL2Z`, `isZeroAtImInfty_iff`, `CuspFormClass.zero_at_infty_slash`, `OnePoint.isZeroAt_iff`, `IsZeroAtImInfty.of_exp_decay`
`atImInfty` 📖	CompOp	15 math math: `tendsto_smul_atImInfty`, `IsZeroAtImInfty.petersson_exp_decay_left`, `ModularFormClass.exp_decay_sub_atImInfty`, `IsZeroAtImInfty.exp_decay_atImInfty`, `qParam_tendsto_atImInfty`, `atImInfty_mem`, `atImInfty_basis`, `instNeBotAtImInfty`, `CuspFormClass.exp_decay_atImInfty'`, `IsZeroAtImInfty.exp_decay_atImInfty'`, `tendsto_coe_atImInfty`, `CuspFormClass.exp_decay_atImInfty`, `IsZeroAtImInfty.petersson_exp_decay_right`, `tendsto_comap_im_ofComplex`, `ModularFormClass.exp_decay_sub_atImInfty'`
`boundedAtImInftySubalgebra` 📖	CompOp	—
`zeroAtImInftySubmodule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`atImInfty_basis` 📖	mathematical	—	`Filter.HasBasis` `UpperHalfPlane` `Real` `atImInfty` `Set.preimage` `im` `Set.Ici` `Real.instPreorder`	—	`Filter.HasBasis.comap` `Filter.atTop_basis` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean`
`atImInfty_mem` 📖	mathematical	—	`Set` `UpperHalfPlane` `Filter` `Filter.instMembership` `atImInfty` `Set.instMembership`	—	`Filter.HasBasis.mem_iff` `atImInfty_basis`
`instNeBotAtImInfty` 📖	mathematical	—	`Filter.NeBot` `UpperHalfPlane` `atImInfty`	—	`Filter.comap_neBot_iff_frequently` `Filter.Eventually.frequently` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Filter.univ_mem'` `MulZeroClass.mul_zero` `one_mul` `zero_add`
`isBoundedAtImInfty_iff` 📖	mathematical	—	`IsBoundedAtImInfty` `Real` `Real.instLE` `Norm.norm`	—	`CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `mul_one`
`isZeroAtImInfty_iff` 📖	mathematical	—	`IsZeroAtImInfty` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SeminormedAddGroup.toAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Norm.norm` `SeminormedAddGroup.toNorm`	—	`Filter.HasBasis.tendsto_iff` `atImInfty_basis` `Metric.nhds_basis_closedBall` `dist_zero_right`
`tendsto_coe_atImInfty` 📖	mathematical	—	`Filter.Tendsto` `UpperHalfPlane` `Complex` `coe` `atImInfty` `Filter.comap` `Real` `Complex.im` `Filter.atTop` `Real.instPreorder`	—	`coe_im` `Filter.tendsto_comap`
`tendsto_comap_im_ofComplex` 📖	mathematical	—	`Filter.Tendsto` `Complex` `UpperHalfPlane` `OpenPartialHomeomorph.toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instTopologicalSpace` `ofComplex` `Filter.comap` `Real` `Complex.im` `Filter.atTop` `Real.instPreorder` `atImInfty`	—	`Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.preimage_mem_comap` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `ofComplex_apply_of_im_pos` `Filter.tendsto_comap`
`tendsto_smul_atImInfty` 📖	mathematical	`Units.val` `Matrix` `Real` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Real.semiring` `Fin.fintype` `Real.instZero`	`Filter.Tendsto` `UpperHalfPlane` `Matrix.GeneralLinearGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `glAction` `atImInfty`	—	`Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `Filter.tendsto_comap` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Matrix.det_fin_two` `MulZeroClass.mul_zero` `sub_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Matrix.GeneralLinearGroup.det_ne_zero` `Real.instNontrivial` `im_smul` `MulZeroClass.zero_mul` `zero_add` `Complex.div_ofReal_im` `add_zero` `mul_div_right_comm` `abs_mul` `Real.instIsOrderedRing` `abs_div` `abs_of_pos` `im_pos`
`zero_form_isBoundedAtImInfty` 📖	mathematical	—	`IsBoundedAtImInfty` `NormedField.toNorm` `Pi.instZero` `UpperHalfPlane` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`Filter.const_boundedAtFilter`

UpperHalfPlane.IsZeroAtImInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBoundedAtImInfty` 📖	mathematical	`UpperHalfPlane.IsZeroAtImInfty` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SeminormedAddGroup.toAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace`	`UpperHalfPlane.IsBoundedAtImInfty` `SeminormedAddGroup.toNorm`	—	`Filter.ZeroAtFilter.boundedAtFilter`

---

← Back to Index