Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,333 to 1,338 of 2,569 results.
Heat.integral_mul_exp_neg_sq_Ici_zero
Mathematical statement
Evaluation of ∫₀^∞ z exp(-z²) dz = 1/2.
Source project: PDE
Person-level attribution pending.
Heat.integral_split_near_far
Project documentation
Helper lemma for splitting integrals into near and far regions.
Source project: PDE
Person-level attribution pending.
HermitianMat.eigenvalues_le_one_of_le_one
Mathematical statement
If A ≥ 0 and A ≤ 1, then each eigenvalue of A is in [0, 1].
Source project: quantumInfo
Person-level attribution pending.
HermitianMat.inner_le_trace_rpow_mul
Mathematical statement
Hermitian trace Hölder inequality: for PSD A, B and conjugate exponents p, q > 1, ⟪A, B⟫ ≤ Tr[A^p]^(1/p) * Tr[B^q]^(1/q).
Source project: quantumInfo
Person-level attribution pending.
HermitianMat.inv_kronecker
Project documentation
The operator norm of the conjugate transpose is equal to the operator norm. -/ theorem Matrix.opNorm_conjTranspose_eq_opNorm {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n 𝕜) : Matrix.opNorm Aᴴ = Matrix.opNorm A := by unfold Matrix.opNorm rw [← ContinuousLinearMap.adjoint.norm_map (toEuclideanLin A).toContinuousLine...
Source project: quantumInfo
Person-level attribution pending.
HermitianMat.ker_weighted_sum_le
Mathematical statement
If for all i, ker(σs i) ≤ ker(ρs i), then ker(∑ w i • σs i) ≤ ker(∑ w i • ρs i), provided all weights are nonneg and all matrices are PSD.
Source project: quantumInfo
Person-level attribution pending.