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 10 research declarations. Search 10,000 more complete Mathlib declarations.
10 results
Clear filtersdoubly_stochastic_holder
Plain-language statement
Doubly stochastic Hölder inequality: for nonneg a, b, doubly stochastic w, and conjugate p, q > 1: ∑{ij} a_i * b_j * w{ij} ≤ (∑ a_i^p)^{1/p} * (∑ b_j^q)^{1/q}.
Source project: quantumInfo
Person-level attribution pending.
HermitianMat.eigenvalues_le_one_of_le_one
Plain-language 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
Plain-language 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.rpow_neg_mul_rpow_eq_supportProj
Plain-language statement
For PSD A and p ≠ 0, A^{-p} * A^p = HermitianMat.supportProj A.
Source project: quantumInfo
Person-level attribution pending.
HermitianMat.trace_rpow_le_trace_of_le_one
Plain-language statement
For positive A ≤ 1 and p ≥ 1, Tr[A^p] ≤ Tr[A].
Source project: quantumInfo
Person-level attribution pending.
ker_kron_le_of_le
Plain-language statement
If the kernels of the components are contained, then the kernel of the Kronecker product is contained.
Source project: quantumInfo
Person-level attribution pending.