Documentation Verification Report

PoissonSummation

📁 Source: Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean

Statistics

Metric	Count
Definitions	0
Theorems `tsum_exp_neg_mul_int_sq`, `tsum_exp_neg_quadratic`, `tsum_exp_neg_mul_int_sq`, `cexp_neg_quadratic_isLittleO_abs_rpow_cocompact`, `cexp_neg_quadratic_isLittleO_rpow_atTop`, `isLittleO_exp_neg_mul_sq_cocompact`, `rexp_neg_quadratic_isLittleO_rpow_atTop`, `tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact`	8
Total	8

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsum_exp_neg_mul_int_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `exp` `instMul` `instNeg` `ofReal` `Real.pi` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instIntCast` `SummationFilter.unconditional` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instPow` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero` `tsum_exp_neg_quadratic`
`tsum_exp_neg_quadratic` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `exp` `instAdd` `instMul` `instNeg` `ofReal` `Real.pi` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instIntCast` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instPow` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `Continuous.comp` `continuous_exp` `Continuous.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `continuous_const` `Continuous.pow` `continuous_ofReal` `Real.borelSpace` `FiniteDimensional.rclike_to_real` `fourier_gaussian_pi'` `re_ofReal_mul` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.pi_pos` `div_eq_mul_inv` `inv_re` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `normSq_pos` `Mathlib.Tactic.Contrapose.contrapose₃` `zero_re` `le_refl` `Asymptotics.IsLittleO.isBigO` `cexp_neg_quadratic_isLittleO_abs_rpow_cocompact` `neg_mul` `neg_re` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.pow_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.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.mul_assoc_rev` `mul_one` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.RingNF.add_assoc_rev` `I_sq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsInt.to_isNat` `exp_add` `mul_assoc` `mul_comm` `Asymptotics.IsBigO.const_mul_left` `neg_div` `zero_add` `tsum_mul_left` `instT2Space` `fourier_eval_zero` `Real.tsum_eq_tsum_fourier_of_rpow_decay` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsum_exp_neg_mul_int_sq` 📖	mathematical	`Real` `instLT` `instZero`	`tsum` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp` `instMul` `instNeg` `pi` `Monoid.toNatPow` `instMonoid` `instIntCast` `SummationFilter.unconditional` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instPow` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal_tsum` `Complex.ofReal_exp` `Complex.ofReal_mul` `Complex.ofReal_neg` `Complex.ofReal_pow` `Complex.ofReal_div` `Complex.ofReal_cpow` `LT.lt.le` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero` `Complex.tsum_exp_neg_quadratic` `Complex.ofReal_re`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp_neg_quadratic_isLittleO_abs_rpow_cocompact` 📖	mathematical	`Real` `Real.instLT` `Complex.re` `Real.instZero`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Real.norm` `Filter.cocompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Complex.exp` `Complex.instAdd` `Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.instPow` `abs` `Real.lattice` `Real.instAddGroup`	—	`cocompact_eq_atBot_atTop` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMinOrderOfNontrivial` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Asymptotics.isLittleO_sup` `Asymptotics.IsLittleO.congr'` `Asymptotics.IsLittleO.comp_tendsto` `cexp_neg_quadratic_isLittleO_rpow_atTop` `Filter.tendsto_neg_atBot_atTop` `Filter.Eventually.of_forall` `neg_mul` `Complex.ofReal_neg` `neg_sq` `mul_neg` `neg_neg` `Filter.Eventually.mp` `Filter.eventually_lt_atBot` `instNoBotOrderOfNoMinOrder` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `Filter.EventuallyEq.rfl` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `abs_of_pos`
`cexp_neg_quadratic_isLittleO_rpow_atTop` 📖	mathematical	`Real` `Real.instLT` `Complex.re` `Real.instZero`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Real.norm` `Filter.atTop` `Real.instPreorder` `Complex.exp` `Complex.instAdd` `Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.instPow`	—	`Asymptotics.IsLittleO.of_norm_left` `Complex.norm_exp` `mul_comm` `Complex.re_ofReal_mul` `rexp_neg_quadratic_isLittleO_rpow_atTop`
`isLittleO_exp_neg_mul_sq_cocompact` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Real.norm` `Filter.cocompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.instPow` `abs` `Real.lattice` `Real.instAddGroup`	—	`MulZeroClass.zero_mul` `add_zero` `cexp_neg_quadratic_isLittleO_abs_rpow_cocompact` `Complex.neg_re` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`rexp_neg_quadratic_isLittleO_rpow_atTop` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.exp` `Real.instAdd` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instPow`	—	`Real.isLittleO_exp_comp_exp_comp` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `mul_one` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `Mathlib.Tactic.Ring.mul_one` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Filter.Tendsto.atTop_mul_atTop₀` `Real.instIsOrderedRing` `Filter.tendsto_id` `Filter.tendsto_atTop_add_const_right` `Real.instIsOrderedAddMonoid` `Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Asymptotics.IsLittleO.trans` `neg_one_mul` `isLittleO_exp_neg_mul_rpow_atTop` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `Real.instMul` `Real.instPow` `abs` `Real.lattice` `Real.instAddGroup` `Real.exp` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Filter.cocompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `nhds`	—	`sq_abs` `cocompact_eq_atBot_atTop` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMinOrderOfNontrivial` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Filter.comap_abs_atTop` `Filter.tendsto_comap'_iff` `Filter.mem_atTop_sets` `instIsDirectedOrder` `Real.instArchimedean` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Asymptotics.IsLittleO.tendsto_zero_of_tendsto` `Nat.instAtLeastTwoHAddOfNat` `rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg` `Filter.Tendsto.comp` `Real.tendsto_exp_atBot` `Filter.Tendsto.const_mul_atTop_of_neg` `Real.instIsStrictOrderedRing` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Filter.tendsto_id`

---

← Back to Index