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 filtersker_le_of_ker_kron_le_left
Plain-language 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
Plain-language 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.
qRelativeEnt.lowerSemicontinuous
Project documentation
Quantum relative entropy when σ has full rank -/ theorem qRelativeEnt_rank {ρ σ : MState d} [σ.M.NonSingular] : (𝐃(ρ‖σ) : EReal) = ⟪ρ.M, ρ.M.log - σ.M.log⟫ := by apply qRelativeEnt_ker simp [HermitianMat.nonSingular_ker_bot] section lowerSemicontinuous_1 variable {d : Type*} [Fintype d] [DecidableEq d] open scoped InnerProductSpace RealInnerProductSpace...
Source project: quantumInfo
Person-level attribution pending.
sandwichedRelRentropy_additive_alpha_ne_one
Project documentation
The Sandwiched Renyi Relative entropy is additive for α=1 (standard relative entropy). -/ private theorem sandwichedRelRentropy_additive_alpha_one (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : D̃_ 1(ρ₁ ⊗ᴹ ρ₂‖σ₁ ⊗ᴹ σ₂) = D̃_ 1(ρ₁‖σ₁) + D̃_ 1(ρ₂‖σ₂) := by by_cases h1 : σ₁.M.ker ≤ ρ₁.M.ker <;> by_cases h2 : σ₂.M.ker ≤ ρ₂.M.ker · simp only [SandwichedRelRentropy,...
Source project: quantumInfo
Person-level attribution pending.