Sandwiched Trace Functional mono trace Right

theorem sandwichedTraceFunctional_mono_traceRight [Nonempty dB]    (hα : 1 < α) (ρ σ : MState (dA × dB)) (hker : σ.M.ker ≤ ρ.M.ker) :    Q̃_ α(ρ.traceRight‖σ.traceRight) ≤ Q̃_ α(ρ‖σ) := by  -- Obtain the twirling unitaries  obtain ⟨κ, hκ_fin, hκ_ne, V, hV⟩ := exists_twirling_unitaries (dB := dB)  letI : Fintype κ := hκ_fin  letI : Nonempty κ := hκ_ne  -- By unitary invariance, Q̃_α(ρ‖σ) = Q̃_α(V_i ρ V_i†‖V_i σ V_i†) for each i  have h_inv (i) : Q̃_ α(ρ.conjTensorUnitary (V i)‖σ.conjTensorUnitary (V i)) = Q̃_ α(ρ‖σ) :=    sandwichedTraceFunctional_conj_tensorUnitary ρ σ (V i)  -- Step 2: Q̃_α(ρ‖σ) = Σ_i (1/|κ|) * Q̃_α(V_i ρ V_i†‖V_i σ V_i†)  have hcard_ne : (Fintype.card κ : ℝ) ≠ 0 :=    Nat.cast_ne_zero.mpr Fintype.card_ne_zero  have h_avg : Q̃_ α(ρ‖σ) = ∑ i : κ, (Fintype.card κ : ℝ)⁻¹ * Q̃_ α(ρ.conjTensorUnitary (V i)‖σ.conjTensorUnitary (V i)) := by    simp only [h_inv, Finset.sum_const, Finset.card_univ, nsmul_eq_mul]    field_simp  -- Step 3: By joint convexity (α > 1)  have hw_sum : ∑ i : κ, (Fintype.card κ : ℝ)⁻¹ = 1 := by    rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]    exact mul_inv_cancel₀ hcard_ne  set ρ_mix := ρ.traceRight ⊗ᴹ MState.uniform (d := dB)  set σ_mix := σ.traceRight ⊗ᴹ MState.uniform (d := dB)  have hρ_mix : ρ_mix.M = ∑ i : κ, (Fintype.card κ : ℝ)⁻¹ • (ρ.conjTensorUnitary (V i)).M :=    (twirling_average_eq κ V hV ρ).symm  have hσ_mix : σ_mix.M = ∑ i : κ, (Fintype.card κ : ℝ)⁻¹ • (σ.conjTensorUnitary (V i)).M :=    (twirling_average_eq κ V hV σ).symm  have h_convex := sandwichedTraceFunctional_jointly_convex hα    (fun (_ : κ) => (Fintype.card κ : ℝ)⁻¹) (by intro; positivity) hw_sum    (fun i => ρ.conjTensorUnitary (V i)) (fun i => σ.conjTensorUnitary (V i))    ρ_mix σ_mix hρ_mix hσ_mix    (fun i => MState.ker_conjTensorUnitary_le ρ σ (V i) hker)  -- Step 4 + 5: Q̃_α(ρ_A ⊗ π_B‖σ_A ⊗ π_B) = Q̃_α(ρ_A‖σ_A) by tensor invariance  have h_tensor : Q̃_ α(ρ_mix‖σ_mix) = Q̃_ α(ρ.traceRight‖σ.traceRight) :=    sandwichedTraceFunctional_tensor_invariant (by linarith) ρ.traceRight σ.traceRight MState.uniform  -- Combine  calc Q̃_ α(ρ.traceRight‖σ.traceRight)      = Q̃_ α(ρ_mix‖σ_mix) := h_tensor.symm    _ ≤ ∑ i : κ, (Fintype.card κ : ℝ)⁻¹ * Q̃_ α(ρ.conjTensorUnitary (V i)‖σ.conjTensorUnitary (V i)) := h_convex    _ = Q̃_ α(ρ‖σ) := h_avg.symm