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,465 to 1,470 of 2,569 results.
KEMScheme.perfectlyCorrect_composeWithDEM
Mathematical statement
If a KEM and externally keyed DEM are both perfectly correct in the concrete probabilistic semantics of m, then their composition is also perfectly correct.
Source project: VCVio
Person-level attribution pending.
ker_kron_le_of_le
Mathematical 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.
ker_le_of_ker_kron_le_left
Mathematical statement
If the kernel of a product state is contained in another, the left component kernel is contained.
Source project: quantumInfo
Person-level attribution pending.
ker_le_of_ker_kron_le_right
Mathematical statement
If the kernel of a product state is contained in another, the right component kernel is contained.
Source project: quantumInfo
Person-level attribution pending.
ker_le_traceRight
Mathematical statement
The kernel condition σ.M.ker ≤ ρ.M.ker is preserved under partial trace. This follows because supp(ρ) ⊆ supp(σ) implies supp(Tr_B ρ) ⊆ supp(Tr_B σ): if v ∈ supp(Tr_B ρ), then ⟨v, (Tr_B ρ) v⟩ > 0, so for some basis vector e_b we have v ⊗ e_b ∈ supp(ρ) ⊆ supp(σ), hence ⟨v, (Tr_B σ) v⟩ ≥ ⟨v ⊗ e_b, σ (v ⊗ e_b)⟩ > 0.
Source project: quantumInfo
Person-level attribution pending.
Ket.IsProd_iff_mul_eq_mul
Mathematical statement
A ket is a product state iff its components are cross-multiplicative.
Source project: quantumInfo
Person-level attribution pending.