ResidueCalcOnRectangles

📁 Source: PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean

Statistics

Metric	Count
Definitions `HIntegral`, `HIntegral'`, `HolomorphicOn`, `LowerUIntegral`, `RectangleBorderIntegrable`, `RectangleIntegral`, `RectangleIntegral'`, `UpperUIntegral`, `VIntegral`, `VIntegral'`, `VerticalIntegral`, `VerticalIntegral'`	12
Theorems `BddAbove_on_rectangle_of_bdd_near`, `inv_re_add_im`, `rectangleBorderIntegrable`, `rectangleBorderNoPIntegrable`, `rectangleBorder_integrable`, `DiffVertRect_eq_UpperLowerUs`, `HIntegral_symm`, `rectangleBorderIntegrable`, `rectangleBorderIntegrable'`, `vanishesOnRectangle`, `IsBigO_to_BddAbove`, `add`, `RectangleIntegral'_congr`, `const_mul'`, `const_smul`, `translate`, `translate'`, `RectangleIntegralHSplit`, `RectangleIntegralHSplit'`, `RectangleIntegralVSplit`, `RectangleIntegralVSplit'`, `RectangleIntegral_congr`, `RectanglePullToNhdOfPole`, `RectanglePullToNhdOfPole'`, `RectanglePullToNhdOfPole''`, `ResidueTheoremAtOrigin`, `ResidueTheoremAtOrigin'`, `ResidueTheoremAtOrigin_aux1c`, `ResidueTheoremAtOrigin_aux1c'`, `ResidueTheoremAtOrigin_aux2c`, `ResidueTheoremAtOrigin_aux2c'`, `ResidueTheoremInRectangle`, `ResidueTheoremOnRectangleWithSimplePole`, `ResidueTheoremOnRectangleWithSimplePole'`, `VIntegral_symm`, `continuous_self_div_sq_add_sq`, `existsDifferentiableOn_of_bddAbove`, `integral_const_div_re_add_self`, `integral_const_div_self_add_im`, `integral_const_div_sq_add_sq`, `integral_self_div_sq_add_sq`, `rectangleIntegral_symm`, `rectangleIntegral_symm_re`, `sq_add_sq_ne_zero`, `verticalIntegral_split_three`	45
Total	57

Complex

Theorems

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

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rectangleBorderIntegrable` 📖	mathematical	—	`RectangleBorderIntegrable`	—	`rectangleBorder_integrable` `rectangleBorder_subset_rectangle`
`rectangleBorderNoPIntegrable` 📖	mathematical	`RectangleBorder`	`RectangleBorderIntegrable`	—	`rectangleBorder_integrable` `rectangleBorder_subset_rectangle`
`rectangleBorder_integrable` 📖	mathematical	`RectangleBorder`	`RectangleBorderIntegrable`	—	`mapsTo_rectangleBorder_left_im` `mapsTo_rectangleBorder_right_im` `mapsTo_rectangleBorder_right_re` `mapsTo_rectangleBorder_left_re`

HolomorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rectangleBorderIntegrable` 📖	mathematical	`HolomorphicOn`	`RectangleBorderIntegrable`	—	`ContinuousOn.rectangleBorderIntegrable`
`rectangleBorderIntegrable'` 📖	mathematical	`HolomorphicOn`	`RectangleBorderIntegrable`	—	`ContinuousOn.rectangleBorderNoPIntegrable` `not_mem_rectangleBorder_of_rectangle_mem_nhds`
`vanishesOnRectangle` 📖	mathematical	`HolomorphicOn`	`RectangleIntegral`	—	—

RectangleBorderIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`RectangleBorderIntegrable`	`RectangleIntegral`	—	—

RectangleIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_mul'` 📖	mathematical	—	`RectangleIntegral'`	—	`const_smul`
`const_smul` 📖	mathematical	—	`RectangleIntegral`	—	—
`translate` 📖	mathematical	—	`RectangleIntegral`	—	—
`translate'` 📖	mathematical	—	`RectangleIntegral'`	—	`translate`

(root)

Definitions

Name	Category	Theorems
`HIntegral` 📖	CompOp	1 math math: `HIntegral_symm`
`HIntegral'` 📖	CompOp	—
`HolomorphicOn` 📖	MathDef	8 math math: `MeromorphicOnRectangle.holomorphicOn`, `LogDerivZetaHoloOn`, `HolomorphicOn_riemannZeta0`, `LogDerivZetaHolcLargeT`, `LogDerivZetaHolcSmallT`, `LogDerivZetaBoundedAndHolo`, `Perron.isHolomorphicOn`, `HolomophicOn_riemannZeta`
`LowerUIntegral` 📖	CompOp	3 math math: `Perron.HolomorphicOn.lowerUIntegral_eq_zero`, `RectangleIntegral_tendsTo_LowerU`, `DiffVertRect_eq_UpperLowerUs`
`RectangleBorderIntegrable` 📖	MathDef	5 math math: `ContinuousOn.rectangleBorderNoPIntegrable`, `HolomorphicOn.rectangleBorderIntegrable`, `ContinuousOn.rectangleBorder_integrable`, `HolomorphicOn.rectangleBorderIntegrable'`, `ContinuousOn.rectangleBorderIntegrable`
`RectangleIntegral` 📖	CompOp	19 math math: `ResidueTheoremAtOrigin'`, `RectangleIntegralHSplit'`, `RectangleIntegral_congr`, `RectangleBorderIntegrable.add`, `RectangleIntegral_tendsTo_UpperU`, `RectangleIntegral.const_smul`, `RectanglePullToNhdOfPole`, `RectangleIntegralVSplit`, `RectangleIntegral_tendsTo_LowerU`, `rectangleIntegral_symm`, `rectangleIntegral_symm_re`, `RectangleIntegral_tendsTo_VerticalIntegral`, `RectangleIntegralVSplit'`, `verticalIntegral_sub_verticalIntegral_eq_squareIntegral`, `RectangleIntegralHSplit`, `RectanglePullToNhdOfPole'`, `RectangleIntegral.translate`, `HolomorphicOn.vanishesOnRectangle`, `DiffVertRect_eq_UpperLowerUs`
`RectangleIntegral'` 📖	CompOp	10 math math: `RectanglePullToNhdOfPole''`, `RectangleIntegral'_congr`, `Perron.residueAtNegOne`, `ResidueTheoremAtOrigin`, `RectangleIntegral.translate'`, `ResidueTheoremOnRectangleWithSimplePole'`, `ResidueTheoremOnRectangleWithSimplePole`, `RectangleIntegral.const_mul'`, `Perron.residueAtZero`, `ResidueTheoremInRectangle`
`UpperUIntegral` 📖	CompOp	3 math math: `RectangleIntegral_tendsTo_UpperU`, `Perron.HolomorphicOn.upperUIntegral_eq_zero`, `DiffVertRect_eq_UpperLowerUs`
`VIntegral` 📖	CompOp	4 math math: `verticalIntegral_split_three_finite'`, `verticalIntegral_split_three`, `VIntegral_symm`, `verticalIntegral_split_three_finite`
`VIntegral'` 📖	CompOp	—
`VerticalIntegral` 📖	CompOp	8 math math: `Perron.formulaLtOne`, `Perron.contourPull`, `verticalIntegral_split_three`, `RectangleIntegral_tendsTo_VerticalIntegral`, `verticalIntegral_sub_verticalIntegral_eq_squareIntegral`, `verticalIntegral_eq_verticalIntegral`, `Perron.vertIntBound`, `DiffVertRect_eq_UpperLowerUs`
`VerticalIntegral'` 📖	CompOp	5 math math: `Perron.residuePull1`, `Perron.vertIntBoundLeft`, `Perron.formulaGtOne`, `Perron.residuePull2`, `Perron.contourPull3`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BddAbove_on_rectangle_of_bdd_near` 📖	—	—	—	—	`IsBigO_to_BddAbove`
`DiffVertRect_eq_UpperLowerUs` 📖	mathematical	—	`VerticalIntegral` `RectangleIntegral` `UpperUIntegral` `LowerUIntegral`	—	`verticalIntegral_split_three`
`HIntegral_symm` 📖	mathematical	—	`HIntegral`	—	—
`IsBigO_to_BddAbove` 📖	—	—	—	—	—
`RectangleIntegral'_congr` 📖	mathematical	`RectangleBorder`	`RectangleIntegral'`	—	`RectangleIntegral'.eq_1` `RectangleIntegral_congr`
`RectangleIntegralHSplit` 📖	mathematical	—	`RectangleIntegral`	—	—
`RectangleIntegralHSplit'` 📖	mathematical	`RectangleBorderIntegrable`	`RectangleIntegral`	—	`RectangleIntegralHSplit`
`RectangleIntegralVSplit` 📖	mathematical	—	`RectangleIntegral`	—	—
`RectangleIntegralVSplit'` 📖	mathematical	`RectangleBorderIntegrable`	`RectangleIntegral`	—	`RectangleIntegralVSplit`
`RectangleIntegral_congr` 📖	mathematical	`RectangleBorder`	`RectangleIntegral`	—	—
`RectanglePullToNhdOfPole` 📖	mathematical	`HolomorphicOn`	`RectangleIntegral`	—	`SmallSquareInRectangle` `RectanglePullToNhdOfPole'` `square_mem_nhds`
`RectanglePullToNhdOfPole'` 📖	mathematical	`HolomorphicOn`	`RectangleIntegral`	—	`rect_subset_iff` `rectangle_mem_nhds_iff` `ContinuousOn.rectangleBorder_integrable` `rectangleBorder_subset_punctured_rect` `rectangle_subset_punctured_rect` `RectangleIntegralVSplit'` `HolomorphicOn.vanishesOnRectangle` `RectangleIntegralHSplit'`
`RectanglePullToNhdOfPole''` 📖	mathematical	`HolomorphicOn`	`RectangleIntegral'`	—	`RectanglePullToNhdOfPole`
`ResidueTheoremAtOrigin` 📖	mathematical	—	`RectangleIntegral'`	—	`RectangleIntegral'.eq_1` `ResidueTheoremAtOrigin'`
`ResidueTheoremAtOrigin'` 📖	mathematical	—	`RectangleIntegral`	—	`integral_const_div_re_add_self` `integral_const_div_self_add_im`
`ResidueTheoremAtOrigin_aux1c` 📖	—	—	—	—	—
`ResidueTheoremAtOrigin_aux1c'` 📖	—	—	—	—	—
`ResidueTheoremAtOrigin_aux2c` 📖	—	—	—	—	—
`ResidueTheoremAtOrigin_aux2c'` 📖	—	—	—	—	—
`ResidueTheoremInRectangle` 📖	mathematical	—	`RectangleIntegral'`	—	`RectangleIntegral.translate'` `RectangleIntegral'.eq_1` `ResidueTheoremAtOrigin'`
`ResidueTheoremOnRectangleWithSimplePole` 📖	mathematical	`HolomorphicOn`	`RectangleIntegral'`	—	`rectangleBorder_subset_rectangle` `not_mem_rectangleBorder_of_rectangle_mem_nhds` `RectangleIntegral'_congr` `HolomorphicOn.rectangleBorderIntegrable` `HolomorphicOn.rectangleBorderIntegrable'` `RectangleIntegral'.eq_1` `RectangleBorderIntegrable.add` `HolomorphicOn.vanishesOnRectangle` `ResidueTheoremInRectangle`
`ResidueTheoremOnRectangleWithSimplePole'` 📖	mathematical	`HolomorphicOn`	`RectangleIntegral'`	—	`BddAbove_on_rectangle_of_bdd_near` `existsDifferentiableOn_of_bddAbove` `ResidueTheoremOnRectangleWithSimplePole`
`VIntegral_symm` 📖	mathematical	—	`VIntegral`	—	—
`continuous_self_div_sq_add_sq` 📖	—	—	—	—	`sq_add_sq_ne_zero`
`existsDifferentiableOn_of_bddAbove` 📖	—	`HolomorphicOn`	—	—	—
`integral_const_div_re_add_self` 📖	—	—	—	—	`integral_const_div_self_add_im`
`integral_const_div_self_add_im` 📖	—	—	—	—	`Complex.inv_re_add_im` `continuous_self_div_sq_add_sq` `sq_add_sq_ne_zero` `integral_self_div_sq_add_sq` `integral_const_div_sq_add_sq`
`integral_const_div_sq_add_sq` 📖	—	—	—	—	—
`integral_self_div_sq_add_sq` 📖	—	—	—	—	`sq_add_sq_ne_zero` `continuous_self_div_sq_add_sq`
`rectangleIntegral_symm` 📖	mathematical	—	`RectangleIntegral`	—	—
`rectangleIntegral_symm_re` 📖	mathematical	—	`RectangleIntegral`	—	`HIntegral_symm`
`sq_add_sq_ne_zero` 📖	—	—	—	—	—
`verticalIntegral_split_three` 📖	mathematical	—	`VerticalIntegral` `VIntegral`	—	—

---

← Back to Index