feat(ProbabilisticTheory): effects

Physlib.lean

@@ -254,6 +254,14 @@ 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.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.QFT.AnomalyCancellation.Basic
 public import Physlib.QFT.AnomalyCancellation.GroupActions
 public import Physlib.QFT.PerturbationTheory.CreateAnnihilate

Physlib/ProbabilisticTheory/Effect/Basic.lean

@@ -0,0 +1,77 @@
+/-
+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
+
+variable {E : Type*} [OrderUnitSpace 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]
+
+/-- 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 Effect

Physlib/ProbabilisticTheory/Effect/Complement.lean

@@ -0,0 +1,98 @@
+/-
+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
+
+variable {E : Type*} [OrderUnitSpace 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
+
+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 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*} [OrderUnitSpace 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

Physlib/ProbabilisticTheory/Effect/Metric.lean

@@ -0,0 +1,106 @@
+/-
+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 Physlib.ProbabilisticTheory.OrderUnit.Archimedean
+public import Mathlib.Topology.MetricSpace.Defs
+
+/-!
+# The metric space of effects
+
+## i. Overview
+
+Effects sit inside `E`, so pulling back the order-unit norm along the inclusion `Effect E ↪ E`
+gives them a metric space structure for free.
+
+Effects also correspond to points of the order-unit-norm ball, by the affine rescaling
+`e ↦ 2 • e - 1` that turns `[0, 1]` into the symmetric `[-1, 1]` the norm itself ranges over.
+
+## ii. Key results
+
+- `Effect.dist_eq_orderUnitNorm` : the effect metric is the order-unit norm of the difference.
+- `Effect.equivBall` : effects correspond to points of the order-unit-norm ball.
+
+## iii. Table of contents
+
+- A. The effect metric
+- B. Effects as points of the order-unit-norm ball
+
+-/
+
+@[expose] public section
+
+open ArchimedeanOrderUnitSpace
+
+variable {E : Type*} [ArchimedeanOrderUnitSpace E]
+
+namespace Effect
+
+/-!
+
+## A. The effect metric
+
+-/
+
+/-- Effects, metrized by restricting the order-unit norm: pulling back the normed group structure
+on `E` along the inclusion `Effect E ↪ E` -/
+noncomputable instance : MetricSpace (Effect E) :=
+  letI := orderUnitNormedAddCommGroup (E := E)
+  MetricSpace.induced Subtype.val Subtype.val_injective inferInstance
+
+lemma dist_eq_orderUnitNorm (e f : Effect E) : dist e f = orderUnitNorm ((e : E) - (f : E)) := by
+  let := orderUnitNormedAddCommGroup (E := E)
+  exact dist_eq_norm (e : E) (f : E)
+
+/-!
+
+## B. Effects as points of the order-unit-norm ball
+
+-/
+
+/-- Doubling and re-centering an effect at the order unit lands in the order-unit-norm ball. -/
+lemma orderUnitNorm_two_smul_sub_one_le_one (e : Effect E) :
+    orderUnitNorm ((2 : ℝ) • (e : E) - 1) ≤ 1 := by
+  rw [orderUnitNorm_le_iff]
+  refine ⟨by norm_num, ?_, ?_⟩
+  · rw [one_smul, ← sub_nonneg,
+      show (2 : ℝ) • (e : E) - 1 - -(1 : E) = (2 : ℝ) • (e : E) from by module]
+    exact smul_nonneg (by norm_num) e.2.1
+  · rw [one_smul, ← sub_nonneg,
+      show (1 : E) - ((2 : ℝ) • (e : E) - 1) = (2 : ℝ) • (1 - (e : E)) from by module]
+    exact smul_nonneg (by norm_num) (sub_nonneg.mpr e.2.2)
+
+/-- Undoing the re-centering on a point of the order-unit-norm ball gives back an effect. -/
+lemma mem_effect_two_inv_smul_one_add (A : {A : E // orderUnitNorm A ≤ 1}) :
+    (2 : ℝ)⁻¹ • (1 + (A : E)) ∈ (Effect E : Set E) := by
+  obtain ⟨-, hAl, hAu⟩ := orderUnitNorm_le_iff.mp A.2
+  rw [one_smul] at hAl hAu
+  refine ⟨smul_nonneg (by norm_num) (by simpa using add_le_add (le_refl (1 : E)) hAl), ?_⟩
+  have h := add_le_add (le_refl (1 : E)) hAu
+  rw [show (1 : E) + 1 = (2 : ℝ) • (1 : E) from by module] at h
+  have h2 := smul_le_smul_of_nonneg_left h (show (0 : ℝ) ≤ (2 : ℝ)⁻¹ by norm_num)
+  rwa [smul_smul, inv_mul_cancel₀ (two_ne_zero), one_smul] at h2
+
+/-- Re-centering, then undoing it, returns the original effect. -/
+lemma two_inv_smul_one_add_two_smul_sub_one (e : Effect E) :
+    (2 : ℝ)⁻¹ • (1 + ((2 : ℝ) • (e : E) - 1)) = (e : E) := by module
+
+/-- Undoing the re-centering, then redoing it, returns the original ball point. -/
+lemma two_smul_two_inv_smul_one_add_sub_one (A : {A : E // orderUnitNorm A ≤ 1}) :
+    (2 : ℝ) • ((2 : ℝ)⁻¹ • (1 + (A : E))) - 1 = (A : E) := by
+  rw [smul_smul, mul_inv_cancel₀ (two_ne_zero), one_smul]
+  module
+
+/-- Effects correspond to points of the order-unit-norm ball by doubling and re-centering at the
+order unit: `e ↦ 2 • e - 1`, with inverse `A ↦ (1 + A) / 2`. -/
+noncomputable def equivBall : Effect E ≃ {A : E // orderUnitNorm A ≤ 1} where
+  toFun e := ⟨(2 : ℝ) • (e : E) - 1, orderUnitNorm_two_smul_sub_one_le_one e⟩
+  invFun A := ⟨(2 : ℝ)⁻¹ • (1 + (A : E)), mem_effect_two_inv_smul_one_add A⟩
+  left_inv e := Subtype.ext (two_inv_smul_one_add_two_smul_sub_one e)
+  right_inv A := Subtype.ext (two_smul_two_inv_smul_one_add_sub_one A)
+
+end Effect