refactor: Fix build

.github/workflows/build.yml

@@ -6,6 +6,7 @@ on:
   pull_request:
     branches:
       - master
+  merge_group:
 
 name: Style linters
 

Physlib/ProbabilisticTheory/Effect/Basic.lean

@@ -39,6 +39,8 @@ elements of a POVM.
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 /-!
 
 ## A. Effects
@@ -86,3 +88,5 @@ lemma exists_pos_smul_mem {B : E} (hB : 0 ≤ B) :
   exact hn.trans (smul_le_smul_of_nonneg_right (by linarith) one_nonneg)
 
 end Effect
+
+end ProbabilisticTheory

Physlib/ProbabilisticTheory/Effect/Complement.lean

@@ -31,6 +31,8 @@ Physically, a state's probability of "no" is always `1` minus its probability of
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 namespace Effect
 
 variable {E : Type*} [OrderUnitSpace E]
@@ -80,3 +82,5 @@ lemma complement_mix (e f : Effect E) (t : unitInterval) :
   ext; simp; module
 
 end Effect
+
+end ProbabilisticTheory

Physlib/ProbabilisticTheory/Effect/Convex.lean

@@ -30,6 +30,8 @@ actually run is itself a legitimate measurement.
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 variable {E : Type*} [OrderUnitSpace E]
 
 namespace Effect
@@ -54,3 +56,5 @@ 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
+
+end ProbabilisticTheory

Physlib/ProbabilisticTheory/Effect/Metric.lean

@@ -32,6 +32,8 @@ Effects also correspond to points of the order-unit-norm ball, by the affine res
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 open ArchimedeanOrderUnitSpace
 
 variable {E : Type*} [ArchimedeanOrderUnitSpace E]
@@ -105,3 +107,5 @@ noncomputable def effectEquiv : Effect E ≃ {A : E // orderUnitNorm A ≤ 1} wh
   right_inv A := Subtype.ext (two_smul_two_inv_smul_one_add_sub_one (A : E))
 
 end Effect
+
+end ProbabilisticTheory

Physlib/ProbabilisticTheory/Effect/Sharp.lean

@@ -30,6 +30,8 @@ be written as a nontrivial mixture of two distinct effects. Sharp effects genera
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 namespace Effect
 
 variable {E : Type*} [OrderUnitSpace E]
@@ -70,3 +72,5 @@ lemma isSharp_one : IsSharp (1 : Effect E) :=
   complement_zero (E := E) ▸ isSharp_complement isSharp_zero
 
 end Effect
+
+end ProbabilisticTheory

PhyslibAlpha.lean

@@ -123,10 +123,6 @@ public import PhyslibAlpha.ProbabilisticTheory.Dynamics.Generator
 public import PhyslibAlpha.ProbabilisticTheory.Dynamics.GeneratorIsDerivation
 public import PhyslibAlpha.ProbabilisticTheory.Dynamics.OneParameterGroup
 public import PhyslibAlpha.ProbabilisticTheory.Effect.Basic
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Complement
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Convex
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Metric
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
 public import PhyslibAlpha.ProbabilisticTheory.Examples.GBit
 public import PhyslibAlpha.ProbabilisticTheory.Examples.NormCone
 public import PhyslibAlpha.ProbabilisticTheory.Examples.Qubit

PhyslibAlpha/ProbabilisticTheory/CStarAlgebra/SharpEffect.lean

@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.OrderUnit
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 public import Mathlib.Analysis.CStarAlgebra.Basic
 public import Mathlib.Algebra.Module.Torsion.Free

PhyslibAlpha/ProbabilisticTheory/Channel/Operation.lean

@@ -5,7 +5,7 @@ Authors: Tom Ole Diem
 -/
 module
 
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 public import PhyslibAlpha.ProbabilisticTheory.Channel.Normal
 public import PhyslibAlpha.ProbabilisticTheory.State.Basic
 public import Mathlib.Algebra.Order.Module.PositiveLinearMap

PhyslibAlpha/ProbabilisticTheory/Classical/FiniteSystem.lean

@@ -5,7 +5,7 @@ Authors: Tom Ole Diem
 -/
 module
 
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
 public import PhyslibAlpha.ProbabilisticTheory.State.Convex
 public import PhyslibAlpha.Mathematics.Geometry.Simplex

PhyslibAlpha/ProbabilisticTheory/Effect/Basic.lean

@@ -5,30 +5,24 @@ Authors: Tom Ole Diem
 -/
 module
 
-public import Mathlib.Tactic.Positivity
-public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+public import Physlib.ProbabilisticTheory.Effect.Basic
 
 /-!
-# Effects
+# Orthogonal 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.
+Two effects are orthogonal when their sum is still an effect, that is, still bounded by the order
+unit. Their partial sum is then again an effect.
 
 ## 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.
+- `Effect.Orthogonal` : two effects whose sum is bounded by the order unit.
+- `Effect.addOfOrthogonal` : the partial sum of two orthogonal effects.
 
 ## iii. Table of contents
 
-- A. Effects
+- A. Orthogonal effects
 
 ## iv. References
 
@@ -43,40 +37,14 @@ namespace ProbabilisticTheory
 
 /-!
 
-## A. Effects
+## A. Orthogonal 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
-
-open OrderUnitSpace
-
 variable {E : Type*} [OrderUnitSpace E]
 
-instance instZero : Zero (Effect E) := ⟨0, le_refl 0, one_nonneg⟩
-
-instance instOne : One (Effect E) := ⟨1, one_nonneg, le_refl 1⟩
-
-instance instNonempty : Nonempty (Effect E) := ⟨0⟩
-
-@[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl
-
-@[simp] lemma coe_one : ((1 : Effect E) : E) = 1 := rfl
-
 /-- Two effects are orthogonal when their sum is still bounded by the order unit. -/
 def Orthogonal (e f : Effect E) : Prop := (e : E) + (f : E) ≤ 1
 
@@ -89,16 +57,6 @@ def addOfOrthogonal (e f : Effect E) (h : Orthogonal e f) : Effect E :=
 lemma coe_addOfOrthogonal (e f : Effect E) (h : Orthogonal e f) :
     (addOfOrthogonal e f h : E) = (e : E) + (f : E) := rfl
 
-/-- 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⟩ := exists_nsmul_one_le B
-  rw [← Nat.cast_smul_eq_nsmul ℝ] at hn
-  refine ⟨((n : ℝ) + 1)⁻¹, by positivity, smul_nonneg (by positivity) hB, ?_⟩
-  rw [inv_smul_le_iff_of_pos (by positivity)]
-  exact hn.trans (smul_le_smul_of_nonneg_right (by linarith) one_nonneg)
-
 end Effect
 
 end ProbabilisticTheory