Sandwiched Renyi Entropy DPI gt one

theorem sandwichedRenyiEntropy_DPI_gt_one (hα : 1 < α) (ρ σ : MState d₁) (Φ : CPTPMap d₁ d₂) :    D̃_ α(Φ ρ‖Φ σ) ≤ D̃_ α(ρ‖σ) := by  have _ : Nonempty d₁ := ρ.nonempty  have _ : Nonempty d₂ := (Φ ρ).nonempty  haveI : Inhabited d₂ := Classical.inhabited_of_nonempty ‹_›  let ψ₀ : Ket (d₂ × d₂) := Ket.basis default  let τ := MState.pure ψ₀  obtain ⟨U, hU⟩ := Φ.purify_IsUnitary  -- USe the `zero_prep` / `prep` / `append` from `CPTPMap.purify_trace`  let zero_prep : CPTPMap Unit (d₂ × d₂) := CPTPMap.replacement τ  let prep := ((CPTPMap.id : CPTPMap d₁ d₁) ⊗ᶜᵖ zero_prep)  let append : CPTPMap d₁ (d₁ × Unit) := CPTPMap.ofEquiv (Equiv.prodPUnit d₁).symm  calc D̃_ α(Φ ρ‖Φ σ)    _ = D̃_ α((Φ.purify ((prep ∘ₘ append) ρ)).traceLeft.traceLeft‖            (Φ.purify ((prep ∘ₘ append) σ)).traceLeft.traceLeft) := by        have h_trace (ξ) : Φ ξ = (Φ.purify ((prep ∘ₘ append) ξ)).traceLeft.traceLeft := by          simpa using congr($Φ.purify_trace ξ)        rw [h_trace ρ, h_trace σ]    _ = D̃_ α(((ρ ⊗ᴹ τ).U_conj U).traceLeft.traceLeft‖             ((σ ⊗ᴹ τ).U_conj U).traceLeft.traceLeft) := by        have h_app (ξ) : Φ.purify ξ = ξ.U_conj U := congr($hU ξ)        rw [prep_append_eq_tensor_pure ρ, prep_append_eq_tensor_pure σ, h_app, h_app]    _ ≤ D̃_ α(((ρ ⊗ᴹ τ).U_conj U).traceLeft‖((σ ⊗ᴹ τ).U_conj U).traceLeft) :=        sandwichedRenyiEntropy_mono_traceLeft hα ..    _ ≤ D̃_ α((ρ ⊗ᴹ τ).U_conj U‖(σ ⊗ᴹ τ).U_conj U) :=        sandwichedRenyiEntropy_mono_traceLeft hα ..    _ = D̃_ α(ρ ⊗ᴹ τ‖σ ⊗ᴹ τ) :=        sandwichedRenyiEntropy_conj_unitary (by positivity) _ _ _    _ = D̃_ α(ρ‖σ) :=        sandwichedRenyiEntropy_tensor_pure (by positivity) ρ σ ψ₀