DPI (Data Processing Inequality)

The Data Processing Inequality (DPI) for the sandwiched Rényi relative entropy, and as a consequence, the quantum relative entropy.

noncomputable def weighted_norm {d : Type u_1} [Fintype d] [DecidableEq d] (p : ℝ) (σ : MState d) (X : Matrix d d ℂ) : ℝ

The weighted norm |X|_{p, σ} defined in the paper.

Equations

• weighted_norm p σ X = schattenNorm (↑((↑σ).cfc fun (x : ℝ) => x ^ (1 / (2 * p))) * X * ↑((↑σ).cfc fun (x : ℝ) => x ^ (1 / (2 * p)))) p

noncomputable def spectralNorm_mat {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) : ℝ

The spectral norm (operator norm) of a matrix.

Equations

• spectralNorm_mat A = if h : Finset.univ.Nonempty then let A_dag_A := ⟨A.conjTranspose * A, ⋯⟩; √((Finset.image ⋯.eigenvalues Finset.univ).max' ⋯) else 0

noncomputable def weighted_norm_infty {d : Type u_1} [Fintype d] [DecidableEq d] : MState d → (X : Matrix d d ℂ) → ℝ

The weighted norm for p = \infty.

Equations

• weighted_norm_infty x✝ X = spectralNorm_mat X

noncomputable def Gamma {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (X : Matrix d d ℂ) : Matrix d d ℂ

The map Γ_σ(X) = σ^{1/2} X σ^{1/2}.

Equations

• Gamma σ X = ↑((↑σ).cfc fun (x : ℝ) => x ^ (1 / 2)) * X * ↑((↑σ).cfc fun (x : ℝ) => x ^ (1 / 2))

noncomputable def Gamma_inv {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (X : Matrix d d ℂ) : Matrix d d ℂ

The inverse map Γ_σ^{-1}(X) = σ^{-1/2} X σ^{-1/2}.

Equations

• Gamma_inv σ X = ↑((↑σ).cfc fun (x : ℝ) => x ^ (-1 / 2)) * X * ↑((↑σ).cfc fun (x : ℝ) => x ^ (-1 / 2))

noncomputable def T_op {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (Φ : CPTPMap d d₂ ℂ) (σ : MState d) (X : Matrix d d ℂ) : Matrix d₂ d₂ ℂ

The operator T = Γ_{Φ(σ)}^{-1} ∘ Φ ∘ Γ_σ.

Equations

• T_op Φ σ X = Gamma_inv (Φ σ) ((((Φ.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map (Gamma σ X))

noncomputable def induced_norm {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (p : ℝ) (σ : MState d) (Φ : CPTPMap d d₂ ℂ) (Ψ : Matrix d d ℂ → Matrix d₂ d₂ ℂ) : ℝ

The induced norm of a map Ψ: M_d -> M_d2 with respect to weighted norms.

Equations

• induced_norm p σ Φ Ψ = sSup {x : ℝ | ∃ (X : Matrix d d ℂ) (_ : weighted_norm p σ X ≠ 0), weighted_norm p (Φ σ) (Ψ X) / weighted_norm p σ X = x}

noncomputable def induced_norm_infty_map {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) (Ψ : Matrix d d ℂ → Matrix d₂ d₂ ℂ) : ℝ

Equations

• induced_norm_infty_map σ Φ Ψ = sSup {x : ℝ | ∃ (X : Matrix d d ℂ) (_ : weighted_norm_infty σ X ≠ 0), weighted_norm_infty (Φ σ) (Ψ X) / weighted_norm_infty σ X = x}

noncomputable def T_map {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) : MatrixMap d d₂ ℂ

Equations

• T_map σ Φ = { toFun := fun (X : Matrix d d ℂ) => T_op Φ σ X, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Gamma_map {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : MatrixMap d d ℂ

Equations

• Gamma_map σ = MatrixMap.conj ↑((↑σ).cfc fun (x : ℝ) => x ^ (1 / 2))

theorem Gamma_map_eq {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (X : Matrix d d ℂ) : (Gamma_map σ) X = Gamma σ X

theorem Gamma_map_CP {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : (Gamma_map σ).IsCompletelyPositive

noncomputable def Gamma_inv_map {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : MatrixMap d d ℂ

Equations

• Gamma_inv_map σ = MatrixMap.conj ↑((↑σ).cfc fun (x : ℝ) => x ^ (-1 / 2))

theorem Gamma_inv_map_eq {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (X : Matrix d d ℂ) : (Gamma_inv_map σ) X = Gamma_inv σ X

noncomputable def sigma_inv_sqrt {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : Matrix d d ℂ

Equations

• sigma_inv_sqrt σ = ↑((↑σ).cfc fun (x : ℝ) => x ^ (-1 / 2))

theorem Gamma_inv_map_eq_conj {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : Gamma_inv_map σ = MatrixMap.conj (sigma_inv_sqrt σ)

theorem Gamma_inv_map_CP {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : (Gamma_inv_map σ).IsCompletelyPositive

theorem T_map_eq_comp {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) : T_map σ Φ = Gamma_inv_map (Φ σ) ∘ₗ (((Φ.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map ∘ₗ Gamma_map σ

theorem T_is_CP {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) : (T_map σ Φ).IsCompletelyPositive

theorem T_is_positive {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) : (T_map σ Φ).IsPositive

theorem weighted_norm_one_eq_trace_norm_Gamma {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (X : Matrix d d ℂ) : weighted_norm 1 σ X = schattenNorm (Gamma σ X) 1

noncomputable def general_induced_norm {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (p q : ℝ) (σ : MState d) (σ' : MState d₂) (Ψ : MatrixMap d d₂ ℂ) : ℝ

Equations

• general_induced_norm p q σ σ' Ψ = sSup {x : ℝ | ∃ (X : Matrix d d ℂ) (_ : weighted_norm p σ X ≠ 0), weighted_norm q σ' (Ψ X) / weighted_norm p σ X = x}

theorem HermitianMat.cfc_mul {d : Type u_11} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (f g : ℝ → ℝ) : ↑(A.cfc f) * ↑(A.cfc g) = ↑(A.cfc fun (x : ℝ) => f x * g x)

theorem Gamma_one {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) : Gamma σ 1 = ↑↑σ

theorem Gamma_inv_self {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (hσ : σ.m.PosDef) : Gamma_inv σ ↑↑σ = 1

theorem CPTPMap_apply_MState_M {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (Φ : CPTPMap d d₂ ℂ) (σ : MState d) : ↑↑(Φ σ) = (((Φ.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map ↑↑σ

theorem T_map_unital {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) (hΦσ : (Φ σ).m.PosDef) : (T_map σ Φ) 1 = 1

theorem T_map_is_CP_proof {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (σ : MState d) (Φ : CPTPMap d d₂ ℂ) : (T_map σ Φ).IsCompletelyPositive

theorem Gamma_Gamma_inv {d : Type u_1} [Fintype d] [DecidableEq d] (σ : MState d) (hσ : σ.m.PosDef) (X : Matrix d d ℂ) : Gamma σ (Gamma_inv σ X) = X

theorem HermitianMat.le_smul_one_imp_eigenvalues_le {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (M : ℝ) (h : A ≤ M • 1) (i : d) : ⋯.eigenvalues i ≤ M

theorem HermitianMat.eigenvalues_le_imp_le_smul_one {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (M : ℝ) (h : ∀ (i : d), ⋯.eigenvalues i ≤ M) : A ≤ M • 1

theorem block_matrix_posSemidef {m : Type u_11} {n : Type u_12} {k : Type u_13} [Fintype m] [Fintype n] [Fintype k] (X : Matrix k n ℂ) (Y : Matrix k m ℂ) : (Matrix.fromBlocks (Y.conjTranspose * Y) (Y.conjTranspose * X) (X.conjTranspose * Y) (X.conjTranspose * X)).PosSemidef

The block matrix [[1, X], [X†, X†X]] is positive semidefinite.

theorem block_matrix_one_posSemidef {m : Type u_11} {n : Type u_12} [Fintype m] [Fintype n] [DecidableEq m] (X : Matrix m n ℂ) : (Matrix.fromBlocks 1 X X.conjTranspose (X.conjTranspose * X)).PosSemidef

theorem sandwichedRenyiEntropy_DPI {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] {α : ℝ} (hα : 1 ≤ α) (ρ σ : MState d) (Φ : CPTPMap d d₂ ℂ) : D̃_α(Φ ρ‖Φ σ) ≤ D̃_α(ρ‖σ)

The Data Processing Inequality for the Sandwiched Renyi relative entropy. Proved in https://arxiv.org/pdf/1306.5920. Seems kind of involved.

axiom sandwichedRenyiEntropy_DPI_ax {d : Type u_11} {d₂ : Type u_12} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] {α : ℝ} (hα : 1 ≤ α) (ρ σ : MState d) (Φ : CPTPMap d d₂ ℂ) : D̃_α(Φ ρ‖Φ σ) ≤ D̃_α(ρ‖σ)