Research proof index

Monotonicity of the sandwiched Rényi divergence under traceLeft for α > 1. Follows from sandwichedRenyiEntropy_mono_traceRight' + SWAP invariance.

The sandwiched Rényi divergence is monotone under partial trace for α > 1. This follows from monotonicity of the trace functional together with the fact that D̃_α = log(Q̃_α) / (α - 1) and both log and 1/(α-1) are order-preserving for α > 1.

The trace functional is strictly positive when the kernel condition holds. Under σ.M.ker ≤ ρ.M.ker (i.e. supp(ρ) ⊆ supp(σ)), the sandwich σ^γ ρ σ^γ ≠ 0 because ρ has support inside σ's support. -/ theorem sandwichedTraceFunctional_pos (ρ σ : MState d) (hker : σ.M.ker ≤ ρ.M.ker) : 0 < Q̃_ α(ρ‖σ) := by rw [sandwichedTraceFunctional] apply HermitianMat...

The trace functional Q̃_α is jointly convex for α > 1. This is Proposition 3 of the paper, originally from Frank–Lieb. The proof uses the variational formula: Q̃_α(ρ‖σ) = sup_{H ≥ 0} f_α(H, ρ, σ) where f_α(H, ρ, σ) = α · Tr[ρ H] - (α-1) · Tr[(σ^{-γ} H σ^{-γ})^{α/(α-1)}] is jointly convex in (ρ, σ) for fixed H (since the first term is linear an...

Monotonicity of the trace functional under partial trace for α > 1. Equation (2.8) of the paper (second line).

Twirling on a bipartite system: applying 1_A ⊗ V_i and averaging produces the -- partial trace tensored with the maximally mixed state. -/ -- theorem twirling_bipartite [Nonempty dB] -- (κ : Type) [Fintype κ] (V : κ → Matrix.unitaryGroup dB ℂ) -- (hV : ∀ (X : HermitianMat dB ℂ), -- (Fintype.card κ : ℝ)⁻¹ • ∑ i : κ, X.conj (V i : Matrix dB dB ℂ) = -- (X....