Declaration search

Search projects and Mathlib in one place.

Find source-pinned declarations outside Mathlib by name or constant. The same query runs through Loogle for genuine elaborated structural search over Mathlib.

Name"PFR_conjecture"ConstantSubmodule Mathlib shape_ * (_ ^ _)Conclusion|- tsum _ = _ * tsum _Non-linearReal.sqrt ?a * Real.sqrt ?a

Standalone research projects

Structural project search needs compiled indexes

Therefore index

Therefore does not fake Lean elaboration with text matching. Name and constant filters work across the project corpus. Wildcards, metavariables, and conclusion filters require a compiled project-specific Loogle index. The Mathlib results below use that genuine engine today.

Mathlib

7 elaborated matches

Open in Loogle

ENNReal.tsum_mul_left

{α : Type u_1} {a : ENNReal} {f : α → ENNReal} : ∑' (i : α), a * f i = a * ∑' (i : α), f i

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Documentation

Real.tsum_exp_neg_mul_int_sq

{a : ℝ} (ha : 0 < a) : ∑' (n : ℤ), Real.exp (-Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Real.exp (-Real.pi / a * ↑n ^ 2)

Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Documentation

Complex.tsum_exp_neg_mul_int_sq

{a : ℂ} (ha : 0 < a.re) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * ↑n ^ 2)

Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Documentation

Complex.tsum_exp_neg_quadratic

{a : ℂ} (ha : 0 < a.re) (b : ℂ) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2 + 2 * ↑Real.pi * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * (↑n + Complex.I * b) ^ 2)

Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Jacobi's theta-function transformation formula for the sum of `exp -Q(x)`, where `Q` is a negative definite quadratic form.

Documentation

EisensteinSeries.qExpansion_identity

{k : ℕ} (hk : 1 ≤ k) (z : UpperHalfPlane) : ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial * ∑' (n : ℕ), ↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n

Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

This is one key identity relating infinite series to q-expansions which shows that `∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n, n ^ k q ^n` where `q = cexp (2 π I z)`.

Documentation

Showing 5 of 7. Open Loogle for the complete result window.

conclusion matches tsum _ = _ * tsum _