Sandwiched Renyi Entropy DPI eq one

theorem sandwichedRenyiEntropy_DPI_eq_one (ρ σ : MState d₁) (Φ : CPTPMap d₁ d₂) :    D̃_ 1(Φ ρ‖Φ σ) ≤ D̃_ 1(ρ‖σ) := by  by_contra h_contra;  -- Since $\alpha \mapsto D_\alpha(\rho \| \sigma)$ is continuous on $(0, \infty)$, we can take the limit as $\alpha \to 1$.  have h_cont : Filter.Tendsto (fun α : ℝ => D̃_ α(Φ ρ‖Φ σ)) (nhdsWithin 1 (Set.Ioi 1)) (nhds (D̃_ 1(Φ ρ‖Φ σ))) ∧ Filter.Tendsto (fun α : ℝ => D̃_ α(ρ‖σ)) (nhdsWithin 1 (Set.Ioi 1)) (nhds (D̃_ 1(ρ‖σ))) := by    exact ⟨ tendsto_nhdsWithin_of_tendsto_nhds ( by simpa using sandwichedRelRentropy.continuousOn ( Φ ρ ) ( Φ σ ) |> ContinuousOn.continuousAt <| Ioi_mem_nhds zero_lt_one ), tendsto_nhdsWithin_of_tendsto_nhds ( by simpa using sandwichedRelRentropy.continuousOn ρ σ |> ContinuousOn.continuousAt <| Ioi_mem_nhds zero_lt_one ) ⟩;  exact h_contra <| le_of_tendsto_of_tendsto h_cont.1 h_cont.2 <| Filter.eventually_of_mem self_mem_nhdsWithin fun x hx => sandwichedRenyiEntropy_DPI_gt_one hx ρ σ Φ