Advance provider-backed Lieb theorem surfaces

HighDimProb/Analysis/OpenJensen.lean

@@ -0,0 +1,89 @@
+import Mathlib.Analysis.Convex.Continuous
+import Mathlib.Analysis.Convex.Integral
+
+/-!
+# Open-domain Jensen
+
+This module upgrades Mathlib's closed-domain integral Jensen inequality to the
+case of a concave function on an open convex set, provided the Bochner mean is
+known to stay in the domain.
+-/
+
+noncomputable section
+
+open MeasureTheory Set
+open scoped Topology
+
+section ClosureHypograph
+
+variable {E : Type*} [TopologicalSpace E]
+variable {s : Set E} {g : E → Real}
+
+private theorem le_of_mem_closure_hypograph_of_isOpen
+    (hgc : ContinuousOn g s) (hsOpen : IsOpen s)
+    {x : E} (hx : x ∈ s) {r : Real}
+    (hr : (x, r) ∈ closure {p : E × Real | p.1 ∈ s ∧ p.2 ≤ g p.1}) :
+    r ≤ g x := by
+  let hypograph : Set (E × Real) := {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
+  let strictEpigraph : Set (E × Real) := {p | p.1 ∈ s ∧ g p.1 < p.2}
+  by_contra hle
+  have hxr : (x, r) ∈ strictEpigraph := by
+    exact ⟨hx, lt_of_not_ge hle⟩
+  have hmap :
+      ContinuousOn (fun p : E × Real => (g p.1, p.2)) (s ×ˢ (Set.univ : Set Real)) :=
+    hgc.prodMap continuousOn_id
+  have hOpenStrict : IsOpen strictEpigraph := by
+    have :
+        IsOpen
+          ((s ×ˢ (Set.univ : Set Real)) ∩
+            (fun p : E × Real => (g p.1, p.2)) ⁻¹'
+              {q : Real × Real | q.1 < q.2}) :=
+      hmap.isOpen_inter_preimage (hsOpen.prod isOpen_univ)
+        (isOpen_lt continuous_fst continuous_snd)
+    simpa [strictEpigraph, Set.prod_eq] using this
+  rcases mem_closure_iff_nhds.mp hr strictEpigraph (hOpenStrict.mem_nhds hxr) with
+    ⟨p, hpStrict, hpHypo⟩
+  exact (not_lt_of_ge hpHypo.2) hpStrict.2
+
+end ClosureHypograph
+
+variable {α E : Type*}
+variable [MeasurableSpace α]
+variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+variable [FiniteDimensional ℝ E]
+variable {μ : Measure α} [IsProbabilityMeasure μ]
+variable {s : Set E} {f : α → E} {g : E → Real}
+
+namespace ConcaveOn
+
+/-- Integral Jensen for a concave function on a convex open domain.
+
+Mathlib already provides `ConcaveOn.le_map_integral` for convex closed domains.
+This wrapper uses the convex hypograph together with continuity on open convex
+sets to remove the closedness assumption, replacing it with an explicit
+hypothesis that the Bochner mean stays in the domain.
+-/
+theorem le_map_integral_of_mem_open
+    (hg : ConcaveOn ℝ s g) (hsOpen : IsOpen s)
+    (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ)
+    (hmean : ∫ x, f x ∂μ ∈ s) :
+    ∫ x, g (f x) ∂μ ≤ g (∫ x, f x ∂μ) := by
+  let hypograph : Set (E × Real) := {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
+  have hmem :
+      ∀ᵐ x ∂μ, (f x, g (f x)) ∈ hypograph := by
+    filter_upwards [hfs] with x hx
+    exact ⟨hx, le_rfl⟩
+  have hpairInt : Integrable (fun x => (f x, g (f x))) μ :=
+    hfi.prodMk <| by simpa [Function.comp] using hgi
+  have hpairClosure :
+      ∫ x, (f x, g (f x)) ∂μ ∈ closure hypograph := by
+    exact hg.convex_hypograph.closure.integral_mem isClosed_closure
+      (hmem.mono fun _ hx => subset_closure hx) hpairInt
+  have hpair :
+      (∫ x, f x ∂μ, ∫ x, g (f x) ∂μ) ∈ closure hypograph := by
+    rw [integral_pair hfi (by simpa [Function.comp] using hgi)] at hpairClosure
+    exact hpairClosure
+  exact le_of_mem_closure_hypograph_of_isOpen
+    (s := s) (g := g) (hg.continuousOn hsOpen) hsOpen hmean hpair
+
+end ConcaveOn

HighDimProb/Analysis/SelfAdjointCarrier.lean

@@ -0,0 +1,142 @@
+import Mathlib
+import Mathlib.Topology.Algebra.Module.Star
+
+/-!
+# Self-adjoint carrier bridge
+
+This module bridges the two Mathlib carriers used for real self-adjoint elements:
+`selfAdjoint A` and the subtype carrier of `selfAdjoint.submodule Real A`.
+-/
+
+noncomputable section
+
+namespace selfAdjoint
+
+section Carrier
+
+variable {A : Type*}
+variable [NormedAddCommGroup A] [NormedSpace Real A]
+variable [StarAddMonoid A] [StarModule Real A]
+
+instance : ContinuousENorm (selfAdjoint A) where
+  toENorm := inferInstance
+  continuous_enorm :=
+    (continuous_enorm : Continuous fun a : A => enorm a).comp continuous_subtype_val
+
+instance : ContinuousENorm (selfAdjoint.submodule Real A) where
+  toENorm := inferInstance
+  continuous_enorm :=
+    (continuous_enorm : Continuous fun a : A => enorm a).comp continuous_subtype_val
+
+/-- The self-adjoint carrier inherits continuous real scalar multiplication
+from the ambient normed real vector space. This lets finite-dimensional linear
+equivalences on `selfAdjoint A` upgrade to continuous linear equivalences. -/
+instance instContinuousSMulSelfAdjoint : ContinuousSMul Real (selfAdjoint A) :=
+  Topology.IsInducing.continuousSMul (g := fun x : selfAdjoint A => (x : A))
+    (f := fun r : Real => r) Topology.IsInducing.subtypeVal continuous_id (by intro c x; rfl)
+
+omit [NormedSpace Real A] [StarModule Real A] in
+theorem isClosed [ContinuousStar A] : IsClosed (selfAdjoint A : Set A) := by
+  simpa [selfAdjoint.mem_iff] using
+    (isClosed_eq (continuous_star : Continuous fun a : A => star a) continuous_id :
+      IsClosed {a : A | star a = a})
+
+instance instCompleteSpaceSelfAdjoint
+    [CompleteSpace A] [ContinuousStar A] : CompleteSpace (selfAdjoint A) := by
+  let hClosed : IsClosed (selfAdjoint A : Set A) := selfAdjoint.isClosed (A := A)
+  exact hClosed.completeSpace_coe
+/-- Continuous linear equivalence between `selfAdjoint A` and the subtype carrier
+of `selfAdjoint.submodule Real A`. -/
+@[simps!]
+def submoduleContinuousLinearEquiv :
+    ContinuousLinearEquiv (RingHom.id Real) (selfAdjoint A) (selfAdjoint.submodule Real A) where
+  toLinearEquiv :=
+    { toFun := fun x => Subtype.mk x.1 x.2
+      invFun := fun x => Subtype.mk x.1 x.2
+      left_inv := fun _ => rfl
+      right_inv := fun _ => rfl
+      map_add' := fun _ _ => rfl
+      map_smul' := fun _ _ => rfl }
+  continuous_toFun := continuous_subtype_val.subtype_mk _
+  continuous_invFun := continuous_subtype_val.subtype_mk _
+
+instance instFiniteDimensionalSelfAdjoint [FiniteDimensional Real A] :
+    FiniteDimensional Real (selfAdjoint A) := by
+  letI : FiniteDimensional Real (selfAdjoint.submodule Real A) :=
+    FiniteDimensional.finiteDimensional_submodule (selfAdjoint.submodule Real A)
+  exact LinearEquiv.finiteDimensional
+    (submoduleContinuousLinearEquiv (A := A)).toLinearEquiv.symm
+
+@[simp]
+theorem coe_submoduleContinuousLinearEquiv_apply (x : selfAdjoint A) :
+    ((submoduleContinuousLinearEquiv (A := A) x : selfAdjoint.submodule Real A) : A) = x :=
+  rfl
+
+@[simp]
+theorem coe_submoduleContinuousLinearEquiv_symm_apply (x : selfAdjoint.submodule Real A) :
+    ((submoduleContinuousLinearEquiv (A := A)).symm x : A) = x :=
+  rfl
+
+/-- The coercion from `selfAdjoint A` to `A` as a continuous linear map. -/
+def subtypeL : ContinuousLinearMap (RingHom.id Real) (selfAdjoint A) A :=
+  (selfAdjoint.submodule Real A).subtypeL.comp
+    (submoduleContinuousLinearEquiv (A := A)).toContinuousLinearMap
+
+@[simp]
+theorem subtypeL_apply (x : selfAdjoint A) : subtypeL (A := A) x = (x : A) :=
+  rfl
+
+section Integral
+
+variable {X : Type*}
+variable [MeasurableSpace X] {mu : MeasureTheory.Measure X}
+
+/-- Lift ambient Bochner integrability into the `selfAdjoint` carrier when all values are
+pointwise self-adjoint. -/
+theorem integrable_mk_of_integrable_coe
+    [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul Real A]
+    [Invertible (2 : Real)]
+    {F : X -> A} (hF : MeasureTheory.Integrable F mu) (hSA : forall x, IsSelfAdjoint (F x)) :
+    MeasureTheory.Integrable (fun x => ((Subtype.mk (F x) (hSA x)) : selfAdjoint A)) mu := by
+  have hpart :
+      MeasureTheory.Integrable (fun x => selfAdjointPartL (R := Real) (A := A) (F x)) mu :=
+    (selfAdjointPartL (R := Real) (A := A)).integrable_comp hF
+  refine hpart.congr <| Filter.Eventually.of_forall fun x => ?_
+  simpa [selfAdjointPartL] using (hSA x).selfAdjointPart_apply (R := Real)
+
+variable [CompleteSpace A]
+
+theorem coe_integral [hSA : CompleteSpace (selfAdjoint A)] {F : X -> selfAdjoint A}
+    (hF : MeasureTheory.Integrable F mu) :
+    ((MeasureTheory.integral mu F : selfAdjoint A) : A) =
+      MeasureTheory.integral mu (fun x => (F x : A)) := by
+  simpa [subtypeL_apply] using
+    (@ContinuousLinearMap.integral_comp_comm X (selfAdjoint A) A _ mu Real _ _ _ _ _ _ _ _ hSA
+      (subtypeL (A := A)) F hF).symm
+
+end Integral
+
+end Carrier
+
+section Part
+
+variable {A : Type*}
+variable [NormedAddCommGroup A] [NormedSpace Real A]
+variable [StarAddMonoid A] [StarModule Real A]
+variable [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul Real A]
+variable [Invertible (2 : Real)]
+
+/-- `selfAdjointPartL` retargeted to the submodule carrier. -/
+def partSubmoduleL : ContinuousLinearMap (RingHom.id Real) A (selfAdjoint.submodule Real A) :=
+  (submoduleContinuousLinearEquiv (A := A)).toContinuousLinearMap.comp
+    (selfAdjointPartL (R := Real) (A := A))
+
+@[simp]
+theorem coe_partSubmoduleL_apply (x : A) :
+    ((partSubmoduleL (A := A) x : selfAdjoint.submodule Real A) : A) =
+      ((selfAdjointPartL (R := Real) (A := A) x : selfAdjoint A) : A) :=
+  rfl
+
+end Part
+
+end selfAdjoint

HighDimProb/Analysis/SelfAdjointPositiveDomain.lean

@@ -0,0 +1,94 @@
+import Mathlib.Analysis.CStarAlgebra.Matrix
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
+import Mathlib.Analysis.Normed.Algebra.Spectrum
+import HighDimProb.Analysis.SelfAdjointCarrier
+import Mathlib.Analysis.Matrix.Order
+
+/-!
+# Strictly positive self-adjoint matrix domain
+
+This module packages the strictly positive real matrix domain in the
+`selfAdjoint` carrier used by the provider's Jensen-side transport work.
+
+It only exposes carrier/domain wrappers and small reusable set-level API.
+It does not prove any Lieb/Jensen exact statement.
+-/
+
+noncomputable section
+
+namespace HighDimProb
+
+open Set Topology
+open scoped MatrixOrder Matrix.Norms.L2Operator
+open Matrix
+
+/-- The strictly positive real self-adjoint matrices, viewed in the
+`selfAdjoint` carrier. -/
+abbrev selfAdjointStrictlyPositiveSet (n : Nat) :
+    Set (selfAdjoint (Matrix (Fin n) (Fin n) ℝ)) :=
+  { M | IsStrictlyPositive (M : Matrix (Fin n) (Fin n) ℝ) }
+
+@[simp]
+theorem mem_selfAdjointStrictlyPositiveSet {n : Nat}
+    {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ)} :
+    M ∈ selfAdjointStrictlyPositiveSet n ↔
+      IsStrictlyPositive (M : Matrix (Fin n) (Fin n) ℝ) :=
+  Iff.rfl
+
+@[simp]
+theorem mem_selfAdjointStrictlyPositiveSet_iff_posDef {n : Nat}
+    {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ)} :
+    M ∈ selfAdjointStrictlyPositiveSet n ↔
+      ((M : Matrix (Fin n) (Fin n) ℝ)).PosDef := by
+  rw [mem_selfAdjointStrictlyPositiveSet, Matrix.isStrictlyPositive_iff_posDef]
+
+/-- The carrier-form strictly positive domain is convex. -/
+theorem convex_selfAdjointStrictlyPositiveSet (n : Nat) :
+    Convex ℝ (selfAdjointStrictlyPositiveSet n) := by
+  classical
+  intro x hx y hy a b ha hb hab
+  have hxpd : ((x : Matrix (Fin n) (Fin n) ℝ)).PosDef :=
+    (mem_selfAdjointStrictlyPositiveSet_iff_posDef).mp hx
+  have hypd : ((y : Matrix (Fin n) (Fin n) ℝ)).PosDef :=
+    (mem_selfAdjointStrictlyPositiveSet_iff_posDef).mp hy
+  by_cases ha0 : a = 0
+  · have hb1 : b = 1 := by nlinarith [hab, ha0]
+    subst ha0 hb1
+    simpa using hy
+  · by_cases hb0 : b = 0
+    · have ha1 : a = 1 := by nlinarith [hab, hb0]
+      subst hb0 ha1
+      simpa using hx
+    · have ha_pos : 0 < a := lt_of_le_of_ne ha (Ne.symm ha0)
+      have hb_pos : 0 < b := lt_of_le_of_ne hb (Ne.symm hb0)
+      have hsum :
+          (a • ((x : Matrix (Fin n) (Fin n) ℝ)) +
+              b • ((y : Matrix (Fin n) (Fin n) ℝ))).PosDef :=
+        (hxpd.smul ha_pos).add (hypd.smul hb_pos)
+      exact (mem_selfAdjointStrictlyPositiveSet_iff_posDef).mpr hsum
+
+private theorem isOpen_matrix_strictlyPositiveOnSelfAdjointCarrier (n : Nat) :
+    IsOpen {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ) |
+      spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ) ⊆ Ioi (0 : ℝ)} := by
+  let f : selfAdjoint (Matrix (Fin n) (Fin n) ℝ) → Set ℝ :=
+    fun M => spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ)
+  have hf : UpperHemicontinuous f := by
+    simpa [f] using
+      (upperHemicontinuous_spectrum ℝ (Matrix (Fin n) (Fin n) ℝ)).comp continuous_subtype_val
+  exact (upperHemicontinuous_iff_isOpen_preimage_Iic.mp hf) (Ioi (0 : ℝ)) isOpen_Ioi
+
+/-- The strictly positive self-adjoint carrier domain is open. -/
+theorem isOpen_selfAdjointStrictlyPositiveSet (n : Nat) :
+    IsOpen (selfAdjointStrictlyPositiveSet n) := by
+  rw [show selfAdjointStrictlyPositiveSet n =
+      {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ) |
+        spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ) ⊆ Ioi (0 : ℝ)} from by
+        ext M
+        change IsStrictlyPositive (M : Matrix (Fin n) (Fin n) ℝ) ↔
+          spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ) ⊆ Ioi (0 : ℝ)
+        simpa using
+          (StarOrderedRing.isStrictlyPositive_iff_spectrum_pos
+            (a := (M : Matrix (Fin n) (Fin n) ℝ)) M.2)]
+  exact isOpen_matrix_strictlyPositiveOnSelfAdjointCarrier n
+
+end HighDimProb