PerronFormula

📁 Source: PrimeNumberTheoremAnd/PerronFormula.lean

Statistics

Metric	Count
Definitions `f`	1
Theorems `cpow_eq_exp_log_ofReal`, `cpow_neg_eq_inv_pow_ofReal_pos`, `eventually_bddAbove`, `lowerUIntegral_eq_zero`, `upperUIntegral_eq_zero`, `one_div_const_add_sq`, `bddAbove_square_of_tendsto`, `contourPull`, `contourPull3`, `diffBddAtNegOne`, `diffBddAtZero`, `f_mul_eq_f`, `formulaGtOne`, `formulaLtOne`, `horizontal_integral_isBigO`, `integralPosAux`, `integralPosAux'`, `integralPosAux'_of_le`, `integral_one_div_const_add_sq_pos`, `isHolomorphicOn`, `isIntegrable`, `isTheta`, `isTheta_uniformlyOn_uIcc`, `isTheta_uniformlyOn_uIoc`, `keyIdentity`, `map_conj`, `residueAtNegOne`, `residueAtZero`, `residuePull1`, `residuePull2`, `sPlusOneNeZero`, `tendsto_zero_Lower`, `tendsto_zero_Upper`, `vertIntBound`, `vertIntBoundLeft`, `RectangleIntegral_tendsTo_LowerU`, `RectangleIntegral_tendsTo_UpperU`, `RectangleIntegral_tendsTo_VerticalIntegral`, `limitOfConstant`, `limitOfConstantLeft`, `tendsto_rpow_atTop_nhds_zero_of_norm_gt_one`, `tendsto_rpow_atTop_nhds_zero_of_norm_lt_one`, `verticalIntegral_eq_verticalIntegral`, `verticalIntegral_sub_verticalIntegral_eq_squareIntegral`, `zeroTendstoDiff`	45
Total	46

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cpow_eq_exp_log_ofReal` 📖	—	—	—	—	—
`cpow_neg_eq_inv_pow_ofReal_pos` 📖	—	—	—	—	—

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_bddAbove` 📖	—	—	—	—	—

Perron

Definitions

Name	Category	Theorems
`f` 📖	CompOp	17 math math: `residuePull1`, `formulaLtOne`, `vertIntBoundLeft`, `tendsto_zero_Upper`, `horizontal_integral_isBigO`, `f_mul_eq_f`, `contourPull`, `residueAtNegOne`, `map_conj`, `isTheta_uniformlyOn_uIoc`, `isTheta_uniformlyOn_uIcc`, `isHolomorphicOn`, `vertIntBound`, `residueAtZero`, `tendsto_zero_Lower`, `isTheta`, `isIntegrable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_square_of_tendsto` 📖	mathematical	—	`Square`	—	`Filter.Tendsto.eventually_bddAbove` `Complex.nhds_hasBasis_square` `square_subset_square`
`contourPull` 📖	mathematical	—	`VerticalIntegral` `f`	—	`verticalIntegral_eq_verticalIntegral` `isHolomorphicOn` `tendsto_zero_Lower` `tendsto_zero_Upper` `isIntegrable`
`contourPull3` 📖	mathematical	—	`VerticalIntegral'`	—	`contourPull`
`diffBddAtNegOne` 📖	mathematical	—	`Square`	—	`bddAbove_square_of_tendsto` `keyIdentity`
`diffBddAtZero` 📖	mathematical	—	`Square`	—	`bddAbove_square_of_tendsto` `keyIdentity`
`f_mul_eq_f` 📖	mathematical	—	`f`	—	`Complex.cpow_neg_eq_inv_pow_ofReal_pos`
`formulaGtOne` 📖	mathematical	—	`VerticalIntegral'`	—	`residuePull1` `residuePull2` `contourPull3` `vertIntBoundLeft` `tendsto_rpow_atTop_nhds_zero_of_norm_gt_one` `limitOfConstantLeft`
`formulaLtOne` 📖	mathematical	—	`VerticalIntegral` `f`	—	`contourPull` `integralPosAux` `vertIntBound` `tendsto_rpow_atTop_nhds_zero_of_norm_lt_one` `limitOfConstant`
`horizontal_integral_isBigO` 📖	mathematical	—	`f`	—	`isTheta_uniformlyOn_uIoc`
`integralPosAux` 📖	—	—	—	—	`integralPosAux'`
`integralPosAux'` 📖	—	—	—	—	`integralPosAux'_of_le`
`integralPosAux'_of_le` 📖	—	—	—	—	`integral_one_div_const_add_sq_pos` `Integrable.one_div_const_add_sq`
`integral_one_div_const_add_sq_pos` 📖	—	—	—	—	—
`isHolomorphicOn` 📖	mathematical	—	`HolomorphicOn` `f`	—	—
`isIntegrable` 📖	mathematical	—	`f`	—	`isHolomorphicOn` `map_conj` `isTheta`
`isTheta` 📖	mathematical	—	`f`	—	`Asymptotics.isTheta_of_isThetaUniformly` `isTheta_uniformlyOn_uIcc`
`isTheta_uniformlyOn_uIcc` 📖	mathematical	—	`f`	—	`ContinuousOn.const_isThetaUniformlyOn_isCompact` `Asymptotics.isLittleO_const_snd_atBot` `Asymptotics.isLittleO_const_snd_atTop` `ContinuousOn.const_isBigOUniformlyOn_isCompact`
`isTheta_uniformlyOn_uIoc` 📖	mathematical	—	`f`	—	`isTheta_uniformlyOn_uIcc`
`keyIdentity` 📖	—	—	—	—	—
`map_conj` 📖	mathematical	—	`f`	—	—
`residueAtNegOne` 📖	mathematical	—	`RectangleIntegral'` `f`	—	`diffBddAtNegOne` `mem_Rect` `Square.eq_1` `isHolomorphicOn` `sPlusOneNeZero` `square_mem_nhds` `existsDifferentiableOn_of_bddAbove` `ResidueTheoremOnRectangleWithSimplePole`
`residueAtZero` 📖	mathematical	—	`RectangleIntegral'` `f`	—	`diffBddAtZero` `mem_Rect` `Square.eq_1` `isHolomorphicOn` `square_mem_nhds` `existsDifferentiableOn_of_bddAbove` `ResidueTheoremOnRectangleWithSimplePole`
`residuePull1` 📖	mathematical	—	`VerticalIntegral'` `f`	—	`isHolomorphicOn` `residueAtZero` `verticalIntegral_sub_verticalIntegral_eq_squareIntegral` `tendsto_zero_Lower` `tendsto_zero_Upper` `isIntegrable` `VerticalIntegral'.eq_1` `RectangleIntegral'.eq_1`
`residuePull2` 📖	mathematical	—	`VerticalIntegral'`	—	`isHolomorphicOn` `residueAtNegOne` `verticalIntegral_sub_verticalIntegral_eq_squareIntegral` `tendsto_zero_Lower` `tendsto_zero_Upper` `isIntegrable` `VerticalIntegral'.eq_1` `RectangleIntegral'.eq_1`
`sPlusOneNeZero` 📖	—	—	—	—	—
`tendsto_zero_Lower` 📖	mathematical	—	`f`	—	`horizontal_integral_isBigO`
`tendsto_zero_Upper` 📖	mathematical	—	`f`	—	`horizontal_integral_isBigO`
`vertIntBound` 📖	mathematical	—	`VerticalIntegral` `f`	—	`integralPosAux`
`vertIntBoundLeft` 📖	mathematical	—	`VerticalIntegral'` `f`	—	`integralPosAux'`

Perron.HolomorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lowerUIntegral_eq_zero` 📖	mathematical	`HolomorphicOn`	`LowerUIntegral`	—	`RectangleIntegral_tendsTo_LowerU` `HolomorphicOn.vanishesOnRectangle` `mem_Rect`
`upperUIntegral_eq_zero` 📖	mathematical	`HolomorphicOn`	`UpperUIntegral`	—	`RectangleIntegral_tendsTo_UpperU` `HolomorphicOn.vanishesOnRectangle` `mem_Rect`

Perron.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_div_const_add_sq` 📖	—	—	—	—	`Perron.integral_one_div_const_add_sq_pos`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`RectangleIntegral_tendsTo_LowerU` 📖	mathematical	—	`RectangleIntegral` `LowerUIntegral`	—	—
`RectangleIntegral_tendsTo_UpperU` 📖	mathematical	—	`RectangleIntegral` `UpperUIntegral`	—	—
`RectangleIntegral_tendsTo_VerticalIntegral` 📖	mathematical	—	`RectangleIntegral` `VerticalIntegral`	—	—
`limitOfConstant` 📖	—	—	—	—	—
`limitOfConstantLeft` 📖	—	—	—	—	—
`tendsto_rpow_atTop_nhds_zero_of_norm_gt_one` 📖	—	—	—	—	`tendsto_rpow_atTop_nhds_zero_of_norm_lt_one`
`tendsto_rpow_atTop_nhds_zero_of_norm_lt_one` 📖	—	—	—	—	—
`verticalIntegral_eq_verticalIntegral` 📖	mathematical	`HolomorphicOn`	`VerticalIntegral`	—	`zeroTendstoDiff` `RectangleIntegral_tendsTo_VerticalIntegral`
`verticalIntegral_sub_verticalIntegral_eq_squareIntegral` 📖	mathematical	`HolomorphicOn`	`VerticalIntegral` `RectangleIntegral`	—	`Complex.nhds_hasBasis_square` `square_subset_square` `RectangleIntegral_tendsTo_VerticalIntegral` `RectanglePullToNhdOfPole'` `square_mem_nhds` `RectSubRect'`
`zeroTendstoDiff` 📖	—	—	—	—	—

---

← Back to Index