feat(ProbabilisticTheory): state separation

Physlib.lean

@@ -253,6 +253,24 @@ public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa
 public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.ZMod
 public import Physlib.Particles.SuperSymmetry.SU5.FieldLabels
 public import Physlib.Particles.SuperSymmetry.SU5.Potential
+public import Physlib.ProbabilisticTheory.Channel.Basic
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Physlib.ProbabilisticTheory.Effect.Complement
+public import Physlib.ProbabilisticTheory.Effect.Convex
+public import Physlib.ProbabilisticTheory.Effect.Metric
+public import Physlib.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+public import Physlib.ProbabilisticTheory.State.Basic
+public import Physlib.ProbabilisticTheory.State.Convex
+public import Physlib.ProbabilisticTheory.State.Discrimination
+public import Physlib.ProbabilisticTheory.State.Metric
+public import Physlib.ProbabilisticTheory.State.Pairing
+public import Physlib.ProbabilisticTheory.State.Separation
+public import Physlib.ProbabilisticTheory.State.WeightEquivalence
+public import Physlib.ProbabilisticTheory.Weight.Basic
+public import Physlib.ProbabilisticTheory.Weight.Extension
 public import Physlib.QFT.AnomalyCancellation.Basic
 public import Physlib.QFT.AnomalyCancellation.GroupActions
 public import Physlib.QFT.PerturbationTheory.CreateAnnihilate

Physlib/ProbabilisticTheory/Channel/Basic.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Algebra.Order.Module.PositiveLinearMap
+
+/-!
+# Positive unital maps
+
+## i. Overview
+
+A channel is the most general physical transformation the theory allows: time evolution, noise,
+or a measurement whose outcome is never recorded. Whatever it does, it must send observables to
+observables without turning a possible outcome negative, and it must leave the certain outcome
+certain. In the Heisenberg picture, where a channel acts on observables rather than states,
+that's exactly a positive linear map preserving the distinguished unit.
+
+## ii. Key results
+
+- `UnitalPositiveLinearMap` : a positive linear map preserving `1`, notated `E →ₚ₁[R] F`.
+- `UnitalPositiveLinearMap.ofLinearMap` : bundle a linear map after checking positivity and
+  unitality.
+
+## iii. Table of contents
+
+- A. Unital positive linear maps
+- B. Constructing unital positive linear maps
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Unital positive linear maps
+
+-/
+
+/-- A positive linear map preserving `1`. -/
+structure UnitalPositiveLinearMap (R E F : Type*) [Semiring R]
+    [AddCommMonoid E] [PartialOrder E] [AddCommMonoid F] [PartialOrder F]
+    [Module R E] [Module R F] [One E] [One F] extends E →ₚ[R] F where
+  /-- A unital positive linear map preserves the order unit. -/
+  map_one' : toPositiveLinearMap 1 = 1
+
+/-- Notation for positive unital linear maps. -/
+notation:25 E " →ₚ₁[" R:25 "] " F:0 => UnitalPositiveLinearMap R E F
+
+namespace UnitalPositiveLinearMap
+
+variable {R E F : Type*} [Semiring R]
+  [AddCommMonoid E] [PartialOrder E] [AddCommMonoid F] [PartialOrder F]
+  [Module R E] [Module R F] [One E] [One F]
+
+instance : FunLike (E →ₚ₁[R] F) E F where
+  coe f := f.toFun
+  coe_injective f g h := by
+    cases f
+    cases g
+    congr
+    exact DFunLike.coe_injective h
+
+instance : LinearMapClass (E →ₚ₁[R] F) R E F where
+  map_add f := map_add f.toLinearMap
+  map_smulₛₗ f := f.toLinearMap.map_smul'
+
+instance : OrderHomClass (E →ₚ₁[R] F) E F where
+  map_rel f {_ _} h := f.monotone' h
+
+instance : OneHomClass (E →ₚ₁[R] F) E F where
+  map_one f := f.map_one'
+
+@[ext]
+lemma ext {f g : E →ₚ₁[R] F} (h : ∀ x, f x = g x) : f = g :=
+  DFunLike.ext f g h
+
+/-- Unital positive linear maps are determined by their underlying linear map. -/
+lemma toLinearMap_injective : Function.Injective (fun f : E →ₚ₁[R] F => f.toLinearMap) :=
+  fun _ _ h => ext fun x => congrArg (fun k : E →ₗ[R] F => k x) h
+
+end UnitalPositiveLinearMap
+
+namespace UnitalPositiveLinearMap
+
+variable {R E F : Type*} [Semiring R]
+  [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E]
+  [AddCommGroup F] [PartialOrder F] [IsOrderedAddMonoid F]
+  [Module R E] [Module R F] [One E] [One F]
+
+/-!
+
+## B. Constructing unital positive linear maps
+
+-/
+
+/-- Bundle a linear map after proving only positivity and preservation of `1`. -/
+def ofLinearMap (f : E →ₗ[R] F) (hpos : ∀ x, 0 ≤ x → 0 ≤ f x) (hone : f 1 = 1) : E →ₚ₁[R] F where
+  toPositiveLinearMap := PositiveLinearMap.mk₀ f hpos
+  map_one' := hone
+
+end UnitalPositiveLinearMap

Physlib/ProbabilisticTheory/Effect/Basic.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Order.Interval.Set.Defs
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+
+/-!
+# Effects
+
+## i. Overview
+
+An effect models a yes/no measurement outcome, ranging continuously between the impossible
+outcome `0` and the certain outcome `1`. Formally, it is a point of the order interval `[0, 1]`
+inside `E`. For self-adjoint matrices, effects are exactly the operators `0 ≤ M ≤ 1` — the
+elements of a POVM.
+
+## ii. Key results
+
+- `Effect` : a bounded measurement outcome, the order interval `[0, 1]`.
+- `Effect.mem_iff_mem_posCone_and_one_sub_mem_posCone` : an effect is exactly a positive element
+  whose complement from the order unit is also positive.
+- `Effect.exists_pos_smul_mem` : every positive observable becomes an effect after scaling it down
+  enough.
+
+## iii. Table of contents
+
+- A. Effects
+
+## iv. References
+
+- G. Ludwig, *Foundations of Quantum Mechanics I*, Springer, 1983.
+  <https://link.springer.com/book/10.1007/978-3-642-86751-4>
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Effects
+
+-/
+
+/-- A bounded measurement outcome. -/
+abbrev Effect (E : Type*) [PartialOrder E] [One E] [Zero E] := Set.Icc (0 : E) 1
+
+namespace Effect
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+/-- An effect is a positive element whose complement from the order unit is positive. -/
+lemma mem_iff_mem_posCone_and_one_sub_mem_posCone {A : E} :
+    A ∈ (Effect E : Set E) ↔ A ∈ PosCone E ∧ 1 - A ∈ PosCone E := by
+  simp only [Set.mem_Icc, PointedCone.mem_positive, sub_nonneg]
+
+end OrderedVectorSpace
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-- Every nonnegative observable becomes an effect after scaling it down by a large enough
+positive real: the effect interval reaches in every direction the positive cone does. -/
+lemma exists_pos_smul_mem {B : E} (hB : 0 ≤ B) :
+    ∃ r : ℝ, 0 < r ∧ r • B ∈ (Effect E : Set E) := by
+  obtain ⟨n, hn⟩ := OrderUnitSpace.exists_nsmul_one_le B
+  have hn1 : (0 : ℝ) < (n : ℝ) + 1 := by positivity
+  refine ⟨((n : ℝ) + 1)⁻¹, by positivity, smul_nonneg (by positivity) hB, ?_⟩
+  have hBr : B ≤ ((n : ℝ) + 1) • (1 : E) :=
+    calc
+      B ≤ n • (1 : E) := hn
+      _ = (n : ℝ) • (1 : E) := (Nat.cast_smul_eq_nsmul ℝ n (1 : E)).symm
+      _ ≤ ((n : ℝ) + 1) • (1 : E) :=
+        smul_le_smul_of_nonneg_right (by linarith) OrderUnitSpace.one_nonneg
+  have hs := smul_le_smul_of_nonneg_left hBr (by positivity : (0 : ℝ) ≤ ((n : ℝ) + 1)⁻¹)
+  simpa [smul_smul, hn1.ne'] using hs
+
+end OrderUnitSpace
+
+end Effect

Physlib/ProbabilisticTheory/Effect/Complement.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Physlib.ProbabilisticTheory.Effect.Convex
+public import Mathlib.Tactic.Module
+
+/-!
+# Complementary effects
+
+## i. Overview
+
+The complement of an effect `e` is the yes/no test that fires exactly when `e` doesn't: `1 - e`.
+Physically, a state's probability of "no" is always `1` minus its probability of "yes".
+
+## ii. Key results
+
+- `Effect.complement` : the complementary effect `1 - e`.
+- `Effect.complement_antitone` : the complement reverses order.
+- `Effect.complement_mix` : the complement of a mixture is the mixture of the complements.
+
+## iii. Table of contents
+
+- A. The complement
+- B. Monotonicity of the complement
+- C. The complement and mixtures
+
+-/
+
+@[expose] public section
+
+namespace Effect
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+/-!
+
+## A. The complement
+
+-/
+
+/-- The complementary effect. -/
+def complement (e : Effect E) : Effect E :=
+  ⟨1 - e.1, sub_nonneg.mpr e.2.2, sub_le_self 1 e.2.1⟩
+
+@[simp]
+lemma complement_complement (e : Effect E) : complement (complement e) = e := by
+  apply Subtype.ext
+  simp [complement]
+
+/-!
+
+## B. Monotonicity of the complement
+
+-/
+
+/-- The complement reverses order: a more certain test's complement is a less certain one. -/
+lemma complement_antitone : Antitone (complement (E := E)) :=
+  fun _ _ h => sub_le_sub_left (show (_ : E) ≤ _ from h) 1
+
+end OrderedVectorSpace
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+instance : Zero (Effect E) := ⟨0, le_refl 0, OrderUnitSpace.one_nonneg⟩
+instance : One (Effect E) := ⟨1, OrderUnitSpace.one_nonneg, le_refl 1⟩
+instance : Nonempty (Effect E) := ⟨0⟩
+
+@[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl
+
+@[simp] lemma coe_one : ((1 : Effect E) : E) = 1 := rfl
+
+@[simp]
+lemma complement_zero : complement (0 : Effect E) = 1 := by
+  apply Subtype.ext
+  simp [complement]
+
+@[simp]
+lemma complement_one : complement (1 : Effect E) = 0 := by
+  apply Subtype.ext
+  simp [complement]
+
+/-!
+
+## C. The complement and mixtures
+
+-/
+
+/-- Mixing commutes with taking the complement. -/
+lemma complement_mix (e f : Effect E) (t : unitInterval) :
+    complement (mix e f t) = mix (complement e) (complement f) t := by
+  apply Subtype.ext
+  show (1 : E) - ((t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E))
+      = (t : ℝ) • ((1 : E) - (e : E)) + (1 - (t : ℝ)) • ((1 : E) - (f : E))
+  module
+
+end OrderUnitSpace
+
+end Effect

Physlib/ProbabilisticTheory/Effect/Convex.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Mathlib.Topology.UnitInterval
+
+/-!
+# Convexity and mixtures of effects
+
+## i. Overview
+
+The effect interval `[0, 1]` is convex: randomizing between two effects with some probability
+gives back an effect. Physically, flipping a biased coin to decide which of two measurements to
+actually run is itself a legitimate measurement.
+
+## ii. Key results
+
+- `Effect.convex` : the effect interval is convex.
+- `Effect.mix` : randomize between two effects with a given probability.
+
+## iii. Table of contents
+
+- A. Convexity and mixtures of effects
+
+-/
+
+@[expose] public section
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+namespace Effect
+
+/-!
+
+## A. Convexity and mixtures of effects
+
+-/
+
+/-- The effect interval is convex. -/
+lemma convex : Convex ℝ (Effect E : Set E) := convex_Icc 0 1
+
+/-- Randomize between two effects with probability `t` of testing the first. -/
+noncomputable def mix (e f : Effect E) (t : unitInterval) : Effect E :=
+  ⟨(t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E),
+    convex e.2 f.2 t.2.1 (sub_nonneg.mpr t.2.2) (by ring)⟩
+
+/-- Evaluation of a mixture is the pointwise convex combination. -/
+@[simp]
+lemma coe_mix (e f : Effect E) (t : unitInterval) :
+    ((mix e f t : Effect E) : E) = (t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E) := rfl
+
+end Effect