Sandwiched Rel Rentropy additive alpha ne one

theorem sandwichedRelRentropy_additive_alpha_ne_one {α : ℝ} (hα : α ≠ 1) (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) :    D̃_ α(ρ₁ ⊗ᴹ ρ₂‖σ₁ ⊗ᴹ σ₂) = D̃_ α(ρ₁‖σ₁) + D̃_ α(ρ₂‖σ₂) := by  by_cases hα0 : 0 < α; swap  · simp [SandwichedRelRentropy, hα0]  by_cases h_ker : σ₁.M.ker ≤ ρ₁.M.ker ∧ σ₂.M.ker ≤ ρ₂.M.ker  · simp_all [SandwichedRelRentropy]    -- Apply the additivity of the trace term to split the logarithm into the sum of the logarithms.    have h_trace_add : Real.log ((ρ₁ ⊗ᴹ ρ₂).M.conj ((σ₁ ⊗ᴹ σ₂).M ^ ((1 - α) / (2 * α))).mat ^ α).trace = Real.log ((ρ₁.M.conj (σ₁.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace + Real.log ((ρ₂.M.conj (σ₂.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace := by      rw [ sandwiched_term_product, Real.log_mul ];      · exact (sandwiched_trace_pos h_ker.1).ne'      · exact (sandwiched_trace_pos h_ker.2).ne'    split_ifs <;> simp_all    · norm_num [ add_div ];      exact rfl;    · exact False.elim ( ‹¬ ( σ₁ ⊗ᴹ σ₂ |> MState.M |> HermitianMat.ker ) ≤ ( ρ₁ ⊗ᴹ ρ₂ |> MState.M |> HermitianMat.ker ) › ( by simpa [ HermitianMat.ker ] using ker_prod_le_iff _ _ _ _ |>.2 h_ker ) );  · have h_ker_prod : ¬((σ₁ ⊗ᴹ σ₂).M.ker ≤ (ρ₁ ⊗ᴹ ρ₂).M.ker) := by      simp_all  [ ker_prod_le_iff ]    rw [not_and_or] at h_ker    rcases h_ker with h_ker | h_ker    · simp [SandwichedRelRentropy, h_ker_prod, h_ker, hα0]    · simp [SandwichedRelRentropy, h_ker_prod, h_ker, hα0]