Documentation Verification Report

Exp

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

Statistics

Metric	Count
Definitions	0
Theorems `im_invQParam_pos_of_norm_lt_one`, `norm_qParam_le_of_one_half_le_im`, `norm_exp_two_pi_I_lt_one`, `norm_qParam_lt_one`	4
Total	4

Function.Periodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`im_invQParam_pos_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Norm.norm` `Complex` `Complex.instNorm` `Real.instOne`	`Complex.im` `invQParam`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `div_neg_of_neg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Real.two_pi_pos` `Real.log_neg_iff` `norm_pos_iff` `im_invQParam`
`norm_qParam_le_of_one_half_le_im` 📖	mathematical	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.im`	`Norm.norm` `Complex` `Complex.instNorm` `qParam` `Real.exp` `Real.instNeg` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `qParam.eq_1` `Complex.ofReal_one` `div_one` `Complex.norm_exp` `Real.exp_le_exp` `mul_right_comm` `Complex.mul_I_re` `neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Complex.ofReal_ofNat` `Complex.ofReal_mul` `Complex.im_ofReal_mul` `mul_comm` `mul_assoc` `le_mul_iff_one_le_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.pi_pos` `div_le_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `two_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`

UpperHalfPlane

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_exp_two_pi_I_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Complex.exp` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `coe` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `Complex.norm_exp` `MulZeroClass.mul_zero` `sub_zero` `MulZeroClass.zero_mul` `add_zero` `mul_one` `sub_self` `zero_sub` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_one` `Function.Periodic.norm_qParam` `neg_mul` `div_one` `norm_qParam_lt_one`
`norm_qParam_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Function.Periodic.qParam` `Real.instNatCast` `coe` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `Function.Periodic.norm_qParam` `Real.exp_lt_one_iff` `neg_mul` `coe_im` `neg_div` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_pos_iff_of_pos_right` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.pi_pos` `im_pos`

---

← Back to Index