feat(CStarAlgebra): x ↦ x ^ p is operator concave for p ∈ [0, 1]

Mathlib/Algebra/Algebra/Unitization.lean

@@ -405,19 +405,23 @@ theorem linearMap_ext {N} [CommSemiring S] [AddCommMonoid R] [AddCommMonoid A] [
   (linearEquiv S R A).arrowCongr (.refl ..) |>.injective <|
     LinearMap.prod_ext (LinearMap.ext hl) (LinearMap.ext hr)
 
-variable (R A)
+variable [Semiring S] [Semiring R] [AddCommMonoid A] [SMul R A] [Module S R] [Module S A]
 
--- TODO: generalize to `S`-linear
-/-- The canonical `R`-linear inclusion `A → Unitization R A`. -/
+variable (S R A) in
+/-- The canonical `S`-linear inclusion `A → Unitization R A`. -/
 @[simps apply]
-def inrHom [Semiring R] [AddCommMonoid A] [Module R A] : A →ₗ[R] Unitization R A where
+def inrHom : A →ₗ[S] Unitization R A where
   toFun := (↑)
   map_add' := inr_add R
   map_smul' := inr_smul R
 
-/-- The canonical `R`-linear projection `Unitization R A → A`. -/
+omit [SMul R A] in
+lemma inrHom_injective : Function.Injective (inrHom S R A) := Unitization.inr_injective
+
+variable (S R A) in
+/-- The canonical `S`-linear projection `Unitization R A → A`. -/
 @[simps apply]
-def sndHom [Semiring R] [AddCommMonoid A] [Module R A] : Unitization R A →ₗ[R] A where
+def sndHom : Unitization R A →ₗ[S] A where
   toFun a := a.snd
   map_add' := snd_add
   map_smul' := snd_smul

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -109,6 +109,22 @@ lemma inr_nonneg_iff {a : A} : 0 ≤ (a : A⁺¹) ↔ 0 ≤ a := by
     · exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h
     · exact .of_nonneg h
 
+lemma convexOn_of_convexOn_inr_comp {f : A → A} {s : Set A}
+    (hf : ∀ x, IsSelfAdjoint (f x))
+    (hf₂ : ConvexOn ℝ s (Unitization.inr (R := ℂ) ∘ f)) : ConvexOn ℝ s f := by
+  refine ⟨hf₂.1, ?_⟩
+  intro x hx y hy a b ha hb hab
+  rw [← Unitization.inr_le_iff _ _]
+  simpa using hf₂.2 hx hy ha hb hab
+
+lemma concaveOn_of_concaveOn_inr_comp {f : A → A} {s : Set A}
+    (hf : ∀ x, IsSelfAdjoint (f x))
+    (hf₂ : ConcaveOn ℝ s (Unitization.inr (R := ℂ) ∘ f)) : ConcaveOn ℝ s f := by
+  refine ⟨hf₂.1, ?_⟩
+  intro x hx y hy a b ha hb hab
+  rw [← Unitization.inr_le_iff _ _]
+  simpa using hf₂.2 hx hy ha hb hab
+
 alias ⟨LE.le.of_inr, LE.le.inr⟩ := inr_nonneg_iff
 
 set_option backward.isDefEq.respectTransparency false in
@@ -489,6 +505,50 @@ lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a} := by
 instance : OrderClosedTopology A where
   isClosed_le' := isClosed_le_of_isClosed_nonneg isClosed_nonneg
 
+open Unitization in
+lemma convexOn_cfcₙ_of_convexOn_cfc {f : ℝ → ℝ} {s : Set A}
+    (hf : ConvexOn ℝ (inr (R := ℂ) '' s) (cfc f)) : ConvexOn ℝ s (cfcₙ f) := by
+  let inrl : A →ₗ[ℝ] A⁺¹ := inrHom ℝ ℂ A
+  by_cases hf₀ : f 0 = 0
+  case neg =>
+    have : (cfcₙ f : A → A) = fun _ => 0 := by
+      ext x
+      simp [cfcₙ_apply_of_not_map_zero _ hf₀]
+    rw [this]
+    refine convexOn_const _ ?_
+    have : Convex ℝ (inrl ⁻¹' (inrl '' s)) := Convex.linear_preimage hf.1 _
+    rwa [Set.preimage_image_eq _ inrHom_injective] at this
+  refine convexOn_of_convexOn_inr_comp (fun _ => IsSelfAdjoint.cfcₙ) ?_
+  have h₁ : inr (R := ℂ) ∘ (cfcₙ f) = fun x : A => ((cfcₙ f x : A) : A⁺¹) := rfl
+  have h₂ : (fun x : A => ((cfcₙ f x : A) : A⁺¹))
+      = fun x : A => cfc f (x : A⁺¹) := by ext1; rw [real_cfcₙ_eq_cfc_inr ..]; rfl
+  rw [h₁, h₂]
+  have h₃ : ConvexOn ℝ (inrl ⁻¹' (inrl '' s)) ((cfc f) ∘ inrl) :=
+    ConvexOn.comp_linearMap (g := inrl) hf
+  rwa [Set.preimage_image_eq _ inrHom_injective] at h₃
+
+open Unitization in
+lemma concaveOn_cfcₙ_of_concaveOn_cfc {f : ℝ → ℝ} {s : Set A}
+    (hf : ConcaveOn ℝ (inr (R := ℂ) '' s) (cfc f)) : ConcaveOn ℝ s (cfcₙ f) := by
+  let inrl : A →ₗ[ℝ] A⁺¹ := inrHom ℝ ℂ A
+  by_cases hf₀ : f 0 = 0
+  case neg =>
+    have : (cfcₙ f : A → A) = fun _ => 0 := by
+      ext x
+      simp [cfcₙ_apply_of_not_map_zero _ hf₀]
+    rw [this]
+    refine concaveOn_const _ ?_
+    have : Convex ℝ (inrl ⁻¹' (inrl '' s)) := Convex.linear_preimage hf.1 _
+    rwa [Set.preimage_image_eq _ inrHom_injective] at this
+  refine concaveOn_of_concaveOn_inr_comp (fun _ => IsSelfAdjoint.cfcₙ) ?_
+  have h₁ : inr (R := ℂ) ∘ (cfcₙ f) = fun x : A => ((cfcₙ f x : A) : A⁺¹) := rfl
+  have h₂ : (fun x : A => ((cfcₙ f x : A) : A⁺¹))
+      = fun x : A => cfc f (x : A⁺¹) := by ext1; rw [real_cfcₙ_eq_cfc_inr ..]; rfl
+  rw [h₁, h₂]
+  have h₃ : ConcaveOn ℝ (inrl ⁻¹' (inrl '' s)) ((cfc f) ∘ inrl) :=
+    ConcaveOn.comp_linearMap (g := inrl) hf
+  rwa [Set.preimage_image_eq _ inrHom_injective] at h₃
+
 section Icc
 
 open Unitization Set Metric
@@ -508,6 +568,10 @@ lemma preimage_inr_Icc_zero_one :
   ext
   simp [-mem_Icc, inr_mem_Icc_iff_norm_le]
 
+lemma inr_map_Ici_zero : inr '' (Ici (0 : A)) ⊆ Ici (0 : A⁺¹) := by
+  rintro - ⟨a, ha, rfl⟩
+  exact Unitization.inr_nonneg_iff.mpr ha
+
 end Icc
 
 end CStarAlgebra

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -790,8 +790,8 @@ lemma cfc_inv_id (a : Aˣ) (ha : p a := by cfc_tac) :
   · rintro x hx rfl
     exact spectrum.zero_notMem R a.isUnit hx
 
-lemma cfc_ringInverse_id (a : A) (ha_unit : IsUnit a) (ha : p a := by cfc_tac) :
-    cfc (fun x ↦ x⁻¹ : R → R) (a : A) = a⁻¹ʳ := by
+lemma cfc_ringInverse_id (ha_unit : IsUnit a) (ha : p a := by cfc_tac) :
+    cfc (fun x ↦ x⁻¹ : R → R) a = a⁻¹ʳ := by
   rw [Ring.inverse_of_isUnit ha_unit]
   change cfc (fun x ↦ x⁻¹ : R → R) (ha_unit.unit : A) = ha_unit.unit⁻¹
   exact cfc_inv_id _ ha

Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

@@ -80,7 +80,7 @@ lemma unitization_nnnorm_inr (x : A) : ‖toLp 1 (x : Unitization 𝕜 A)‖₊
 
 lemma unitization_isometry_inr : Isometry fun x : A ↦ toLp 1 (x : Unitization 𝕜 A) :=
   AddMonoidHomClass.isometry_of_norm
-    ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 A)
+    ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 𝕜 A)
     unitization_norm_inr
 
 variable [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A]

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

@@ -128,6 +128,9 @@ lemma nnrpow_one (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ (1 : ℝ≥0) = a :=
   change cfcₙ (id : ℝ≥0 → ℝ≥0) a = a
   rw [cfcₙ_id ℝ≥0 a]
 
+lemma nnrpow_one_eqOn : (Set.Ici (0 : A)).EqOn (fun a : A => a ^ (1 : ℝ≥0)) id :=
+  fun _ ha => CFC.nnrpow_one _ ha
+
 lemma nnrpow_two (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ (2 : ℝ≥0) = a * a := by
   simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_two]
   change cfcₙ (fun z : ℝ≥0 => id z * id z) a = a * a
@@ -437,6 +440,10 @@ lemma one_rpow {x : ℝ} : (1 : A) ^ x = (1 : A) := by simp [rpow_def]
 lemma rpow_zero (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ (0 : ℝ) = 1 := by
   simp [rpow_def, cfc_const_one ℝ≥0 a]
 
+lemma rpow_zero_eqOn : (Set.Ici (0 : A)).EqOn (fun a => a ^ (0 : ℝ)) (fun _ => 1) := by
+  intro a ha
+  simp [rpow_zero a ha]
+
 lemma zero_rpow {x : ℝ} (hx : x ≠ 0) : rpow (0 : A) x = 0 := by simp [rpow, NNReal.zero_rpow hx]
 
 lemma rpow_natCast (a : A) (n : ℕ) (ha : 0 ≤ a := by cfc_tac) : a ^ (n : ℝ) = a ^ n := by

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean

@@ -7,8 +7,9 @@ module
 
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
 public import Mathlib.Analysis.CStarAlgebra.ApproximateUnit
-import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
 public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
 
 /-!
 # Integral representations of `rpow`
@@ -76,6 +77,13 @@ lemma rpowIntegrand₀₁_zero_right : rpowIntegrand₀₁ p t 0 = 0 := by simp
 lemma rpowIntegrand₀₁_zero_left (hp : 0 < p) : rpowIntegrand₀₁ p 0 x = 0 := by
   simp [rpowIntegrand₀₁, Real.zero_rpow hp.ne']
 
+lemma rpowIntegrand₀₁_eq_sub {p t : ℝ} (hp : p ≠ 1) (ht : 0 < t) :
+    rpowIntegrand₀₁ p t = fun x => t ^ (p - 1) - t ^ p * (t + x)⁻¹ := by
+  unfold rpowIntegrand₀₁
+  ext x
+  rw [mul_sub, ← rpow_neg_one, ← rpow_add' (by grind) (by grind)]
+  grind only
+
 lemma rpowIntegrand₀₁_nonneg (hp : 0 < p) (ht : 0 ≤ t) (hx : 0 ≤ x) :
     0 ≤ rpowIntegrand₀₁ p t x := by
   unfold rpowIntegrand₀₁
@@ -562,6 +570,31 @@ lemma exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂ [CompleteSpac
 
 end NonUnitalCFC
 
+section UnitalCStarAlgebra
+
+variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+
+/-- `rpowIntegrand₀₁ p t` is operator concave for all `p ∈ Ioo 0 1` -/
+lemma concaveOn_cfc_rpowIntegrand₀₁ {p t : ℝ} (hp : p ∈ Ioo 0 1) (ht : 0 < t) :
+    ConcaveOn ℝ (Ici (0 : A)) (cfc (rpowIntegrand₀₁ p t)) := by
+  have h₁ : (Ici (0 : A)).EqOn (cfc (rpowIntegrand₀₁ p t))
+      (fun x : A =>
+        algebraMap ℝ A (t ^ (p - 1)) - t ^ p • Ring.inverse (algebraMap ℝ A t + x)) := by
+    intro x hx
+    rw [rpowIntegrand₀₁_eq_sub (by grind) ht]
+    have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
+      fun_prop (disch := grind -abstractProof)
+    have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop
+    have hspectrum :  ∀ r ∈ spectrum ℝ x, t + r ≠ 0 := by grind
+    have := cfc_sub (fun _ : ℝ => t ^ (p - 1)) (fun z : ℝ => t ^ p * (t + z)⁻¹) x
+    rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
+        cfc_id' ..]
+  refine ConcaveOn.congr ?_ h₁.symm
+  refine ConcaveOn.sub (concaveOn_const _ (convex_Ici 0)) ?_
+  exact ConvexOn.smul (by positivity) <| CStarAlgebra.convexOn_ringInverse_algebraMap_add ht
+
+end UnitalCStarAlgebra
+
 section NonUnitalCStarAlgebra
 
 variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
@@ -583,6 +616,14 @@ lemma monotoneOn_cfcₙ_rpowIntegrand₀₁ {p : ℝ} {t : ℝ} (hp : p ∈ Ioo
     _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
       rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]
 
+open CStarAlgebra in
+/-- `rpowIntegrand₀₁ p t` is operator concave for all `p ∈ Ioo 0 1` and all `0 < t`. -/
+lemma concaveOn_cfcₙ_rpowIntegrand₀₁ {p : ℝ} {t : ℝ} (hp : p ∈ Ioo 0 1) (ht : 0 < t) :
+    ConcaveOn ℝ (Ici (0 : A)) (cfcₙ (rpowIntegrand₀₁ p t)) := by
+  apply concaveOn_cfcₙ_of_concaveOn_cfc
+  refine ConcaveOn.subset (concaveOn_cfc_rpowIntegrand₀₁ hp ht) inr_map_Ici_zero ?_
+  exact Convex.linear_image (convex_Ici _) (Unitization.inrHom ℝ ℂ A)
+
 end NonUnitalCStarAlgebra
 
 end CFC

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean

@@ -20,10 +20,11 @@ C⋆-algebra. The proof makes use of the integral representation of `rpow` in
 
 + `CFC.monotone_nnrpow`, `CFC.monotone_rpow`: `a ↦ a ^ p` is operator monotone for `p ∈ [0,1]`
 + `CFC.monotone_sqrt`: `CFC.sqrt` is operator monotone
++ `CFC.concaveOn_nnrpow`, `CFC.concaveOn_rpow`: `a ↦ a ^ p` is operator concave for `p ∈ [0,1]`
++ `CFC.concaveOn_sqrt`: `CFC.sqrt` is operator concave
 
 ## TODO
 
-+ Show operator concavity of `rpow` over `Icc 0 1`
 + Show that `rpow` over `Icc (-1) 0` is operator antitone and operator convex
 + Show operator convexity of `rpow` over `Icc 1 2`
 
@@ -88,6 +89,38 @@ lemma nnrpow_le_nnrpow {p : ℝ≥0} (hp : p ∈ Icc 0 1) {a b : A} (hab : a ≤
 lemma sqrt_le_sqrt (a b : A) (hab : a ≤ b) : sqrt a ≤ sqrt b :=
   monotone_sqrt hab
 
+/-- This is an intermediate result; use the more general `CFC.concaveOn_nnrpow` instead. -/
+private lemma concaveOn_nnrpow_Ioo {p : ℝ≥0} (hp : p ∈ Ioo 0 1) :
+    ConcaveOn ℝ (Ici (0 : A)) (fun a : A => a ^ p) := by
+  obtain ⟨μ, hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ A hp
+  have h₃' : (Ici 0).EqOn (fun a : A => a ^ p)
+      (fun a : A => ∫ t in Ioi 0, cfcₙ (rpowIntegrand₀₁ p t) a ∂μ) :=
+    fun a ha => (hμ a ha).2
+  refine ConcaveOn.congr ?_ h₃'.symm
+  refine integral_concaveOn_of_integrand_ae (convex_Ici _) ?_ fun a ha => (hμ a ha).1
+  filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
+  exact concaveOn_cfcₙ_rpowIntegrand₀₁ hp ht
+
+/-- `a ↦ a ^ p` is operator concave for `p ∈ [0,1]`. -/
+lemma concaveOn_nnrpow {p : ℝ≥0} (hp : p ∈ Icc 0 1) :
+    ConcaveOn ℝ (Ici (0 : A)) (fun a : A => a ^ p) := by
+  have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
+  rw [hIcc] at hp
+  obtain (hp | hp) | hp := hp
+  · exact concaveOn_nnrpow_Ioo hp
+  · simp only [mem_singleton_iff] at hp
+    simp only [hp, nnrpow_zero]
+    exact concaveOn_const _ (convex_Ici _)
+  · simp only [mem_singleton_iff] at hp
+    simp only [hp]
+    exact ConcaveOn.congr (concaveOn_id (convex_Ici _)) nnrpow_one_eqOn.symm
+
+/-- The square root is operator concave. -/
+lemma concaveOn_sqrt : ConcaveOn ℝ (Ici (0 : A)) (sqrt : A → A) := by
+  eta_expand
+  simp_rw [sqrt_eq_nnrpow]
+  exact concaveOn_nnrpow ⟨by norm_num, by norm_num⟩
+
 end NonUnitalCStarAlgebra
 
 section UnitalCStarAlgebra
@@ -115,6 +148,19 @@ lemma monotone_rpow {p : ℝ} (hp : p ∈ Icc 0 1) : Monotone (fun a : A => a ^
 lemma rpow_le_rpow {p : ℝ} (hp : p ∈ Icc 0 1) {a b : A} (hab : a ≤ b) :
     a ^ p ≤ b ^ p := monotone_rpow hp hab
 
+/-- `a ↦ a ^ p` is operator concave for `p ∈ [0,1]`. -/
+lemma concaveOn_rpow {p : ℝ} (hp : p ∈ Icc 0 1) :
+    ConcaveOn ℝ (Ici (0 : A)) (fun a : A => a ^ p) := by
+  let q : ℝ≥0 := ⟨p, hp.1⟩
+  change ConcaveOn ℝ (Ici (0 : A)) (fun a : A => a ^ (q : ℝ))
+  cases (zero_le q).lt_or_eq' with
+  | inl hq =>
+    simp_rw [← CFC.nnrpow_eq_rpow hq]
+    exact concaveOn_nnrpow hp
+  | inr hq =>
+    simp only [hq, NNReal.coe_zero]
+    exact ConcaveOn.congr (concaveOn_const _ (convex_Ici _)) rpow_zero_eqOn.symm
+
 end UnitalCStarAlgebra
 
 end CFC

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean

@@ -23,7 +23,7 @@ This file shows that `Ring.inverse` is convex on strictly positive operators.
 
 namespace CStarAlgebra
 
-open CFC
+open CFC Set
 
 variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
 
@@ -85,4 +85,22 @@ public lemma convexOn_ringInverse :
       _ = _ := by
         rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]
 
+public lemma convexOn_ringInverse_algebraMap_add {t : ℝ} (ht : 0 < t) :
+    ConvexOn ℝ (Ici (0 : A)) (fun x : A => Ring.inverse (algebraMap ℝ A t + x)) := by
+  have : ∀ x ∈ Ici (0 : A), IsStrictlyPositive (algebraMap ℝ A t + x) := by grind
+  let addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm (algebraMap ℝ A t, .id)
+  have haddl : Function.Injective addl := by intro _ _; simp [addl]
+  have hici : Ici (0 : A) = addl ⁻¹' (addl '' (Ici 0)) := by
+    rw [Set.preimage_image_eq _ haddl]
+  simp_rw [add_comm]
+  change ConvexOn ℝ (Ici 0) (Ring.inverse ∘ addl)
+  rw [hici]
+  apply ConvexOn.comp_affineMap
+  refine ConvexOn.subset CStarAlgebra.convexOn_ringInverse ?_ (Convex.affine_image _ (convex_Ici _))
+  simp only [AffineMap.toConstProdLinearMap_symm_apply, AffineMap.coe_add,
+    LinearMap.coe_toAffineMap, LinearMap.id_coe, AffineMap.coe_const, Pi.add_apply, id_eq,
+    Function.const_apply, image_add_right, preimage_add_const_Ici, sub_neg_eq_add, zero_add, addl]
+  exact fun x hx  => IsStrictlyPositive.of_le (by grind) hx
+
+
 end CStarAlgebra