import Quantum.QuantumEntropy.VonNeumann.SSA
import Quantum.QuantumEntropy.UmegakiDPI.AlphaOneLimit
import Quantum.QuantumEntropy.UmegakiDPI.AlphaOneSupportLimit
import Quantum.QuantumEntropy.SandwichedRenyi.TripartiteSSA
import Quantum.TraceInequality.JensenOperatorInequalityInterval
import Quantum.TraceInequality.LownerHeinz.GlobalDegeneracy
import Quantum.TraceInequality.JensenOperatorInequalityFinite
import Quantum.QuantumEntropy.SandwichedRenyi.Theorem1
import Quantum.QuantumMechanics.Channel.Equivalence
import Quantum.TraceInequality.LownerHeinz.RpowZeroOne
import Quantum.TraceInequality.LownerHeinz.RpowOneTwo
import Quantum.TraceInequality.LownerHeinz.NegPow
import Quantum.TraceInequality.JensenOperatorInequality
import Quantum.TraceInequality.GeneralizedPerspectiveFunction
import Quantum.TraceInequality.LiebAndo.LinearMapsCore
import Quantum.QuantumEntropy.SandwichedRenyi.NonNeg.Monotonicity

namespace ComparatorChallenges.Paper1

open QuantumState
open TensorProduct
open scoped ComplexOrder MatrixOrder Topology

universe u v w

-- Preserve the normed-algebra instance when providers add scalar-tower instances.
attribute [local instance 2000] NormedAlgebra.toAlgebra

-- The basis argument is kept so that the six CP equivalences share one shape.
set_option linter.unusedDecidableInType false in
set_option linter.unusedFintypeInType false in
theorem cp_iff_tensor
    {ℋ₁ : Type u} {ℋ₂ : Type v} [Qudit ℋ₁] [Qudit ℋ₂]
    {κ : Type w} [DecidableEq κ] [Fintype κ]
    (_b : Module.Basis κ ℂ ℋ₁) (Φ : QuantumChannel.T ℋ₁ ℋ₂) :
    QuantumChannel.IsCompletelyPositive Φ ↔
      QuantumChannel.AmplificationPositive Φ :=
  QuantumChannel.cp_iff_tensor Φ

theorem cp_iff_choi
    {ℋ₁ : Type u} {ℋ₂ : Type v} [Qudit ℋ₁] [Qudit ℋ₂]
    {κ : Type w} [DecidableEq κ] [Fintype κ]
    (b : Module.Basis κ ℂ ℋ₁) (Φ : QuantumChannel.T ℋ₁ ℋ₂) :
    QuantumChannel.IsCompletelyPositive Φ ↔
      QuantumChannel.ChoiPositive b Φ :=
  QuantumChannel.cp_iff_choi b Φ

-- The basis argument is kept so that the six CP equivalences share one shape.
set_option linter.unusedDecidableInType false in
set_option linter.unusedFintypeInType false in
theorem cp_iff_kraus
    {ℋ₁ : Type u} {ℋ₂ : Type v} [Qudit ℋ₁] [Qudit ℋ₂]
    {κ : Type w} [DecidableEq κ] [Fintype κ]
    (_b : Module.Basis κ ℂ ℋ₁) (Φ : QuantumChannel.T ℋ₁ ℋ₂) :
    QuantumChannel.IsCompletelyPositive Φ ↔ QuantumChannel.HasKraus Φ :=
  QuantumChannel.cp_iff_kraus Φ

theorem cp_iff_rank_kraus
    {ℋ₁ : Type u} {ℋ₂ : Type v} [Qudit ℋ₁] [Qudit ℋ₂]
    {κ : Type w} [DecidableEq κ] [Fintype κ]
    (b : Module.Basis κ ℂ ℋ₁) (Φ : QuantumChannel.T ℋ₁ ℋ₂) :
    QuantumChannel.IsCompletelyPositive Φ ↔
      QuantumChannel.HasRankKraus b Φ :=
  QuantumChannel.cp_iff_rank_kraus b Φ

-- The basis argument is kept so that the six CP equivalences share one shape.
set_option linter.unusedDecidableInType false in
set_option linter.unusedFintypeInType false in
theorem cp_iff_stinespring
    {ℋ₁ : Type u} {ℋ₂ : Type v} [Qudit ℋ₁] [Qudit ℋ₂]
    {κ : Type w} [DecidableEq κ] [Fintype κ]
    (_b : Module.Basis κ ℂ ℋ₁) (Φ : QuantumChannel.T ℋ₁ ℋ₂) :
    QuantumChannel.IsCompletelyPositive Φ ↔
      ∃ (ℋ₃ : Type u) (_ : Qudit ℋ₃),
        ∃ A : ℋ₁ →ₗ[ℂ] (ℋ₂ ⊗[ℂ] ℋ₃),
          ∀ X : L ℋ₁,
            Φ X =
              (@QuantumChannel.traceOutRight ℋ₂ inferInstance ℋ₃ inferInstance
                (((A.comp X).comp
                  (LinearMap.adjoint A : (ℋ₂ ⊗[ℂ] ℋ₃) →ₗ[ℂ] ℋ₁)) :
                    L (ℋ₂ ⊗[ℂ] ℋ₃)) : L ℋ₂) := by
  simpa only [QuantumChannel.HasStinespring, QuantumChannel.StinespringRep] using
    QuantumChannel.cp_iff_stinespring Φ

theorem cp_iff_rank_stinespring
    {ℋ₁ : Type u} {ℋ₂ : Type v} [Qudit ℋ₁] [Qudit ℋ₂]
    {κ : Type w} [DecidableEq κ] [Fintype κ]
    (b : Module.Basis κ ℂ ℋ₁) (Φ : QuantumChannel.T ℋ₁ ℋ₂) :
    QuantumChannel.IsCompletelyPositive Φ ↔
      ∃ (ℋ₃ : Type u) (inst : Qudit ℋ₃),
        Module.finrank ℂ ℋ₃ = QuantumChannel.choiRank b Φ ∧
          ∃ A : ℋ₁ →ₗ[ℂ] (ℋ₂ ⊗[ℂ] ℋ₃),
            ∀ X : L ℋ₁,
              Φ X =
                (@QuantumChannel.traceOutRight ℋ₂ inferInstance ℋ₃ inst
                  (((A.comp X).comp
                    (LinearMap.adjoint A : (ℋ₂ ⊗[ℂ] ℋ₃) →ₗ[ℂ] ℋ₁)) :
                      L (ℋ₂ ⊗[ℂ] ℋ₃)) : L ℋ₂) := by
  simpa only [QuantumChannel.HasRankStinespring, QuantumChannel.StinespringRep] using
    QuantumChannel.cp_iff_rank_stinespring b Φ

theorem power_Icc_zero_one_operatorMonotoneOn_Ici
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐]
    [NonnegSpectrumClass ℝ 𝓐] (p : ℝ) (hp : p ∈ Set.Icc (0 : ℝ) 1) :
    LownerHeinzCore.OperatorMonotoneOn (𝓐 := 𝓐) (Set.Ici (0 : ℝ))
      (fun x ↦ x ^ p) :=
  LownerHeinzCore.power_Icc_zero_one_operatorMonotoneOn_Ici p hp

theorem operatorConcaveOn_rpow_Ici
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐]
    [Nontrivial 𝓐] [NonnegSpectrumClass ℝ 𝓐]
    (p : ℝ) (hp : p ∈ Set.Icc (0 : ℝ) 1) :
    LownerHeinzCore.OperatorConcaveOn (𝓐 := 𝓐) (Set.Ici (0 : ℝ))
      (fun x ↦ x ^ p) :=
  LownerHeinzCore.operatorConcaveOn_rpow_Ici p hp

theorem operatorConvexOn_rpow_Ici
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐]
    [Nontrivial 𝓐] [NonnegSpectrumClass ℝ 𝓐]
    (p : ℝ) (hp : p ∈ Set.Icc (1 : ℝ) 2) :
    LownerHeinzCore.OperatorConvexOn (𝓐 := 𝓐) (Set.Ici (0 : ℝ))
      (fun x ↦ x ^ p) :=
  LownerHeinzCore.operatorConvexOn_rpow_Ici p hp

theorem power_Icc_neg_one_zero_neg_operatorMonotoneOn_Ioi
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐]
    [NonnegSpectrumClass ℝ 𝓐]
    (p : ℝ) (hp : p ∈ Set.Icc (-1 : ℝ) 0) :
    LownerHeinzCore.OperatorMonotoneOn (𝓐 := 𝓐) (Set.Ioi (0 : ℝ))
      (fun x ↦ -(x ^ p)) :=
  LownerHeinzCore.power_Icc_neg_one_zero_neg_operatorMonotoneOn_Ioi p hp

theorem operatorConcaveOn_neg_rpow_Ioi
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐]
    [Nontrivial 𝓐] [NonnegSpectrumClass ℝ 𝓐]
    (p : ℝ) (hp : p ∈ Set.Icc (-1 : ℝ) 0) :
    LownerHeinzCore.OperatorConcaveOn (𝓐 := 𝓐) (Set.Ioi (0 : ℝ))
      (fun x ↦ -(x ^ p)) :=
  LownerHeinzCore.operatorConcaveOn_neg_rpow_Ioi p hp

theorem jensenColumn_of_opConvexIciAll
    {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ]
    [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ}
    (hf : JensenOperatorInequality.OperatorConvexIciAllContNonposAtZero.{u} f) :
    JensenOperatorInequality.JensenContractiveColumnCondition (ℋ := ℋ) f :=
  JensenOperatorInequality.jensenColumn_of_opConvexIciAll hf

section

-- Preserve the real scalar action in the frozen perspective and trace statements.
attribute [local instance 2000]
  NormedSpace.toModule NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace

theorem jointlyConvexOn_generalizedPerspective_psdSet_pdSet
    {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ]
    [CompleteSpace ℋ] [Nontrivial ℋ] {f h : ℝ → ℝ}
    (hf : JensenOperatorInequality.OperatorConvexIciAllContNonposAtZero.{u} f)
    (hconc : LownerHeinzTheorem.OperatorConcaveOn (ℋ := ℋ) (Set.Ioi (0 : ℝ)) h)
    (hcont : ContinuousOn h (Set.Ioi (0 : ℝ)))
    (hpos : ∀ x ∈ Set.Ioi (0 : ℝ), 0 < h x) :
    GeneralizedPerspectiveFunction.JointlyConvexOn
      (GeneralizedPerspectiveFunction.psdSet (ℋ := ℋ))
      GeneralizedPerspectiveFunction.pdSet
      (fun A B => GeneralizedPerspectiveFunction.generalizedPerspective f h A B) :=
  GeneralizedPerspectiveFunction.jointlyConvexOn_generalizedPerspective_psdSet_pdSet
    hf hconc hcont hpos

theorem jointlyConcaveOn_generalizedPerspective_psdSet_pdSet
    {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ]
    [CompleteSpace ℋ] [Nontrivial ℋ] {f h : ℝ → ℝ}
    (hfconc : LownerHeinzTheorem.OperatorConcaveOnAll.{u} (Set.Ici (0 : ℝ)) f)
    (hfcont : ContinuousOn f (Set.Ici (0 : ℝ)))
    (hf0 : 0 ≤ f 0)
    (hconc : LownerHeinzTheorem.OperatorConcaveOn (ℋ := ℋ) (Set.Ioi (0 : ℝ)) h)
    (hcont : ContinuousOn h (Set.Ioi (0 : ℝ)))
    (hpos : ∀ x ∈ Set.Ioi (0 : ℝ), 0 < h x) :
    GeneralizedPerspectiveFunction.JointlyConcaveOn
      (GeneralizedPerspectiveFunction.psdSet (ℋ := ℋ))
      GeneralizedPerspectiveFunction.pdSet
      (fun A B => GeneralizedPerspectiveFunction.generalizedPerspective f h A B) :=
  GeneralizedPerspectiveFunction.jointlyConcaveOn_generalizedPerspective_psdSet_pdSet
    (ℋ := ℋ) (f := f) (h := h) (@hfconc) hfcont hf0 hconc hcont hpos

theorem jointlyConcaveOn_liebTraceMap_pdSetLM
    {ℋ : Type u} [Qudit ℋ] [Nontrivial ℋ]
    {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (K : L ℋ) :
    GeneralizedPerspectiveFunction.JointlyConcaveOn
      SandwichedRenyiRelativeEntropy.pdSetLM
      SandwichedRenyiRelativeEntropy.pdSetLM
      (LiebAndoTrace.liebTraceMap s K) :=
  LiebAndoTrace.jointlyConcaveOn_liebTraceMap_pdSetLM hs0 hs1 K

theorem jointlyConvexOn_liebTraceMap_pdSetLM
    {ℋ : Type u} [Qudit ℋ] [Nontrivial ℋ]
    {s : ℝ} (hs1 : 1 ≤ s) (hs2 : s ≤ 2) (K : L ℋ) :
    GeneralizedPerspectiveFunction.JointlyConvexOn
      SandwichedRenyiRelativeEntropy.pdSetLM
      SandwichedRenyiRelativeEntropy.pdSetLM
      (LiebAndoTrace.liebTraceMap s K) :=
  LiebAndoTrace.jointlyConvexOn_liebTraceMap_pdSetLM hs1 hs2 K

theorem jointlyConvexOn_andoTraceMap_pdSetLM
    {ℋ : Type u} [Qudit ℋ] [Nontrivial ℋ]
    {q r : ℝ} (hq1 : 1 ≤ q) (hq2 : q ≤ 2)
    (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hqr : 1 ≤ q - r)
    (K : L ℋ) :
    GeneralizedPerspectiveFunction.JointlyConvexOn
      SandwichedRenyiRelativeEntropy.pdSetLM
      SandwichedRenyiRelativeEntropy.pdSetLM
      (LiebAndoTrace.andoTraceMap q r K) :=
  LiebAndoTrace.jointlyConvexOn_andoTraceMap_pdSetLM hq1 hq2 hr0 hr1 hqr K

end

theorem sandwichedRenyiDiv_monotone
    {ℋ : Type u} [Qudit ℋ] [Nontrivial ℋ]
    {𝒦 : Type u} [Qudit 𝒦] [Nontrivial 𝒦]
    (Φ : QuantumChannel.CPTP ℋ 𝒦)
    {α : ℝ} (hα_ge : (1 : ℝ) / 2 ≤ α) (hα_ne1 : α ≠ 1)
    {ρ σ : L ℋ}
    (hρ : ρ ∈ SandwichedRenyiRelativeEntropy.pdSetLM)
    (hσ : σ ∈ SandwichedRenyiRelativeEntropy.pdSetLM)
    (hΦρ : Φ.toFun ρ ∈ SandwichedRenyiRelativeEntropy.pdSetLM)
    (hΦσ : Φ.toFun σ ∈ SandwichedRenyiRelativeEntropy.pdSetLM) :
    SandwichedRenyiRelativeEntropy.sandwichedRenyiDiv α (Φ.toFun ρ) (Φ.toFun σ) ≤
      SandwichedRenyiRelativeEntropy.sandwichedRenyiDiv α ρ σ :=
  SandwichedRenyiRelativeEntropy.sandwichedRenyiDiv_monotone
    Φ hα_ge hα_ne1 hρ hσ hΦρ hΦσ

theorem sandwichedRenyiDivNN_monotone
    {ℋ 𝒦 : Type u} [Qudit ℋ] [Nontrivial ℋ]
    [Qudit 𝒦] [Nontrivial 𝒦]
    (Φ : QuantumChannel.CPTP ℋ 𝒦) {α : ℝ}
    (hα_ge : (1 : ℝ) / 2 ≤ α) (hα_ne1 : α ≠ 1)
    {ρ σ : L ℋ} (hρ : 0 ≤ ρ) (hσ : 0 ≤ σ) :
    SandwichedRenyiRelativeEntropy.sandwichedRenyiDivNN α (Φ.toFun ρ) (Φ.toFun σ) ≤
      SandwichedRenyiRelativeEntropy.sandwichedRenyiDivNN α ρ σ :=
  SandwichedRenyiRelativeEntropy.sandwichedRenyiDivNN_monotone
    Φ hα_ge hα_ne1 hρ hσ

section
open QuantumChannel VonNeumann

theorem strongSubadditivity_of_state
    {ℋA ℋB ℋC : Type u} [Qudit ℋA] [Qudit ℋB] [Qudit ℋC]
    [Nontrivial ℋA] [Nontrivial ℋB] [Nontrivial ℋC]
    (ρ : L (ℋA ⊗[ℂ] (ℋB ⊗[ℂ] ℋC)))
    (hρ : 0 ≤ ρ)
    (hTr : Tr ρ = 1) :
    vonNeumannEntropy ρ +
        vonNeumannEntropy
          (QuantumChannel.traceOutRight (QuantumChannel.traceOutLeft ρ)) ≤
      vonNeumannEntropy (QuantumChannel.traceOutThird ρ) +
        vonNeumannEntropy (QuantumChannel.traceOutLeft ρ) := by
  exact VonNeumann.strongSubadditivity_of_state ρ hρ hTr

end

section
open QuantumChannel SandwichedRenyiRelativeEntropy

theorem tendsto_sandwichedRenyiDiv_umegakiNorm_right
    {ℋ : Type u} [Qudit ℋ] [Nontrivial ℋ]
    {ρ σ : L ℋ} (hρ : ρ ∈ pdSetLM (ℋ := ℋ)) (hσ : σ ∈ pdSetLM (ℋ := ℋ)) :
    Filter.Tendsto (fun α => sandwichedRenyiDiv α ρ σ) (𝓝[>] (1 : ℝ))
      (𝓝 (umegakiNorm ρ σ)) := by
  exact SandwichedRenyiRelativeEntropy.tendsto_sandwichedRenyiDiv_umegakiNorm_right hρ hσ

end

section
open QuantumChannel SandwichedRenyiRelativeEntropy

theorem tendsto_sandwichedRenyiDiv_umegakiNorm_of_pd
    {H : Type u} [Qudit H] [Nontrivial H] {ρ σ : L H} (hρ : ρ ∈ pdSetLM) (hσ : σ ∈ pdSetLM) :
    Filter.Tendsto (fun α => sandwichedRenyiDiv α ρ σ) (𝓝[≠] (1 : ℝ))
      (𝓝 (umegakiNorm ρ σ)) := by
  exact SandwichedRenyiRelativeEntropy.tendsto_sandwichedRenyiDiv_umegakiNorm_of_pd hρ hσ

end

section
open QuantumChannel SandwichedRenyiRelativeEntropy

theorem sandwichedRenyiDivNN_tripartiteSSA
    {A B C : Type u} [Qudit A] [Qudit B] [Qudit C]
    [Nontrivial A] [Nontrivial B] [Nontrivial C] {α : ℝ} (hα : (1 : ℝ) / 2 ≤ α) (hα1 : α ≠ 1)
    (ρ : L (A ⊗[ℂ] (B ⊗[ℂ] C))) (hρ : 0 ≤ ρ) :
    let τ : L C := (((Module.finrank ℂ C : ℝ)⁻¹ : ℝ) : ℂ) • 1
    sandwichedRenyiDivNN α (traceOutLeft ρ)
      (TensorProduct.map (traceOutRight (traceOutLeft ρ)) τ) ≤
      sandwichedRenyiDivNN α ρ (tripartiteReference (traceOutThird ρ) τ) := by
  exact SandwichedRenyiRelativeEntropy.sandwichedRenyiDivNN_tripartiteSSA hα hα1 ρ hρ

end

section
open QuantumChannel SandwichedRenyiRelativeEntropy

theorem sandwichedRenyiDiv_tripartiteSSA
    {A B C : Type u} [Qudit A] [Qudit B] [Qudit C]
    [Nontrivial A] [Nontrivial B] [Nontrivial C] {α : ℝ}
    (hα : (1 : ℝ) / 2 ≤ α) (hα1 : α ≠ 1)
    (ρ : L (A ⊗[ℂ] (B ⊗[ℂ] C))) (hρ : 0 ≤ ρ)
    (hσ : tripartiteReference (traceOutThird ρ)
      ((((Module.finrank ℂ C : ℝ)⁻¹ : ℝ) : ℂ) • (1 : L C)) ∈ pdSetLM)
    (hQ : (sandwichedQuasi α ρ (tripartiteReference (traceOutThird ρ)
      ((((Module.finrank ℂ C : ℝ)⁻¹ : ℝ) : ℂ) • (1 : L C)))).re ≠ 0)
    (hQBC : (sandwichedQuasi α (traceOutLeft ρ)
      (TensorProduct.map (traceOutRight (traceOutLeft ρ))
        ((((Module.finrank ℂ C : ℝ)⁻¹ : ℝ) : ℂ) • (1 : L C)))).re ≠ 0)
    (_hTr : (Tr ρ).re ≠ 0) (_hTrBC : (Tr (traceOutLeft ρ)).re ≠ 0) :
    let τ : L C := (((Module.finrank ℂ C : ℝ)⁻¹ : ℝ) : ℂ) • 1
    sandwichedRenyiDiv α (traceOutLeft ρ)
      (TensorProduct.map (traceOutRight (traceOutLeft ρ)) τ) ≤
      sandwichedRenyiDiv α ρ (tripartiteReference (traceOutThird ρ) τ) := by
  exact SandwichedRenyiRelativeEntropy.sandwichedRenyiDiv_tripartiteSSA
    hα hα1 ρ hρ hσ hQ hQBC _hTr _hTrBC

end

section
open QuantumChannel LownerHeinzCore

theorem OperatorConvex.eq_zero_of_nontrivial
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐]
    [Nontrivial 𝓐] {f : ℝ → ℝ}
    (hf : OperatorConvex (𝓐 := 𝓐) f) : ∀ x, f x = 0 := by
  exact LownerHeinzCore.OperatorConvex.eq_zero_of_nontrivial hf

end

section
open QuantumChannel LownerHeinzCore

theorem OperatorConcave.eq_zero_of_nontrivial
    {𝓐 : Type u} [CStarAlgebra 𝓐] [PartialOrder 𝓐] [StarOrderedRing 𝓐] [Nontrivial 𝓐]
    {f : ℝ → ℝ} (hf : OperatorConcave (𝓐 := 𝓐) f) : ∀ x, f x = 0 := by
  exact LownerHeinzCore.OperatorConcave.eq_zero_of_nontrivial hf

end

section
open QuantumChannel LownerHeinzTheorem

theorem OperatorConvexAll.eq_zero {f : ℝ → ℝ} (hf : OperatorConvexAll.{u} f) : f = 0 := by
  exact LownerHeinzTheorem.OperatorConvexAll.eq_zero (@hf)

end

section
open QuantumChannel LownerHeinzTheorem

theorem OperatorConcaveAll.eq_zero {f : ℝ → ℝ} (hf : OperatorConcaveAll.{u} f) : f = 0 := by
  exact LownerHeinzTheorem.OperatorConcaveAll.eq_zero (@hf)

end

section
open QuantumChannel LownerHeinzTheorem

theorem operatorConvexOnAll_Ici_sq :
    OperatorConvexOnAll.{u} (Set.Ici 0) (fun x : ℝ ↦ x ^ (2 : ℕ)) := by
  exact @LownerHeinzTheorem.operatorConvexOnAll_Ici_sq.{u}

end

section
open QuantumChannel JensenOperatorInequality LownerHeinzTheorem

theorem jensenFinite_of_opConvexIciAll
    {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ]
    [CompleteSpace ℋ] [Nontrivial ℋ] {ι : Type v} [Fintype ι]
    {f : ℝ → ℝ} (hf : OperatorConvexIciAllContNonposAtZero.{u} f)
    (A X : ι → ℋ →L[ℂ] ℋ)
    (hA : ∀ i, IsSelfAdjoint (A i))
    (hAs : ∀ i, spectrum ℝ (A i) ⊆ Set.Ici (0 : ℝ))
    (hX : ∑ i, star (X i) * X i ≤ 1) :
    cfcR f (∑ i, star (X i) * A i * X i) ≤
      ∑ i, star (X i) * cfcR f (A i) * X i := by
  exact JensenOperatorInequality.jensenFinite_of_opConvexIciAll hf A X hA hAs hX

end

section
open QuantumChannel SandwichedRenyiRelativeEntropy

theorem sandwichedRenyiDivNN_monotone_of_isDensity
    {ℋ 𝒦 : Type u} [Qudit ℋ] [Nontrivial ℋ] [Qudit 𝒦] [Nontrivial 𝒦]
    (Φ : CPTP ℋ 𝒦) {α : ℝ}
    (hα_ge : (1 : ℝ) / 2 ≤ α) (hα_ne1 : α ≠ 1)
    {ρ σ : L ℋ} (hρ : IsDensity ρ) (hσ : IsDensity σ)
    (_hσpd : IsPositiveDefinite σ) :
    sandwichedRenyiDivNN α (Φ.toFun ρ) (Φ.toFun σ) ≤
      sandwichedRenyiDivNN α ρ σ := by
  exact SandwichedRenyiRelativeEntropy.sandwichedRenyiDivNN_monotone_of_isDensity
    Φ hα_ge hα_ne1 hρ hσ _hσpd

end

section
open QuantumChannel SandwichedRenyiRelativeEntropy

theorem tendsto_sandwichedRenyiDiv_umegakiNorm_of_supportLE
    {H : Type u} [Qudit H] [Nontrivial H] {ρ σ : L H}
    (hρ : 0 ≤ ρ) (hρ0 : ρ ≠ 0) (hσ : 0 ≤ σ) (hsupp : SupportLE ρ σ) :
    Filter.Tendsto (fun α => sandwichedRenyiDiv α ρ σ) (𝓝[≠] (1 : ℝ))
      (𝓝 (umegakiNorm ρ σ)) := by
  exact SandwichedRenyiRelativeEntropy.tendsto_sandwichedRenyiDiv_umegakiNorm_of_supportLE
    hρ hρ0 hσ hsupp

end

section
open QuantumChannel JensenOperatorInequality LownerHeinzTheorem

theorem jensenFinite_of_opConvexOnAll_of_isOpen
    {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ]
    [CompleteSpace ℋ] [Nontrivial ℋ] {ι : Type v} [Fintype ι]
    {I : Set ℝ} (hI : I.OrdConnected) (hopen : IsOpen I) (h0 : 0 ∈ I)
    {f : ℝ → ℝ} (hf : OperatorConvexOnAll.{u} I f) (hf0 : f 0 ≤ 0)
    (A X : ι → ℋ →L[ℂ] ℋ) (hA : ∀ i, IsSelfAdjoint (A i))
    (hAs : ∀ i, spectrum ℝ (A i) ⊆ I) (hX : ∑ i, star (X i) * X i ≤ 1) :
    cfcR f (∑ i, star (X i) * A i * X i) ≤
      ∑ i, star (X i) * cfcR f (A i) * X i := by
  exact JensenOperatorInequality.jensenFinite_of_opConvexOnAll_of_isOpen
    hI hopen h0 (@hf) hf0 A X hA hAs hX

end

section
open QuantumChannel JensenOperatorInequality LownerHeinzTheorem

theorem jensenFinite_of_opConvexOnAll_of_endpoints
    {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ]
    [CompleteSpace ℋ] [Nontrivial ℋ] {ι : Type v} [Fintype ι]
    {I : Set ℝ} (hI : I.OrdConnected) (h0 : 0 ∈ I)
    {f : ℝ → ℝ} (hf : OperatorConvexOnAll.{u} I f) (hf0 : f 0 ≤ 0)
    (he : ∀ x ∈ I \ interior I, ContinuousWithinAt f I x)
    (A X : ι → ℋ →L[ℂ] ℋ) (hA : ∀ i, IsSelfAdjoint (A i))
    (hAs : ∀ i, spectrum ℝ (A i) ⊆ I) (hX : ∑ i, star (X i) * X i ≤ 1) :
    cfcR f (∑ i, star (X i) * A i * X i) ≤
      ∑ i, star (X i) * cfcR f (A i) * X i := by
  exact JensenOperatorInequality.jensenFinite_of_opConvexOnAll_of_endpoints
    hI h0 (@hf) hf0 he A X hA hAs hX

end

end ComparatorChallenges.Paper1