From 47b4d339751c4a28521649d56760c8fbd6822d18 Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Sat, 15 Aug 2026 20:45:21 +0200 Subject: [PATCH 1/8] Add LadderSystem and HarmonicOscillator experimental modules to PhyslibAlpha (work-in-progress) --- PhyslibAlpha.lean | 8 + .../Mathematics/LadderSystem/Basic.lean | 316 +++++++++++++++ .../LadderSystem/Irreducibility.lean | 373 ++++++++++++++++++ .../LadderSystem/OccupationBasis.lean | 354 +++++++++++++++++ .../LadderSystem/SymmetricPower.lean | 59 +++ .../Mathematics/LadderSystem/Vacuum.lean | 275 +++++++++++++ .../HarmonicOscillator/Basic.lean | 278 +++++++++++++ .../HarmonicOscillator/LadderOperators.lean | 250 ++++++++++++ .../HarmonicOscillator/Vacuum.lean | 278 +++++++++++++ 9 files changed, 2191 insertions(+) create mode 100644 PhyslibAlpha/Mathematics/LadderSystem/Basic.lean create mode 100644 PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean create mode 100644 PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean create mode 100644 PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean create mode 100644 PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean create mode 100644 PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean create mode 100644 PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean create mode 100644 PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index 71341f2fe4..e222e54188 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -28,8 +28,16 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell public import PhyslibAlpha.QuantumMechanics.QuantumHarmonicOscillator +public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Basic +public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.LadderOperators +public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Vacuum public import PhyslibAlpha.QuantumMechanics.StinespringDilation public import PhyslibAlpha.Mathematics.PartialDerivativeTest +public import PhyslibAlpha.Mathematics.LadderSystem.Basic +public import PhyslibAlpha.Mathematics.LadderSystem.Vacuum +public import PhyslibAlpha.Mathematics.LadderSystem.Irreducibility +public import PhyslibAlpha.Mathematics.LadderSystem.OccupationBasis +public import PhyslibAlpha.Mathematics.LadderSystem.SymmetricPower public import PhyslibAlpha.ClassicalMechanics.CoupledSpringPotential public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.ChargeBalance public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.EffectivePotential diff --git a/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean b/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean new file mode 100644 index 0000000000..7cfd2cf75e --- /dev/null +++ b/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean @@ -0,0 +1,316 @@ +/- +Copyright (c) 2026 Tom Diem. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tom Diem +-/ +module + +public import Mathlib.Algebra.Lie.OfAssociative +public import Mathlib.Tactic.NoncommRing +public import Mathlib.LinearAlgebra.Matrix.StdBasis +public import Mathlib.Data.Matrix.Basis +public import Physlib.Mathematics.KroneckerDelta.Basic +/-! + +# Ladder systems + +## i. Overview + +A `LadderSystem K V d` packages `d` pairs of creation and annihilation endomorphisms of a +`K`-vector space `V` satisfying the canonical commutation relations. The definition abstracts the +algebraic structure shared by bosonic systems independently of a particular representation. The +bilinears `E i j := acᵢaⱼ` satisfy the `gl(d)` commutation relations and define a `gl(d)`-module +structure on `V` via `toGlHom`. + +- `Basic.lean` : this file -- the structure itself, the `gl(d)`-module structure it generates, and + the number operator. +- `Vacuum.lean` : a vacuum state, the creation-operator words built over it, and the excitation- + number sector they span, bundled as a `gl(d)` Lie submodule. +- `OccupationBasis.lean` : the occupation-number states form a basis of each fixed- + excitation-number sector, with an explicit dimension formula. +- `SymmetricPower.lean` : that sector is linearly isomorphic to `Sym^n(K^d)`. + +The harmonic-oscillator instance is defined in +`QuantumMechanics/HarmonicOscillator/LadderOperators.lean`. + +## ii. Key results + +Definitions: +- `LadderSystem.E` : the `gl(d)` bilinears `E i j := acᵢaⱼ`. +- `LadderSystem.toGlHom` : the `gl(d)`-representation on `V` generated by a ladder system. +- `LadderSystem.N` : the number operator for mode `i`, `Nᵢ ≔ Eᵢᵢ`. + +Theorems: +- `LadderSystem.lie_E` : `E` satisfies the defining relations of `gl(d)`. +- `LadderSystem.lie_N_a`, `LadderSystem.lie_N_ac` : `[Nᵢ, aⱼ] = -δᵢⱼaᵢ` and + `[Nᵢ, acⱼ] = δᵢⱼacᵢ`. +- `LadderSystem.lie_N_N` : the number operators commute among themselves, `[Nᵢ, Nⱼ] = 0`. +- `LadderSystem.lie_totalN_E` : the *total* number operator `∑ᵢNᵢ` is central in `gl(d)` -- + it commutes with every generator `E i j`, not just the diagonal ones. This is what makes an + isotropic Hamiltonian (a function of `∑ᵢNᵢ` alone) compatible with the full `gl(d)`-module + structure on `vacuumSpan`, not just individually with each `Nᵢ`. + +## iii. Table of contents + +- A. The `LadderSystem` structure +- B. The `gl(d)`-module structure +- C. The number operator + - C.1. Commutation relations + - C.2. The total number operator + +## iv. References + +-/ + +@[expose] public section + +open Module (Basis) +open KroneckerDelta + +/-! + +## A. The `LadderSystem` structure + +-/ + +attribute [local instance 100] LieRing.ofAssociativeRing + +variable {K : Type*} [Field K] + +section BracketLinearMaps + +variable (L : Type*) [LieRing L] [LieAlgebra K L] + +/-- Bracketing on the right by a fixed element, as a `K`-linear self-map. -/ +def bracketRight (y : L) : L →ₗ[K] L where + toFun x := ⁅x, y⁆ + map_add' a c := add_lie a c y + map_smul' c a := smul_lie c a y + +/-- Bracketing on the left by a fixed element, as a `K`-linear self-map. -/ +def bracketLeft (x : L) : L →ₗ[K] L where + toFun y := ⁅x, y⁆ + map_add' := lie_add x + map_smul' c a := lie_smul c x a + +end BracketLinearMaps + +variable {L L' : Type*} [LieRing L] [LieAlgebra K L] [LieRing L'] [LieAlgebra K L'] +variable {ι : Type*} + +/-- A `K`-linear map agreeing with the bracket on basis pairs agrees with the bracket +everywhere. -/ +theorem LinearMap.lie_apply_eq_of_lie_basis_eq (b : Basis ι K L) (f : L →ₗ[K] L') + (h : ∀ i j, f ⁅b i, b j⁆ = ⁅f (b i), f (b j)⁆) (x y : L) : + f ⁅x, y⁆ = ⁅f x, f y⁆ := by + have step1 : ∀ j : ι, + f.comp (bracketRight L (b j)) = (bracketRight L' (f (b j))).comp f := by + intro j + apply b.ext + intro i + change f ⁅b i, b j⁆ = ⁅f (b i), f (b j)⁆ + exact h i j + have step2 : f.comp (bracketLeft L x) = (bracketLeft L' (f x)).comp f := by + apply b.ext + intro j + have hx := DFunLike.congr_fun (step1 j) x + change f ⁅x, b j⁆ = ⁅f x, f (b j)⁆ at hx + exact hx + exact DFunLike.congr_fun step2 y + +/-- Same, from a spanning set rather than a basis (`LinearMap.ext_on` in place of `Basis.ext`) — +for generators that span but aren't worth packaging as an indexed basis. -/ +theorem LinearMap.lie_apply_eq_of_lie_span_eq {s : Set L} (hs : Submodule.span K s = ⊤) + (f : L →ₗ[K] L') (h : ∀ x ∈ s, ∀ y ∈ s, f ⁅x, y⁆ = ⁅f x, f y⁆) (x y : L) : + f ⁅x, y⁆ = ⁅f x, f y⁆ := by + have step1 : ∀ z ∈ s, + f.comp (bracketRight L z) = (bracketRight L' (f z)).comp f := by + intro z hz + apply LinearMap.ext_on hs + intro w hw + change f ⁅w, z⁆ = ⁅f w, f z⁆ + exact h w hw z hz + have step2 : f.comp (bracketLeft L x) = (bracketLeft L' (f x)).comp f := by + apply LinearMap.ext_on hs + intro z hz + have hx := DFunLike.congr_fun (step1 z hz) x + change f ⁅x, z⁆ = ⁅f x, f z⁆ at hx + exact hx + exact DFunLike.congr_fun step2 y + + +/-- A system of `d` independent ladder pairs on a `K`-vector space `V`: annihilation operators +`a i` and creation operators `ac i` (`i : Fin d`), satisfying the canonical commutation relations. +A physical system exhibits its own concrete operators as one instance of this (e.g. +`QuantumMechanics/HarmonicOscillator/LadderOperators.lean`'s `toLadderSystem`, via +`ContinuousLinearMap.toLinearMap`) and inherits every result in `LadderSystem/` for free. -/ +structure LadderSystem (K V : Type*) [Field K] [AddCommGroup V] [Module K V] (d : ℕ) where + /-- The `d` annihilation operators. -/ + a : Fin d → Module.End K V + /-- The `d` creation operators, `a⁺`. -/ + ac : Fin d → Module.End K V + /-- `[a i, ac j] = δᵢⱼ`. -/ + comm_a_ac : ∀ i j, (⁅a i, ac j⁆ : Module.End K V) = if i = j then 1 else 0 + /-- `[a i, a j] = 0`. -/ + comm_a_a : ∀ i j, (⁅a i, a j⁆ : Module.End K V) = 0 + /-- `[ac i, ac j] = 0`. -/ + comm_ac_ac : ∀ i j, (⁅ac i, ac j⁆ : Module.End K V) = 0 + +namespace LadderSystem + +variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] {d : ℕ} (L : LadderSystem K V d) + +lemma assoc_leibniz (x y z : Module.End K V) : + (⁅x, y * z⁆ : Module.End K V) = ⁅x, y⁆ * z + y * ⁅x, z⁆ := by + simp only [LieRing.of_associative_ring_bracket] + noncomm_ring + +lemma assoc_leibniz' (x y z : Module.End K V) : + (⁅x * y, z⁆ : Module.End K V) = x * ⁅y, z⁆ + ⁅x, z⁆ * y := by + simp only [LieRing.of_associative_ring_bracket] + noncomm_ring + +/-! + +## B. The `gl(d)`-module structure + +-/ + +/-- The `gl(d)` bilinears `E i j := ac i · a j`. -/ +def E (i j : Fin d) : Module.End K V := L.ac i * L.a j + +/-- `E` satisfies the defining relations of `gl(d)`: +`[E i j, E k l] = δⱼₖ E i l - δₗᵢ E k j`. -/ +theorem lie_E (i j k l : Fin d) : + (⁅L.E i j, L.E k l⁆ : Module.End K V) + = (δ[j,k] : K) • L.E i l - (δ[l,i] : K) • L.E k j := by + show (⁅L.ac i * L.a j, L.ac k * L.a l⁆ : Module.End K V) = _ + rw [assoc_leibniz' (L.ac i) (L.a j) (L.ac k * L.a l), assoc_leibniz (L.a j) (L.ac k) (L.a l), + assoc_leibniz (L.ac i) (L.ac k) (L.a l), L.comm_a_ac j k, L.comm_a_a j l, L.comm_ac_ac i k] + have hAl : (⁅L.ac i, L.a l⁆ : Module.End K V) = (-δ[l,i] : K) • (1 : Module.End K V) := by + rw [← lie_skew, L.comm_a_ac l i] + by_cases hli : l = i <;> simp [eq_zero_of_ne, hli] + rw [hAl] + by_cases hjk : j = k <;> by_cases hli : l = i <;> + simp [hjk, hli, E, eq_zero_of_ne, mul_zero, zero_mul, mul_one, one_mul, sub_eq_add_neg] + +/-- The matrix units satisfy the same relations, at the level of `gl(d)` itself. -/ +lemma lie_single (i j k l : Fin d) : + (⁅Matrix.single i j (1 : K), Matrix.single k l (1 : K)⁆ : Matrix (Fin d) (Fin d) K) + = (δ[j,k] : K) • Matrix.single i l 1 - (δ[l,i] : K) • Matrix.single k j 1 := by + rw [LieRing.of_associative_ring_bracket] + by_cases hjk : j = k <;> by_cases hli : l = i <;> + simp [Matrix.single_mul_single_same, Matrix.single_mul_single_of_ne, hjk, hli, + eq_zero_of_ne, sub_eq_add_neg] + +/-- The `K`-linear map sending matrix unit `Matrix.single i j 1` to `E i j`. -/ +noncomputable def toGlHomLinear (L : LadderSystem K V d) : + Matrix (Fin d) (Fin d) K →ₗ[K] Module.End K V := + (Matrix.stdBasis K (Fin d) (Fin d)).constr K (fun p => L.E p.1 p.2) + +@[simp] theorem toGlHomLinear_stdBasis (L : LadderSystem K V d) (i j : Fin d) : + L.toGlHomLinear (Matrix.stdBasis K (Fin d) (Fin d) (i, j)) = L.E i j := + Basis.constr_basis _ _ _ _ + +lemma toGlHomLinear_single (L : LadderSystem K V d) (i j : Fin d) : + L.toGlHomLinear (Matrix.single i j (1 : K)) = L.E i j := by + rw [← Matrix.stdBasis_eq_single, toGlHomLinear_stdBasis] + +/-- `toGlHomLinear` respects brackets. -/ +lemma toGlHomLinear_lie (L : LadderSystem K V d) (x y : Matrix (Fin d) (Fin d) K) : + L.toGlHomLinear ⁅x, y⁆ = ⁅L.toGlHomLinear x, L.toGlHomLinear y⁆ := by + apply LinearMap.lie_apply_eq_of_lie_basis_eq (Matrix.stdBasis K (Fin d) (Fin d)) L.toGlHomLinear + rintro ⟨i, j⟩ ⟨k, l⟩ + simp only [Matrix.stdBasis_eq_single, lie_single, map_sub, map_smul, + toGlHomLinear_single, L.lie_E i j k l] + +/-- The `gl(d)`-representation on `V` generated by a ladder system, bundled as a `LieHom`. -/ +noncomputable def toGlHom (L : LadderSystem K V d) : + Matrix (Fin d) (Fin d) K →ₗ⁅K⁆ Module.End K V := + { L.toGlHomLinear with map_lie' := L.toGlHomLinear_lie _ _ } + +/-- `V` as a `gl(d)`-module, the `LieRingModule` instance (not global -- depends on `L`; use via +`haveI := L.toLieRingModule`). -/ +@[reducible] noncomputable def toLieRingModule (L : LadderSystem K V d) : + LieRingModule (Matrix (Fin d) (Fin d) K) V := + LieRingModule.compLieHom V L.toGlHom + +/-- The companion `LieModule` instance. -/ +lemma toLieModule (L : LadderSystem K V d) : + @LieModule K (Matrix (Fin d) (Fin d) K) V _ _ _ _ _ L.toLieRingModule := + LieModule.compLieHom V L.toGlHom + +/-! + +## C. The number operator + +-/ + +/-- The number operator for mode `i`, `Nᵢ ≔ Eᵢᵢ = acᵢaᵢ`. -/ +def N (i : Fin d) : Module.End K V := L.E i i + +/-! + +### C.1. Commutation relations + +-/ + +/-- `[Nᵢ, aⱼ] = -δᵢⱼaᵢ`. -/ +lemma lie_N_a (i j : Fin d) : + (⁅L.N i, L.a j⁆ : Module.End K V) = (-δ[i,j] : K) • L.a i := by + show (⁅L.ac i * L.a i, L.a j⁆ : Module.End K V) = _ + rw [assoc_leibniz' (L.ac i) (L.a i) (L.a j), L.comm_a_a i j, mul_zero, zero_add] + have h : (⁅L.ac i, L.a j⁆ : Module.End K V) = (-δ[j,i] : K) • (1 : Module.End K V) := by + rw [← lie_skew, L.comm_a_ac j i] + by_cases hji : j = i <;> simp [eq_zero_of_ne, hji] + rw [h, smul_mul_assoc, one_mul, KroneckerDelta.symm i j] + +/-- `[Nᵢ, acⱼ] = δᵢⱼacᵢ`. -/ +lemma lie_N_ac (i j : Fin d) : + (⁅L.N i, L.ac j⁆ : Module.End K V) = (δ[i,j] : K) • L.ac i := by + show (⁅L.ac i * L.a i, L.ac j⁆ : Module.End K V) = _ + rw [assoc_leibniz' (L.ac i) (L.a i) (L.ac j), L.comm_a_ac i j, L.comm_ac_ac i j, zero_mul, + add_zero] + by_cases hij : i = j <;> simp [eq_zero_of_ne, hij] + +/-- `[Nᵢ, Nⱼ] = 0`: the number operators commute among themselves. -/ +lemma lie_N_N (i j : Fin d) : (⁅L.N i, L.N j⁆ : Module.End K V) = 0 := by + rcases eq_or_ne i j with rfl | hij + · exact lie_self _ + · show (⁅L.ac i * L.a i, L.N j⁆ : Module.End K V) = 0 + rw [assoc_leibniz' (L.ac i) (L.a i) (L.N j), + ← lie_skew (L.a i) (L.N j), lie_N_a, ← lie_skew (L.ac i) (L.N j), lie_N_ac] + simp [eq_zero_of_ne, Ne.symm hij] + +/-! + +### C.2. The total number operator + +-/ + +/-- The total number operator, `∑ᵢNᵢ` -- the total excitation count across every mode. -/ +def totalN (L : LadderSystem K V d) : Module.End K V := ∑ i, L.N i + +/-- The total number operator is central in `gl(d)`: it commutes with every generator +`E i j`, not just the diagonal ones (contrast `lie_N_N`, which only says the diagonal `Nᵢ` +commute *among themselves*). Consequently any operator built from `L.totalN` alone -- +in particular an *isotropic* Hamiltonian -- preserves `vacuumSpan` sector-by-sector for the same +reason `vacuumSpanLieSubmodule` does: it is `L.toGlHomLinear` applied to a central element of +`gl(d)` (the identity matrix), so it acts diagonally on the whole `gl(d)`-module structure. -/ +theorem lie_totalN_E (j k : Fin d) : (⁅L.totalN, L.E j k⁆ : Module.End K V) = 0 := by + rw [totalN, sum_lie] + have hstep : ∀ i, (⁅L.N i, L.E j k⁆ : Module.End K V) + = (δ[i,j] : K) • L.E i k - (δ[k,i] : K) • L.E j i := fun i => L.lie_E i i j k + simp_rw [hstep] + rw [Finset.sum_sub_distrib] + have hsum1 : (∑ i : Fin d, (δ[i,j] : K) • L.E i k) = L.E j k := by + rw [Finset.sum_eq_single j (fun i _ hij => by simp [eq_zero_of_ne hij]) + (fun h => absurd (Finset.mem_univ j) h)] + simp + have hsum2 : (∑ i : Fin d, (δ[k,i] : K) • L.E j i) = L.E j k := by + rw [Finset.sum_eq_single k (fun i _ hik => by simp [eq_zero_of_ne hik.symm]) + (fun h => absurd (Finset.mem_univ k) h)] + simp + rw [hsum1, hsum2, sub_self] + +end LadderSystem diff --git a/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean b/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean new file mode 100644 index 0000000000..c863442692 --- /dev/null +++ b/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean @@ -0,0 +1,373 @@ +/- +Copyright (c) 2026 Tom Diem. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tom Diem +-/ +module + +public import PhyslibAlpha.Mathematics.LadderSystem.OccupationBasis +/-! + +# Irreducibility of the excitation-number sector + +## i. Overview + +`LadderSystem.vacuumSpan L Ω n` is `gl(d)`-irreducible: the only submodules of `vacuumSpan L Ω n` +invariant under every `E i j` are `⊥` and `vacuumSpan L Ω n` itself. Completeness in an ambient +Hilbert space is a separate analytic question. The proof uses linear algebra over a field of +characteristic zero. + +## ii. Key results + +- `LadderSystem.vacuumSpan_eq_of_ne_bot` : a nonzero `E i j`-invariant submodule of + `vacuumSpan L Ω n` is all of `vacuumSpan L Ω n`. + +## iii. Table of contents + +- A. Moving a quantum between modes +- B. Extracting a single basis vector from an invariant submodule +- C. Connectivity: one basis vector reaches every other +- D. Irreducibility + +## iv. References + +-/ + +@[expose] public section + +attribute [local instance 100] LieRing.ofAssociativeRing + +namespace LadderSystem + +variable {K V : Type*} [Field K] [CharZero K] [AddCommGroup V] [Module K V] {d : ℕ} + (L : LadderSystem K V d) + +/-! + +## A. Moving a quantum between modes + +-/ + +/-- `α` with one quantum moved from color `j` to color `i`. Only meaningful for `i ≠ j`; the +degenerate `i = j` case is handled separately by `N_word`. -/ +def moveOneTo (α : Fin d → ℕ) (i j : Fin d) : Fin d → ℕ := + fun c => if c = i then α i + 1 else if c = j then α j - 1 else α c + +lemma countWord_moveOneTo_perm {i j : Fin d} (hij : i ≠ j) {α : Fin d → ℕ} : + List.Perm (i :: (countWord d α).erase j) (countWord d (moveOneTo α i j)) := by + rw [List.perm_iff_count] + intro c + rw [count_countWord] + by_cases hci : c = i + · subst hci + rw [List.count_cons_self, List.count_erase_of_ne hij, count_countWord] + simp [moveOneTo] + · rw [List.count_cons_of_ne (Ne.symm hci)] + by_cases hcj : c = j + · subst hcj + rw [List.count_erase_self, count_countWord] + simp [moveOneTo, hci] + · rw [List.count_erase_of_ne hcj, count_countWord] + simp [moveOneTo, hci, hcj] + +variable {L} + +omit [CharZero K] in +/-- The transfer formula: `E i j` moves one quantum from color `j` to color `i`, scaled by +`j`'s occupation number. -/ +lemma E_word_countWord {Ω : V} (P : L.HasVacuum Ω) {i j : Fin d} (hij : i ≠ j) + {α : Fin d → ℕ} : + L.E i j (L.word (countWord d α) Ω) = + (α j : K) • L.word (countWord d (moveOneTo α i j)) Ω := by + rw [Nat.cast_smul_eq_nsmul K, E_word L P.ann i j (countWord d α), count_countWord, + word_perm L (countWord_moveOneTo_perm hij)] + +/-! + +## B. Extracting a single basis vector from an invariant submodule + +-/ + +omit [CharZero K] in +/-- A submodule invariant under an endomorphism `M` is invariant under any polynomial in `M`. -/ +lemma mapsTo_aeval {W : Submodule K V} {M : Module.End K V} (hW : ∀ w ∈ W, M w ∈ W) + (p : Polynomial K) : ∀ w ∈ W, (Polynomial.aeval M p) w ∈ W := by + refine p.induction_on ?_ ?_ ?_ + · intro a w hw + rw [Polynomial.aeval_C, Module.algebraMap_end_apply] + exact W.smul_mem a hw + · intro p q hp hq w hw + rw [map_add, LinearMap.add_apply] + exact W.add_mem (hp w hw) (hq w hw) + · intro k a hka w hw + have heq : Polynomial.C a * Polynomial.X ^ (k + 1) = + (Polynomial.C a * Polynomial.X ^ k) * Polynomial.X := by ring + rw [heq, map_mul, Module.End.mul_apply, Polynomial.aeval_X] + exact hka (M w) (hW w hw) + +/-- A nonzero `E i j`-invariant submodule of `vacuumSpan L Ω n` contains an occupation-number +basis vector. A Lagrange-interpolation polynomial in the diagonal separator +`∑ᵢ(n+1)^i • Nᵢ` projects a nonzero element onto one of its basis components. -/ +lemma exists_word_countWord_mem_of_ne_bot {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) + {W : Submodule K V} (hWle : W ≤ vacuumSpan L Ω n) + (hWE : ∀ i j, ∀ w ∈ W, L.E i j w ∈ W) (hWbot : W ≠ ⊥) : + ∃ α : CountFun d n, L.word (countWord d α.1) Ω ∈ W := by + classical + set M : Module.End K V := ∑ i : Fin d, ((n + 1 : K)) ^ (i : ℕ) • L.N i with hM + have hWM : ∀ w ∈ W, M w ∈ W := by + intro w hw + rw [hM, LinearMap.sum_apply] + refine Submodule.sum_mem W fun i _ => ?_ + rw [LinearMap.smul_apply] + exact W.smul_mem _ (hWE i i w hw) + obtain ⟨w, hwW, hw0⟩ := (Submodule.ne_bot_iff W).mp hWbot + have hwspan : w ∈ vacuumSpan L Ω n := hWle hwW + set c := (vacuumBasis L P n).repr ⟨w, hwspan⟩ with hc + have hc0 : c ≠ 0 := by + intro h + apply hw0 + have h' : (⟨w, hwspan⟩ : L.vacuumSpan Ω n) = 0 := by + rw [hc] at h + exact (vacuumBasis L P n).repr.map_eq_zero_iff.mp h + simpa using congrArg Subtype.val h' + obtain ⟨α₀, hα₀⟩ := Finsupp.support_nonempty_iff.mpr hc0 + set p : Polynomial K := + ∏ β ∈ (Finset.univ.erase α₀ : Finset (CountFun d n)), + (Polynomial.X - Polynomial.C (countEncode n β.1 : K)) with hp + have heval_ne : ∀ β : CountFun d n, β ≠ α₀ → p.eval (countEncode n β.1 : K) = 0 := by + intro β hβ + rw [hp, Polynomial.eval_prod] + refine Finset.prod_eq_zero (Finset.mem_erase.mpr ⟨hβ, Finset.mem_univ β⟩) ?_ + simp + have heval_eq : p.eval (countEncode n α₀.1 : K) ≠ 0 := by + rw [hp, Polynomial.eval_prod] + refine Finset.prod_ne_zero_iff.mpr fun β hβ => ?_ + have hβne : β ≠ α₀ := (Finset.mem_erase.mp hβ).1 + simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C, sub_ne_zero] + intro heq + have heqn : countEncode n α₀.1 = countEncode n β.1 := by exact_mod_cast heq + exact hβne (Subtype.ext (countEncode_injOn α₀.2 β.2 heqn)).symm + have haeval : ∀ β : CountFun d n, + (Polynomial.aeval M p) (L.word (countWord d β.1) Ω) = + p.eval (countEncode n β.1 : K) • L.word (countWord d β.1) Ω := + fun β => Module.End.aeval_apply_of_hasEigenvector (hasEigenvector_word_countWord L P n β) + have hwe : w = ∑ β : CountFun d n, c β • L.word (countWord d β.1) Ω := by + have hsum := (vacuumBasis L P n).sum_repr (⟨w, hwspan⟩ : L.vacuumSpan Ω n) + rw [← hc] at hsum + have hval : (∑ β : CountFun d n, c β • (vacuumBasis L P n β : V)) = w := by + simpa using congrArg Subtype.val hsum + rw [← hval] + refine Finset.sum_congr rfl fun β _ => ?_ + rw [vacuumBasis_apply] + have hmem : (Polynomial.aeval M p) w ∈ W := mapsTo_aeval hWM p w hwW + have hcompute : (Polynomial.aeval M p) w = + (c α₀ * p.eval (countEncode n α₀.1 : K)) • L.word (countWord d α₀.1) Ω := by + rw [hwe, map_sum] + rw [Finset.sum_eq_single α₀] + · rw [map_smul, haeval, smul_smul] + · intro β _ hβne + rw [map_smul, haeval, heval_ne β hβne, zero_smul, smul_zero] + · intro h + exact absurd (Finset.mem_univ α₀) h + rw [hcompute] at hmem + refine ⟨α₀, ?_⟩ + have hne : c α₀ * p.eval (countEncode n α₀.1 : K) ≠ 0 := + mul_ne_zero (Finsupp.mem_support_iff.mp hα₀) heval_eq + have := W.smul_mem (c α₀ * p.eval (countEncode n α₀.1 : K))⁻¹ hmem + rwa [smul_smul, inv_mul_cancel₀ hne, one_smul] at this + +/-! + +## C. Connectivity: one basis vector reaches every other + +-/ + +omit [CharZero K] in +/-- The total occupation number matches the length of the canonical word representing it. -/ +lemma sum_eq_length_countWord (α : Fin d → ℕ) : (∑ c, α c) = (countWord d α).length := by + rw [← sum_count_eq_length (countWord d α)] + exact Finset.sum_congr rfl fun c _ => (count_countWord α c).symm + +omit [CharZero K] in +/-- Moving one quantum between two modes preserves the total occupation number. -/ +lemma sum_moveOneTo {i j : Fin d} (hij : i ≠ j) {α : Fin d → ℕ} (hj : α j ≠ 0) : + (∑ c, moveOneTo α i j c) = ∑ c, α c := by + have hcj : (countWord d α).count j ≠ 0 := by rw [count_countWord]; exact hj + have hmem : j ∈ countWord d α := List.count_pos_iff.mp (Nat.pos_of_ne_zero hcj) + rw [sum_eq_length_countWord, sum_eq_length_countWord, + ← (countWord_moveOneTo_perm hij).length_eq, List.length_cons, List.length_erase_of_mem hmem] + have := List.length_pos_of_mem hmem + omega + +omit [CharZero K] in +/-- `moveOneTo` at the color it moves quanta *into* just increments that color's count. -/ +lemma moveOneTo_self (α : Fin d → ℕ) (i j : Fin d) : moveOneTo α i j i = α i + 1 := by + show (if i = i then α i + 1 else if i = j then α j - 1 else α i) = α i + 1 + rw [if_pos rfl] + +omit [CharZero K] in +/-- Moving a quantum from `j` to `i` and then immediately back from `i` to `j` is the identity. -/ +lemma moveOneTo_moveOneTo {i j : Fin d} (hij : i ≠ j) {α : Fin d → ℕ} (hj : α j ≠ 0) : + moveOneTo (moveOneTo α i j) j i = α := by + have hβj : moveOneTo α i j j = α j - 1 := by + show (if j = i then α i + 1 else if j = j then α j - 1 else α j) = α j - 1 + rw [if_neg (Ne.symm hij), if_pos rfl] + have hβi : moveOneTo α i j i = α i + 1 := moveOneTo_self α i j + funext c + show (if c = j then moveOneTo α i j j + 1 else if c = i then moveOneTo α i j i - 1 + else moveOneTo α i j c) = α c + rcases eq_or_ne c j with rfl | hcj + · rw [if_pos rfl, hβj] + omega + · rw [if_neg hcj] + rcases eq_or_ne c i with rfl | hci + · rw [if_pos rfl, hβi] + omega + · rw [if_neg hci] + show (if c = i then α i + 1 else if c = j then α j - 1 else α c) = α c + rw [if_neg hci, if_neg hcj] + +/-- The atomic move: if `W` is `E i j`-invariant and contains the word for `β`, and mode `k` +is occupied, `W` also contains the word obtained by moving one quantum from `k` to any other +mode `l`. -/ +lemma word_countWord_moveOneTo_mem {Ω : V} (P : L.HasVacuum Ω) {W : Submodule K V} + (hWE : ∀ i j, ∀ w ∈ W, L.E i j w ∈ W) {β : Fin d → ℕ} + (hmem : L.word (countWord d β) Ω ∈ W) {l k : Fin d} (hkl : l ≠ k) (hk : β k ≠ 0) : + L.word (countWord d (moveOneTo β l k)) Ω ∈ W := by + have hE : L.E l k (L.word (countWord d β) Ω) ∈ W := hWE l k _ hmem + rw [E_word_countWord P hkl] at hE + have hne : (β k : K) ≠ 0 := Nat.cast_ne_zero.mpr hk + have hsm := W.smul_mem (β k : K)⁻¹ hE + rwa [smul_smul, inv_mul_cancel₀ hne, one_smul] at hsm + +/-- Every occupation-number word reaches the mode-`0` hub word, given `W` +is `E i j`-invariant and contains it. Proved by strong induction on the mass sitting outside +mode `0`. -/ +lemma word_countWord_hub_mem_of_mem {hd : 0 < d} {Ω : V} (P : L.HasVacuum Ω) + {W : Submodule K V} (hWE : ∀ i j, ∀ w ∈ W, L.E i j w ∈ W) : + ∀ m : ℕ, ∀ α : Fin d → ℕ, (∑ c, α c) - α (⟨0, hd⟩ : Fin d) = m → + L.word (countWord d α) Ω ∈ W → + L.word (countWord d (fun c => if c = (⟨0, hd⟩ : Fin d) then (∑ c, α c) else 0)) Ω ∈ W := by + intro m + induction m using Nat.strong_induction_on with + | _ m ih => + intro α hdeficit hmem + set hub0 := (⟨0, hd⟩ : Fin d) + have hle0 : α hub0 ≤ ∑ c, α c := Finset.single_le_sum (fun _ _ => Nat.zero_le _) + (Finset.mem_univ hub0) + rcases eq_or_ne m 0 with rfl | hm0 + · have hα0 : α hub0 = ∑ c, α c := by omega + have hα : α = (fun c => if c = hub0 then (∑ c, α c) else 0) := by + have hsplit : α hub0 + ∑ c ∈ Finset.univ.erase hub0, α c = ∑ c, α c := + Finset.add_sum_erase _ α (Finset.mem_univ hub0) + funext c + by_cases hc : c = hub0 + · subst hc; rw [if_pos rfl]; exact hα0 + · rw [if_neg hc] + have hle : α c ≤ ∑ c' ∈ Finset.univ.erase hub0, α c' := + Finset.single_le_sum (fun _ _ => Nat.zero_le _) + (Finset.mem_erase.mpr ⟨hc, Finset.mem_univ c⟩) + omega + rwa [← hα] + · obtain ⟨j, hjne, hjpos⟩ : ∃ j : Fin d, j ≠ hub0 ∧ α j ≠ 0 := by + by_contra hcon + push Not at hcon + have hsplit : (∑ c, α c) = α hub0 := + Finset.sum_eq_single hub0 (fun c _ hc => hcon c hc) + (fun h => absurd (Finset.mem_univ hub0) h) + rw [hsplit, Nat.sub_self] at hdeficit + exact hm0 hdeficit.symm + have hstep := word_countWord_moveOneTo_mem P hWE hmem (Ne.symm hjne) hjpos + have hsum' := sum_moveOneTo (Ne.symm hjne) hjpos (α := α) + have hval : moveOneTo α hub0 j hub0 = α hub0 + 1 := moveOneTo_self α hub0 j + have hdeficit' : (∑ c, moveOneTo α hub0 j c) - (moveOneTo α hub0 j) hub0 = m - 1 := by + rw [hsum', hval] + omega + have := ih (m - 1) (by omega) (moveOneTo α hub0 j) hdeficit' hstep + rwa [hsum'] at this + +/-- The hub word reaches every occupation-number word, given `W` is `E i j`-invariant and +contains it. Proved by strong induction on the mass sitting outside mode `0` in the target. -/ +lemma word_countWord_mem_of_hub_mem {hd : 0 < d} {Ω : V} (P : L.HasVacuum Ω) + {W : Submodule K V} (hWE : ∀ i j, ∀ w ∈ W, L.E i j w ∈ W) : + ∀ m : ℕ, ∀ α : Fin d → ℕ, (∑ c, α c) - α (⟨0, hd⟩ : Fin d) = m → + L.word (countWord d (fun c => if c = (⟨0, hd⟩ : Fin d) then (∑ c, α c) else 0)) Ω ∈ W → + L.word (countWord d α) Ω ∈ W := by + intro m + induction m using Nat.strong_induction_on with + | _ m ih => + intro α hdeficit hmem + set hub0 := (⟨0, hd⟩ : Fin d) + have hle0 : α hub0 ≤ ∑ c, α c := Finset.single_le_sum (fun _ _ => Nat.zero_le _) + (Finset.mem_univ hub0) + rcases eq_or_ne m 0 with rfl | hm0 + · have hα0 : α hub0 = ∑ c, α c := by omega + have hα : α = (fun c => if c = hub0 then (∑ c, α c) else 0) := by + have hsplit : α hub0 + ∑ c ∈ Finset.univ.erase hub0, α c = ∑ c, α c := + Finset.add_sum_erase _ α (Finset.mem_univ hub0) + funext c + by_cases hc : c = hub0 + · subst hc; rw [if_pos rfl]; exact hα0 + · rw [if_neg hc] + have hle : α c ≤ ∑ c' ∈ Finset.univ.erase hub0, α c' := + Finset.single_le_sum (fun _ _ => Nat.zero_le _) + (Finset.mem_erase.mpr ⟨hc, Finset.mem_univ c⟩) + omega + rwa [hα] + · obtain ⟨j, hjne, hjpos⟩ : ∃ j : Fin d, j ≠ hub0 ∧ α j ≠ 0 := by + by_contra hcon + push Not at hcon + have hsplit : (∑ c, α c) = α hub0 := + Finset.sum_eq_single hub0 (fun c _ hc => hcon c hc) + (fun h => absurd (Finset.mem_univ hub0) h) + rw [hsplit, Nat.sub_self] at hdeficit + exact hm0 hdeficit.symm + set α' : Fin d → ℕ := moveOneTo α hub0 j with hα' + have hsum' : (∑ c, α' c) = ∑ c, α c := sum_moveOneTo (Ne.symm hjne) hjpos + have hval' : α' hub0 = α hub0 + 1 := by rw [hα']; exact moveOneTo_self α hub0 j + have hα'0 : α' hub0 ≠ 0 := by omega + have hdeficit' : (∑ c, α' c) - α' hub0 = m - 1 := by rw [hsum', hval']; omega + have hhubeq : (fun c => if c = hub0 then (∑ c, α' c) else 0) = + (fun c => if c = hub0 then (∑ c, α c) else 0) := by rw [hsum'] + have hmem' : L.word (countWord d α') Ω ∈ W := by + refine ih (m - 1) (by omega) α' hdeficit' ?_ + rwa [hhubeq] + have hstep := word_countWord_moveOneTo_mem P hWE hmem' hjne hα'0 + have hrev : moveOneTo α' j hub0 = α := by + rw [hα'] + exact moveOneTo_moveOneTo (Ne.symm hjne) hjpos + rwa [hrev] at hstep + +/-- Connectivity: any two occupation-number words of the same total excitation number reach +each other, given `W` is `E i j`-invariant and contains one of them. -/ +lemma word_countWord_mem_of_mem {hd : 0 < d} {Ω : V} (P : L.HasVacuum Ω) + {W : Submodule K V} (hWE : ∀ i j, ∀ w ∈ W, L.E i j w ∈ W) {α α' : Fin d → ℕ} + (hsum : (∑ c, α c) = ∑ c, α' c) (hmem : L.word (countWord d α) Ω ∈ W) : + L.word (countWord d α') Ω ∈ W := by + have h1 := word_countWord_hub_mem_of_mem (hd := hd) P hWE _ α rfl hmem + have h2 := word_countWord_mem_of_hub_mem (hd := hd) P hWE _ α' rfl + rw [hsum] at h1 + exact h2 h1 + +/-! + +## D. Irreducibility + +-/ + +/-- `vacuumSpan L Ω n` is `gl(d)`-irreducible. The only submodules of `vacuumSpan L Ω n` +invariant under every `E i j` are `⊥` and `vacuumSpan L Ω n` itself. -/ +theorem vacuumSpan_eq_of_ne_bot {hd : 0 < d} {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) + {W : Submodule K V} (hWle : W ≤ vacuumSpan L Ω n) + (hWE : ∀ i j, ∀ w ∈ W, L.E i j w ∈ W) (hWbot : W ≠ ⊥) : + W = vacuumSpan L Ω n := by + obtain ⟨α₀, hα₀⟩ := exists_word_countWord_mem_of_ne_bot P n hWle hWE hWbot + refine le_antisymm hWle ?_ + rw [← span_word_countFun_eq_vacuumSpan L Ω n, Submodule.span_le] + rintro _ ⟨α, rfl⟩ + refine word_countWord_mem_of_mem (hd := hd) P hWE ?_ hα₀ + have h1 : (∑ c, α₀.1 c) = n := α₀.2 + have h2 : (∑ c, α.1 c) = n := α.2 + rw [h1, h2] + +end LadderSystem diff --git a/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean b/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean new file mode 100644 index 0000000000..ce92e90271 --- /dev/null +++ b/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean @@ -0,0 +1,354 @@ +/- +Copyright (c) 2026 Tom Diem. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tom Diem +-/ +module + +public import PhyslibAlpha.Mathematics.LadderSystem.Vacuum +public import Mathlib.Data.Sym.Card +public import Mathlib.Data.Finsupp.Multiset +public import Mathlib.LinearAlgebra.Basis.Basic +public import Mathlib.LinearAlgebra.Eigenspace.Zero +public import Mathlib.LinearAlgebra.FiniteDimensional.Defs +public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.List +/-! + +# The occupation-number basis + +## i. Overview + +The occupation-number states `word (countWord d α) Ω`, indexed by degree-`n` count functions +`α : CountFun d n`, form a basis of `vacuumSpan L Ω n`. For linear independence, each state is +viewed as a nonzero eigenvector of the diagonal operator +`M := ∑ᵢ (n+1)^i • Nᵢ`, at the pairwise-distinct eigenvalue `countEncode n α` (a positional +encoding of `α`), so Mathlib's general "eigenvectors at distinct eigenvalues are independent" fact +applies. It follows that `vacuumSpan` is finite-dimensional and has dimension +`(d+n-1).choose n`, the degeneracy of the `n`-th level of a `d`-dimensional bosonic oscillator. + +## ii. Key results + +Definitions: +- `CountFun d n` : a degree-`n` count function on `d` colors. +- `LadderSystem.vacuumBasis` : the occupation-number basis of `vacuumSpan L Ω n`. + +Theorems: +- `LadderSystem.linearIndependent_word_countFun` : the occupation-number states are linearly + independent. +- `LadderSystem.finrank_vacuumSpan_eq_choose` : `vacuumSpan L Ω n` has dimension + `(d+n-1).choose n`. + +## iii. Table of contents + +- A. Count functions +- B. Exact annihilation +- C. The occupation-number basis + - C.1. A positional encoding of count functions + - C.2. Linear independence + - C.3. The basis and its dimension + +## iv. References + +-/ + +@[expose] public section + +open Module (Basis) + +/-! + +## A. Count functions + +-/ + +/-- A degree-`n` count function on `d` colors. -/ +abbrev CountFun (d n : ℕ) := {α : Fin d → ℕ // ∑ c, α c = n} + +/-- Degree-`n` count functions on `d` colors biject with `Sym (Fin d) n`. -/ +noncomputable def countFunEquivSym (d n : ℕ) : CountFun d n ≃ Sym (Fin d) n := + (Sym.equivNatSumOfFintype (Fin d) n).symm + +noncomputable instance instFintypeCountFun {d n : ℕ} : Fintype (CountFun d n) := + Fintype.ofEquiv (Sym (Fin d) n) (Sym.equivNatSumOfFintype (Fin d) n) + +/-- There are exactly `(d + n - 1).choose n` degree-`n` count functions on `d` colors. -/ +lemma card_countFun (d n : ℕ) : Fintype.card (CountFun d n) = (d + n - 1).choose n := by + rw [Fintype.card_congr (countFunEquivSym d n), Sym.card_sym_eq_choose, Fintype.card_fin] + +attribute [local instance 100] LieRing.ofAssociativeRing + +namespace LadderSystem + +variable {K V : Type*} [Field K] [CharZero K] [AddCommGroup V] [Module K V] {d : ℕ} + (L : LadderSystem K V d) + +/-! + +## B. Exact annihilation + +-/ + +omit [CharZero K] in +/-- Annihilation and creation operators of different colors commute at any power. -/ +lemma pow_a_comm_ac {i c : Fin d} (hic : i ≠ c) (k : ℕ) (y : V) : + ((L.a i) ^ k) (L.ac c y) = L.ac c (((L.a i) ^ k) y) := by + have h := L.comm_a_ac i c + rw [if_neg hic, LieRing.of_associative_ring_bracket, sub_eq_zero] at h + have hpow : (L.a i) ^ k * L.ac c = L.ac c * (L.a i) ^ k := Commute.pow_left h k + have happly := congrArg (fun f : Module.End K V => f y) hpow + simpa [Module.End.mul_apply] using happly + +omit [CharZero K] in +/-- Exact annihilation: applying `a i` exactly `count i` times removes every `i`, scaled by the +factorial. -/ +lemma word_peel_eq_count (L : LadderSystem K V d) (i : Fin d) {x : V} (hx : L.a i x = 0) : + ∀ v : List (Fin d), + ((L.a i) ^ (v.count i)) (L.word v x) = (v.count i).factorial • L.word (v.filter (· != i)) x + | [] => by simp [word] + | c :: v' => by + by_cases hic : i = c + · subst hic + have hpeel := word_peel L i hx (i :: v') + rw [List.count_cons_self, List.erase_cons_head] at hpeel + rw [List.count_cons_self, List.filter_cons_of_neg (by simp), pow_succ, + Module.End.mul_apply, hpeel, map_nsmul, word_peel_eq_count L i hx v', + Nat.factorial_succ, mul_smul] + · rw [List.count_cons_of_ne (Ne.symm hic), word_cons, + pow_a_comm_ac L hic, word_peel_eq_count L i hx v', map_nsmul, ← word_cons, + List.filter_cons_of_pos (by simpa using Ne.symm hic)] + +/-- The joint annihilation monomial for a list of colors `cs` and exponents `α`: +`∏_{c ∈ cs} (a c)^{α c}`. -/ +def annMono (cs : List (Fin d)) (α : Fin d → ℕ) : Module.End K V := + (cs.map (fun c => (L.a c) ^ (α c))).prod + +omit [CharZero K] in +@[simp] theorem annMono_nil (α : Fin d → ℕ) : L.annMono [] α = 1 := rfl + +omit [CharZero K] in +lemma annMono_cons (c : Fin d) (cs : List (Fin d)) (α : Fin d → ℕ) : + L.annMono (c :: cs) α = (L.a c) ^ (α c) * L.annMono cs α := rfl + +omit [CharZero K] in +/-- Exact annihilation of every color in the list produces the product of factorials. -/ +lemma annMono_eq_count (L : LadderSystem K V d) {x : V} (hx : ∀ i, L.a i x = 0) : + ∀ (cs : List (Fin d)), cs.Nodup → ∀ (α : Fin d → ℕ) (v : List (Fin d)), + (∀ c ∈ cs, v.count c = α c) → + (L.annMono cs α) (L.word v x) + = ((cs.map (fun c => (α c).factorial)).prod) • + L.word (v.filter (fun y => !cs.contains y)) x + | [], _, _, _, _ => by simp + | c :: cs', hnodup, α, v, hmatch => by + obtain ⟨hcnotmem, hnodup'⟩ := List.nodup_cons.mp hnodup + have hmatch' : ∀ e ∈ cs', v.count e = α e := fun e he => hmatch e (List.mem_cons_of_mem c he) + have hcm : v.count c = α c := hmatch c List.mem_cons_self + rw [annMono_cons, Module.End.mul_apply, + annMono_eq_count L hx cs' hnodup' α v hmatch', map_nsmul] + have hcount : (v.filter (fun y => !cs'.contains y)).count c = v.count c := + List.count_filter (by simpa using hcnotmem) + have hpeel : ((L.a c) ^ (α c)) (L.word (v.filter (fun y => !cs'.contains y)) x) + = (α c).factorial • + L.word ((v.filter (fun y => !cs'.contains y)).filter (· != c)) x := by + have h := word_peel_eq_count L c (hx c) (v.filter (fun y => !cs'.contains y)) + rwa [hcount, hcm] at h + have hY : L.word ((v.filter (fun y => !cs'.contains y)).filter (· != c)) x + = L.word (v.filter (fun y => !(c :: cs').contains y)) x := by + congr 1 + rw [List.filter_filter] + congr 1 + funext y + by_cases hy : y = c + · subst hy; simp + · simp [hy] + rw [hpeel, List.map_cons, List.prod_cons, hY, ← mul_smul, mul_comm] + +end LadderSystem + +/-- `countWord α` contains only colors from `List.finRange d`, i.e. everything. -/ +lemma countWord_filter_finRange {d : ℕ} (α : Fin d → ℕ) : + (LadderSystem.countWord d α).filter (fun y => !(List.finRange d).contains y) = [] := + List.filter_eq_nil_iff.mpr fun y _ => by simp [List.mem_finRange] + +/-! + +## C. The occupation-number basis + +-/ + +/-! + +### C.1. A positional encoding of count functions + +-/ + +/-- A base-`b` positional encoding is injective on tuples with digits `< b`. -/ +lemma encode_injOn_aux : ∀ (d b : ℕ), 0 < b → ∀ γ γ' : Fin d → ℕ, + (∀ c, γ c < b) → (∀ c, γ' c < b) → + (∑ i : Fin d, γ i * b ^ (i : ℕ)) = (∑ i : Fin d, γ' i * b ^ (i : ℕ)) → γ = γ' := by + intro d + induction d with + | zero => intro b _ γ γ' _ _ _; exact funext fun i => i.elim0 + | succ d ih => + intro b hb γ γ' hγ hγ' heq + have hfactor : ∀ f : Fin d → ℕ, + (∑ i : Fin d, f i * b ^ (i.succ : ℕ)) = b * ∑ i : Fin d, f i * b ^ (i : ℕ) := by + intro f + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [Fin.val_succ, pow_succ'] + ring + rw [Fin.sum_univ_succ, Fin.sum_univ_succ] at heq + simp only [Fin.val_zero, pow_zero, mul_one] at heq + rw [hfactor (fun i => γ i.succ), hfactor (fun i => γ' i.succ)] at heq + have h0 : γ 0 = γ' 0 := by + have hmod := congrArg (· % b) heq + simp only [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt (hγ 0), Nat.mod_eq_of_lt (hγ' 0)] + at hmod + exact hmod + have hrest : (∑ i : Fin d, γ i.succ * b ^ (i : ℕ)) = ∑ i : Fin d, γ' i.succ * b ^ (i : ℕ) := by + have heq' := heq + rw [h0] at heq' + exact Nat.eq_of_mul_eq_mul_left hb (Nat.add_left_cancel heq') + have htail := ih b hb (fun i => γ i.succ) (fun i => γ' i.succ) + (fun i => hγ i.succ) (fun i => hγ' i.succ) hrest + funext i + exact Fin.cases h0 (fun j => congrFun htail j) i + +/-- The base-`(n+1)` positional encoding of a degree-`n` count function; injective on such +functions. -/ +def countEncode (n : ℕ) {d : ℕ} (γ : Fin d → ℕ) : ℕ := ∑ i : Fin d, γ i * (n + 1) ^ (i : ℕ) + +lemma countEncode_injOn {d n : ℕ} {γ γ' : Fin d → ℕ} + (hγ : ∑ c, γ c = n) (hγ' : ∑ c, γ' c = n) (heq : countEncode n γ = countEncode n γ') : + γ = γ' := by + refine encode_injOn_aux d (n + 1) (Nat.succ_pos n) γ γ' (fun c => ?_) (fun c => ?_) heq + · exact Nat.lt_succ_of_le (hγ ▸ Finset.single_le_sum (fun c _ => Nat.zero_le _) + (Finset.mem_univ c)) + · exact Nat.lt_succ_of_le (hγ' ▸ Finset.single_le_sum (fun c _ => Nat.zero_le _) + (Finset.mem_univ c)) + +namespace LadderSystem + +variable {K V : Type*} [Field K] [CharZero K] [AddCommGroup V] [Module K V] {d : ℕ} + (L : LadderSystem K V d) + +/-! + +### C.2. Linear independence + +-/ + +/-- Every occupation-number state is nonzero: peeling every color's annihilation operator down to +the vacuum leaves a nonzero factorial multiple of `Ω`. -/ +lemma word_countWord_ne_zero {Ω : V} (hΩ : L.HasVacuum Ω) (α : Fin d → ℕ) : + L.word (countWord d α) Ω ≠ 0 := by + intro hz + have h := L.annMono_eq_count hΩ.ann (List.finRange d) (List.nodup_finRange d) α + (countWord d α) (fun c _ => count_countWord α c) + rw [countWord_filter_finRange, hz, map_zero] at h + have hfact_pos : (0 : ℕ) < ((List.finRange d).map (fun c => (α c).factorial)).prod := + List.prod_pos (by + intro a ha + obtain ⟨c, -, rfl⟩ := List.mem_map.mp ha + exact Nat.factorial_pos _) + have hfact_ne : (((List.finRange d).map (fun c => (α c).factorial)).prod : K) ≠ 0 := + Nat.cast_ne_zero.mpr hfact_pos.ne' + have hΩ' : L.word ([] : List (Fin d)) Ω = Ω := by simp [word] + rw [hΩ', ← Nat.cast_smul_eq_nsmul K] at h + rcases smul_eq_zero.mp h.symm with h1 | h2 + · exact hfact_ne h1 + · exact hΩ.ne_zero h2 + +/-- The occupation-number states are the eigenvectors, at pairwise-distinct eigenvalues, of the +single diagonal operator `M := ∑ᵢ (n+1)^i • Nᵢ`. -/ +lemma hasEigenvector_word_countWord {Ω : V} (hΩ : L.HasVacuum Ω) (n : ℕ) (α : CountFun d n) : + Module.End.HasEigenvector (∑ i : Fin d, ((n + 1 : K)) ^ (i : ℕ) • L.N i) + (countEncode n α.1 : K) (L.word (countWord d α.1) Ω) := by + refine ⟨?_, L.word_countWord_ne_zero hΩ α.1⟩ + rw [Module.End.mem_eigenspace_iff] + have hterm : ∀ i : Fin d, (((n + 1 : K)) ^ (i : ℕ) • L.N i) (L.word (countWord d α.1) Ω) + = ((n + 1 : K) ^ (i : ℕ) * (α.1 i : K)) • L.word (countWord d α.1) Ω := by + intro i + rw [LinearMap.smul_apply, L.N_word hΩ.ann i, count_countWord, + ← Nat.cast_smul_eq_nsmul K, smul_smul] + rw [LinearMap.sum_apply] + simp only [hterm] + rw [← Finset.sum_smul] + congr 1 + unfold countEncode + push_cast + exact Finset.sum_congr rfl (fun i _ => by ring) + +/-- The occupation-number family is linearly independent because its elements are eigenvectors at +pairwise-distinct eigenvalues (`Module.End.eigenvectors_linearIndependent'`). -/ +theorem linearIndependent_word_countFun {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) : + LinearIndependent K (fun α : CountFun d n => L.word (countWord d α.1) Ω) := by + have hinj : Function.Injective (fun α : CountFun d n => (countEncode n α.1 : K)) := by + intro α β hαβ + have hαβ' : countEncode n α.1 = countEncode n β.1 := by + have := hαβ + simp only at this + exact_mod_cast this + exact Subtype.ext (countEncode_injOn α.2 β.2 hαβ') + exact Module.End.eigenvectors_linearIndependent' _ + (fun α : CountFun d n => (countEncode n α.1 : K)) hinj _ + (fun α => L.hasEigenvector_word_countWord P n α) + +/-! + +### C.3. The basis and its dimension + +-/ + +omit [CharZero K] in +/-- The occupation-number family spans `vacuumSpan L Ω n`. -/ +lemma span_word_countFun_eq_vacuumSpan (Ω : V) (n : ℕ) : + Submodule.span K (Set.range fun α : CountFun d n => L.word (countWord d α.1) Ω) + = L.vacuumSpan Ω n := by + apply le_antisymm + · rw [Submodule.span_le] + rintro _ ⟨α, rfl⟩ + exact word_mem_vacuumSpan_of_length_eq L Ω (by + rw [← sum_count_eq_length] + exact (Finset.sum_congr rfl (fun c _ => count_countWord α.1 c)).trans α.2) + · rw [vacuumSpan, Submodule.span_le] + rintro _ ⟨w, rfl⟩ + show L.word (List.ofFn w) Ω ∈ _ + have hsum : (∑ c, (List.ofFn w).count c) = n := by + rw [sum_count_eq_length, List.length_ofFn] + have hperm : L.word (List.ofFn w) Ω + = L.word (countWord d (fun c => (List.ofFn w).count c)) Ω := + L.word_perm (List.perm_iff_count.mpr (fun c => by rw [count_countWord])) Ω + rw [hperm] + exact Submodule.subset_span ⟨⟨fun c => (List.ofFn w).count c, hsum⟩, rfl⟩ + +/-- A basis of `vacuumSpan L Ω n` indexed by degree-`n` occupation-count functions. -/ +noncomputable def vacuumBasis {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) : + Basis (CountFun d n) K (L.vacuumSpan Ω n) := + (Basis.span (L.linearIndependent_word_countFun P n)).map + (LinearEquiv.ofEq _ _ (L.span_word_countFun_eq_vacuumSpan Ω n)) + +lemma vacuumBasis_apply {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) (α : CountFun d n) : + (vacuumBasis L P n α : V) = L.word (countWord d α.1) Ω := by + unfold vacuumBasis + rw [Basis.map_apply, LinearEquiv.coe_ofEq_apply, Basis.coe_span_apply] + +/-- The dimension of `vacuumSpan L Ω n` is `(d+n-1).choose n`, the degeneracy of the `n`-th level +of a `d`-mode bosonic system. -/ +theorem finrank_vacuumSpan_eq_choose {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) : + Module.finrank K (L.vacuumSpan Ω n) = (d + n - 1).choose n := by + rw [Module.finrank_eq_card_basis (vacuumBasis L P n), card_countFun] + +lemma finiteDimensional_vacuumSpan {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) : + FiniteDimensional K (L.vacuumSpan Ω n) := + Module.Basis.finiteDimensional_of_finite (vacuumBasis L P n) + +lemma vacuumSpan_ne_bot {Ω : V} (P : L.HasVacuum Ω) (hd : 0 < d) (n : ℕ) : + L.vacuumSpan Ω n ≠ ⊥ := by + obtain ⟨α⟩ : Nonempty (CountFun d n) := ⟨⟨fun c => if c = ⟨0, hd⟩ then n else 0, by simp⟩⟩ + rw [Submodule.ne_bot_iff] + refine ⟨(vacuumBasis L P n α : V), (vacuumBasis L P n α).2, ?_⟩ + have hne := (vacuumBasis L P n).ne_zero α + exact fun h => hne (Subtype.ext h) + +end LadderSystem diff --git a/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean b/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean new file mode 100644 index 0000000000..752f7e57d6 --- /dev/null +++ b/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Tom Diem. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tom Diem +-/ +module + +public import PhyslibAlpha.Mathematics.LadderSystem.OccupationBasis +public import Mathlib.LinearAlgebra.Finsupp.LinearCombination +/-! + +# The excitation sector is the symmetric power + +## i. Overview + +`vacuumSpan L Ω n` is linearly isomorphic to the `n`-th symmetric power of `K^d` -- concretely, to +the free `K`-vector space on `Sym (Fin d) n` (Mathlib's own type of size-`n` multisets on `Fin d`, +the standard combinatorial model of `Sym^n(K^d)`'s natural basis once a basis `e_1,…,e_d` of `K^d` +is fixed: a multiset `{i_1,…,i_n}` names the basis vector `e_{i_1} ⊙ ⋯ ⊙ e_{i_n}`). The +isomorphism sends this basis to the occupation-number states, i.e. it is exactly +`OccupationBasis.lean`'s `vacuumBasis` reindexed along `countFunEquivSym`. + +## ii. Key results + +- `LadderSystem.vacuumSpanSymEquiv` : `vacuumSpan L Ω n ≃ₗ[K] (Sym (Fin d) n →₀ K)`. + +## iii. References + +-/ + +@[expose] public section + +open Module (Basis) + +namespace LadderSystem + +variable {K V : Type*} [Field K] [CharZero K] [AddCommGroup V] [Module K V] {d : ℕ} + (L : LadderSystem K V d) + +/-- `vacuumSpan L Ω n` is linearly isomorphic to `Sym^n(K^d)` (realized as the free `K`-module +on `Sym (Fin d) n`), matching the natural monomial-type basis on one side to the occupation-number +basis on the other. -/ +noncomputable def vacuumSpanSymEquiv {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) : + (Sym (Fin d) n →₀ K) ≃ₗ[K] L.vacuumSpan Ω n := + Finsupp.basisSingleOne.equiv (vacuumBasis L P n) (countFunEquivSym d n).symm + +/-- The isomorphism sends the basis vector for multiset `s` to the occupation-number state with +that multiset's count function. -/ +lemma vacuumSpanSymEquiv_single {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) (s : Sym (Fin d) n) : + (L.vacuumSpanSymEquiv P n (Finsupp.single s 1) : V) + = L.word (countWord d ((countFunEquivSym d n).symm s).1) Ω := by + have h := Basis.equiv_apply (b := (Finsupp.basisSingleOne : Basis (Sym (Fin d) n) K _)) + (b' := vacuumBasis L P n) (e := (countFunEquivSym d n).symm) s + rw [Finsupp.coe_basisSingleOne] at h + have heq : L.vacuumSpanSymEquiv P n (Finsupp.single s 1) + = vacuumBasis L P n ((countFunEquivSym d n).symm s) := h + rw [heq, vacuumBasis_apply] + +end LadderSystem diff --git a/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean b/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean new file mode 100644 index 0000000000..469c2c4302 --- /dev/null +++ b/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean @@ -0,0 +1,275 @@ +/- +Copyright (c) 2026 Tom Diem. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tom Diem +-/ +module + +public import PhyslibAlpha.Mathematics.LadderSystem.Basic +public import Mathlib.Data.List.Perm.Lattice +public import Mathlib.Algebra.BigOperators.Group.List.Basic +public import Mathlib.Algebra.Lie.Submodule +/-! + +# Vacuum states and creation-operator words + +## i. Overview + +A vacuum `Ω` of a `LadderSystem` is a nonzero vector killed by every annihilation operator. This +file develops creation-operator words `acᵢ₁acᵢ₂⋯acᵢₙΩ` and the excitation-number sector they span, +`vacuumSpan`. This sector is bundled as a `gl(d)` Lie submodule. Its occupation-number basis is +constructed in `OccupationBasis.lean`, and its irreducibility is proved in `Irreducibility.lean`. + +## ii. Key results + +Definitions: +- `LadderSystem.HasVacuum` : `Ω` is nonzero and killed by every `a i`. +- `LadderSystem.word` : a word of creation operators applied to a vector. +- `LadderSystem.vacuumSpan` : the span of all length-`n` words over a vacuum -- the + `n`-particle sector. +- `LadderSystem.vacuumSpanLieSubmodule` : `vacuumSpan`, bundled as a `gl(d)` Lie submodule. + +Theorems: +- `LadderSystem.word_perm` : a word depends only on the multiset of colors it represents. +- `LadderSystem.word_peel` : `aᵢ` applied to a word removes one occurrence of color `i`, scaled + by its count. +- `LadderSystem.E_word`, `LadderSystem.N_word` : how `E i j`/`N i` act on a word. +- `LadderSystem.E_mem_vacuumSpan` : `vacuumSpan` is closed under every `gl(d)` generator `E i j`. + +## iii. Table of contents + +- A. Vacuum states +- B. Words +- C. The excitation-number sector + - C.1. `gl(d)`-invariance + +## iv. References + +-/ + +@[expose] public section + +attribute [local instance 100] LieRing.ofAssociativeRing + +namespace LadderSystem + +variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] {d : ℕ} (L : LadderSystem K V d) + +/-! + +## A. Vacuum states + +-/ + +/-- A vacuum: a nonzero vector killed by every annihilation operator. -/ +structure HasVacuum (Ω : V) : Prop where + /-- A vacuum is nonzero. -/ + ne_zero : Ω ≠ 0 + /-- A vacuum is killed by every annihilation operator. -/ + ann : ∀ i, L.a i Ω = 0 + +variable {L} + +/-! + +## B. Words + +-/ + +/-- A word of creation operators applied to a fixed vector. -/ +def word (L : LadderSystem K V d) (v : List (Fin d)) (x : V) : V := + (v.map L.ac).prod x + +lemma word_cons (L : LadderSystem K V d) (i : Fin d) (v : List (Fin d)) (x : V) : + L.word (i :: v) x = L.ac i (L.word v x) := by + simp [word, Module.End.mul_apply] + +/-- A word depends only on the multiset of colors it represents, not their order. -/ +lemma word_perm (L : LadderSystem K V d) {v v' : List (Fin d)} (h : v.Perm v') (x : V) : + L.word v x = L.word v' x := by + induction h with + | nil => rfl + | cons i _ ih => rw [word_cons, word_cons, ih] + | swap i j v => + have hcomm : (L.ac i * L.ac j : Module.End K V) = L.ac j * L.ac i := by + have h := L.comm_ac_ac i j + rwa [LieRing.of_associative_ring_bracket, sub_eq_zero] at h + simp only [word_cons] + exact congrArg (fun f : Module.End K V => f (L.word v x)) hcomm.symm + | trans _ _ ih1 ih2 => rw [ih1, ih2] + +/-- Peeling: `a i` applied to a word removes one occurrence of color `i`, scaled by its count. -/ +lemma word_peel (L : LadderSystem K V d) (i : Fin d) {x : V} (hx : L.a i x = 0) : + ∀ v : List (Fin d), L.a i (L.word v x) = (v.count i) • L.word (v.erase i) x + | [] => by simp [word, hx] + | c :: v' => by + have hcomm : L.a i * L.ac c + = L.ac c * L.a i + (if i = c then (1 : Module.End K V) else 0) := by + have h := L.comm_a_ac i c + rw [LieRing.of_associative_ring_bracket] at h + exact sub_eq_iff_eq_add'.mp h + have step : L.a i (L.word (c :: v') x) + = L.ac c (L.a i (L.word v' x)) + (if i = c then L.word v' x else 0) := by + rw [word_cons] + have happly := congrArg (fun f : Module.End K V => f (L.word v' x)) hcomm + simpa [Module.End.mul_apply, apply_ite (fun f : Module.End K V => f (L.word v' x))] + using happly + rw [step, word_peel L i hx v'] + by_cases hic : i = c + · subst hic + rw [if_pos rfl, List.count_cons_self, List.erase_cons_head] + by_cases hmem : i ∈ v' + · have hperm : L.word v' x = L.word (i :: v'.erase i) x := + word_perm L (List.perm_cons_erase hmem) x + rw [succ_nsmul, map_nsmul, ← word_cons, ← hperm] + · have hcount : v'.count i = 0 := List.count_eq_zero_of_not_mem hmem + simp [hcount] + · rw [if_neg hic, List.count_cons_of_ne (Ne.symm hic), + List.erase_cons_tail (by simpa using Ne.symm hic), map_nsmul, ← word_cons, add_zero] + +/-- How `E i j` acts on a word: removes one occurrence of `j`, adds one of `i`, scaled by `j`'s +count. -/ +lemma E_word (L : LadderSystem K V d) {x : V} (hx : ∀ i, L.a i x = 0) (i j : Fin d) + (v : List (Fin d)) : + (L.E i j) (L.word v x) = (v.count j) • L.word (i :: v.erase j) x := by + show (L.ac i * L.a j) (L.word v x) = _ + rw [Module.End.mul_apply, word_peel L j (hx j) v, map_nsmul, ← word_cons] + +/-- Words are eigenvectors of the number operator, with eigenvalue their own color count. -/ +lemma N_word (L : LadderSystem K V d) {x : V} (hx : ∀ i, L.a i x = 0) (i : Fin d) + (v : List (Fin d)) : (L.N i) (L.word v x) = (v.count i) • L.word v x := by + rw [N, E_word L hx i i v] + by_cases hmem : i ∈ v + · rw [← word_perm L (List.perm_cons_erase hmem) x] + · simp [List.count_eq_zero_of_not_mem hmem] + +/-! + +## C. The excitation-number sector + +-/ + +/-- The canonical word representing a count function `α`: `α c` copies of color `c`, in +increasing order. -/ +def countWord (d : ℕ) (α : Fin d → ℕ) : List (Fin d) := + (List.finRange d).flatMap (fun c => List.replicate (α c) c) + +/-- `countWord α` has exactly `α i` copies of color `i`. -/ +lemma count_countWord {d : ℕ} (α : Fin d → ℕ) (i : Fin d) : + (countWord d α).count i = α i := by + have key : ∀ (l : List (Fin d)), l.Nodup → i ∈ l → + (l.flatMap (fun c => List.replicate (α c) c)).count i = α i := by + intro l + induction l with + | nil => intro _ hi; exact absurd hi List.not_mem_nil + | cons c l' ih => + intro hnodup hi + obtain ⟨hcl', hnodup'⟩ := List.nodup_cons.mp hnodup + rw [List.flatMap_cons, List.count_append] + rcases List.mem_cons.mp hi with hic | hil' + · subst hic + have hzero : (l'.flatMap (fun c => List.replicate (α c) c)).count i = 0 := by + apply List.count_eq_zero_of_not_mem + intro hmem + obtain ⟨c', hc', hmem'⟩ := List.mem_flatMap.mp hmem + exact hcl' ((List.eq_of_mem_replicate hmem') ▸ hc') + rw [List.count_replicate, hzero] + simp + · have hine : i ≠ c := fun h => hcl' (h ▸ hil') + rw [List.count_replicate, if_neg (by simpa using hine.symm), zero_add] + exact ih hnodup' hil' + exact key (List.finRange d) (List.nodup_finRange d) (List.mem_finRange i) + +/-- A word's length is the sum of its per-color counts. -/ +lemma sum_count_eq_length {d : ℕ} : ∀ v : List (Fin d), (∑ c : Fin d, v.count c) = v.length + | [] => by simp + | a :: v' => by + have hcount : ∀ c : Fin d, (a :: v').count c = v'.count c + (if a = c then 1 else 0) := by + intro c + rw [List.count_cons] + simp only [beq_iff_eq] + have hone : (∑ c : Fin d, if a = c then (1 : ℕ) else 0) = 1 := by + rw [Finset.sum_eq_single a (fun b _ hb => if_neg (Ne.symm hb)) + (fun h => absurd (Finset.mem_univ a) h)] + simp + simp only [hcount, List.length_cons] + rw [Finset.sum_add_distrib, sum_count_eq_length v', hone] + +/-- The `n`-th excitation-number sector generated by a vacuum: the span of all length-`n` +creation words. -/ +def vacuumSpan (L : LadderSystem K V d) (Ω : V) (n : ℕ) : Submodule K V := + Submodule.span K (Set.range fun w : Fin n → Fin d => L.word (List.ofFn w) Ω) + +lemma exists_ofFn_eq_of_length_eq {l : List (Fin d)} {n : ℕ} (h : l.length = n) : + ∃ w : Fin n → Fin d, List.ofFn w = l := by + refine ⟨fun i => l.get (Fin.cast h.symm i), List.ext_get_iff.mpr ⟨by simp [h], ?_⟩⟩ + intro k h1 h2 + rw [List.get_ofFn] + rfl + +/-- Any word of the right length lies in `vacuumSpan`. -/ +lemma word_mem_vacuumSpan_of_length_eq (L : LadderSystem K V d) (Ω : V) {n : ℕ} + {l : List (Fin d)} (h : l.length = n) : L.word l Ω ∈ vacuumSpan L Ω n := by + obtain ⟨w, rfl⟩ := exists_ofFn_eq_of_length_eq h + exact Submodule.subset_span ⟨w, rfl⟩ + +/-! + +### C.1. `gl(d)`-invariance + +-/ + +/-- `E`-invariance of a submodule extends to full `gl(d)`-invariance, by linearity off the +matrix-unit basis. -/ +lemma forall_toGlHomLinear_mem_of_forall_E_mem (L : LadderSystem K V d) {W : Submodule K V} + (hW : ∀ i j, ∀ w ∈ W, (L.E i j) w ∈ W) (x : Matrix (Fin d) (Fin d) K) {w : V} + (hw : w ∈ W) : L.toGlHomLinear x w ∈ W := by + have hx : x ∈ (⊤ : Submodule K (Matrix (Fin d) (Fin d) K)) := Submodule.mem_top + rw [← (Matrix.stdBasis K (Fin d) (Fin d)).span_eq] at hx + induction hx using Submodule.span_induction with + | mem y hy => + obtain ⟨⟨i, j⟩, rfl⟩ := hy + rw [L.toGlHomLinear_stdBasis] + exact hW i j w hw + | zero => simp [W.zero_mem] + | add y y' _ _ ihy ihy' => rw [map_add, LinearMap.add_apply]; exact W.add_mem ihy ihy' + | smul c y _ ihy => rw [map_smul, LinearMap.smul_apply]; exact W.smul_mem c ihy + +/-- `vacuumSpan` is closed under every `gl(d)` generator `E i j`. Unconditional: no +`FiniteDimensional`/spanning hypothesis on the ambient `V` is used or needed. -/ +lemma E_mem_vacuumSpan (L : LadderSystem K V d) {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) + (i j : Fin d) : ∀ v ∈ vacuumSpan L Ω n, (L.E i j) v ∈ vacuumSpan L Ω n := by + intro v hv + rw [vacuumSpan] at hv + induction hv using Submodule.span_induction with + | mem y hy => + obtain ⟨w, rfl⟩ := hy + rw [L.E_word P.ann i j (List.ofFn w)] + rcases Nat.eq_zero_or_pos ((List.ofFn w).count j) with h0 | hpos + · simp [h0] + · have hmem : j ∈ List.ofFn w := List.count_pos_iff.mp hpos + have hlen : (i :: (List.ofFn w).erase j).length = n := by + rw [List.length_cons, List.length_erase_of_mem hmem, List.length_ofFn] + have hn0 : 0 < n := List.length_ofFn (f := w) ▸ List.length_pos_of_mem hmem + omega + exact nsmul_mem (word_mem_vacuumSpan_of_length_eq L Ω hlen) _ + | zero => simp + | add y z _ _ ihy ihz => rw [map_add]; exact Submodule.add_mem _ ihy ihz + | smul c y _ ih => rw [map_smul]; exact Submodule.smul_mem _ c ih + +/-- `vacuumSpan`, bundled as a genuine `gl(d)` Lie submodule. -/ +def vacuumSpanLieSubmodule (L : LadderSystem K V d) {Ω : V} (P : L.HasVacuum Ω) (n : ℕ) : + haveI := L.toLieRingModule + LieSubmodule K (Matrix (Fin d) (Fin d) K) V := by + letI := L.toLieRingModule + refine { toSubmodule := vacuumSpan L Ω n, lie_mem := ?_ } + intro x m hm + show (L.toGlHom x) m ∈ vacuumSpan L Ω n + have heq : L.toGlHom x = L.toGlHomLinear x := rfl + rw [heq] + exact forall_toGlHomLinear_mem_of_forall_E_mem L (E_mem_vacuumSpan L P n) x hm + +@[simp] theorem coe_vacuumSpanLieSubmodule (L : LadderSystem K V d) {Ω : V} (P : L.HasVacuum Ω) + (n : ℕ) : (vacuumSpanLieSubmodule L P n : Submodule K V) = vacuumSpan L Ω n := rfl + +end LadderSystem diff --git a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean new file mode 100644 index 0000000000..d8ec279b9b --- /dev/null +++ b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean @@ -0,0 +1,278 @@ +/- +Copyright (c) 2026 Gregory J. Loges. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gregory J. Loges +-/ +module + +public import Physlib.Meta.Informal.Basic +public import Physlib.QuantumMechanics.Operators.Momentum +public import Physlib.QuantumMechanics.Operators.Multiplication +public import Physlib.QuantumMechanics.QuantumSystem.Basic +/-! + +# The quantum harmonic oscillator + +## i. Overview + +The harmonic oscillator is one of the most public important examples in non-relativistic quantum mechanics. +It describes a particle of mass `m` subject to a positive-definite quadratic potential +in `d` dimensions. + +- `Basic.lean` : Properties of the potential, definition of isotropic oscillators, + kinetic, potential and Hamiltonian operators. +- `LadderOperators.lean` : Definitions of the raising/lowering/number operators + and their algebraic properties. + +## ii. Key results + +- `potentialFunction_apply` : the potential function, expanded to `½m · ∑ᵢ ωᵢ²xᵢ²`. +- `potentialOperator_isSelfAdjoint` : the potential operator is self-adjoint. + +## iii. Table of contents + +- A. Basic properties + - A.1. Positive mass + - A.2. Positive natural frequencies +- B. Characteristic lengths +- C. The quadratic potential function + - C.1. Positive-definite matrix + - C.2. Quadratic form + - C.3. Potential function +- D. Isotropic oscillators +- E. Hilbert space +- F. Operators + - E.1. Kinetic energy + - E.2. Potential energy + - E.3. Hamiltonian +- G. As a quantum system + +## iv. References + +-/ + +@[expose] public section + +TODO "Determine the spectrum of the quantum harmonic oscillator in terms of + the natural frequencies and integer quantum numbers." + +TODO "Determine the energy eigenstates of the quantum harmonic oscillator + in the 'Cartesian basis' in terms of Hermite polynomials." + +TODO "Determine the energy eigenstates of the isotropic quantum harmonic oscillator + in the 'spherical basis' in terms of spherical harmonics." + +noncomputable section +namespace QuantumMechanics + +/-- The `d`-dimensional quantum harmonic oscillator. -/ +structure HarmonicOscillator (d : ℕ) where + /-- The mass (positive). -/ + m : ℝ + hm : 0 < m + /-- The natural frequencies (positive). -/ + ω : Fin d → ℝ + hω : ∀ i, 0 < ω i + +variable {d : ℕ} (Q : HarmonicOscillator d) (i : Fin d) + +namespace HarmonicOscillator + +open Constants SpaceDHilbertSpace MeasureTheory + +/-! +## A. Basic properties +-/ + +/-! +### A.1. Positive mass +-/ + +@[simp] +lemma m_pos : 0 < Q.m := Q.hm + +@[simp] +lemma m_nonneg : 0 ≤ Q.m := Q.hm.le + +@[simp] +lemma m_ne_zero : Q.m ≠ 0 := Q.hm.ne' + +/-! +### A.2. Positive natural frequencies +-/ + +@[simp] +lemma ω_pos : 0 < Q.ω i := Q.hω i + +@[simp] +lemma ω_nonneg : 0 ≤ Q.ω i := (Q.hω i).le + +@[simp] +lemma ω_ne_zero : Q.ω i ≠ 0 := (Q.hω i).ne' + +/-! +## B. Characteristic lengths +-/ + +/-- The characteristic length `ξ i ≔ √ℏ / (√Q.m * √(Q.ω i))`. -/ +def ξ : ℝ := √ℏ / (√Q.m * √(Q.ω i)) + +lemma ξ_eq : Q.ξ i = √ℏ / (√Q.m * √(Q.ω i)) := rfl + +@[simp] +lemma ξ_pos : 0 < Q.ξ i := by simp [ξ_eq] + +@[simp] +lemma ξ_nonneg : 0 ≤ Q.ξ i := (Q.ξ_pos i).le + +@[simp] +lemma ξ_ne_zero : Q.ξ i ≠ 0 := (Q.ξ_pos i).ne' + +lemma ξ_sq : (Q.ξ i) ^ 2 = ℏ / (Q.m * Q.ω i) := by rw [Q.ξ_eq]; field_simp; simp [← mul_rotate] + +lemma ξ_inv : (Q.ξ i)⁻¹ = √Q.m * √(Q.ω i) / √ℏ := by simp [ξ_eq] + +lemma ξ_inv' : (Q.ξ i)⁻¹ = Q.m * Q.ω i * Q.ξ i / ℏ := by field_simp; simp [ξ_sq, mul_assoc] + +/-! +## C. The quadratic potential function +-/ + +section + +open Matrix + +/-! +### C.1. Positive-definite matrix +-/ + +/-- The positive-definite matrix defining the quadratic potential function. -/ +def potentialMatrix : Matrix (Fin d) (Fin d) ℝ := diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2) + +lemma potentialMatrix_eq : Q.potentialMatrix = diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2) := rfl + +lemma potentialMatrix_isHermitian : Q.potentialMatrix.IsHermitian := by simp [potentialMatrix_eq] + +@[simp] +lemma potentialMatrix_mulVec (v : Fin d → ℝ) : + Q.potentialMatrix *ᵥ v = (2⁻¹ * Q.m) • (Q.ω ^ 2 * v) := by + ext + simp [potentialMatrix_eq, smul_mulVec, mulVec_diagonal] + +/-! +### C.2. Quadratic form +-/ + +/-- The positive-definite quadratic form associated to the potential matrix. -/ +def potentialQuadraticForm : QuadraticForm ℝ (Fin d → ℝ) := Q.potentialMatrix.toQuadraticForm' + +/-! +### C.3. Potential function +-/ + +/-- The quadratic potential function, `½m · ∑ i, ωᵢ²·xᵢ²`. -/ +def potentialFunction : Space d → ℝ := Q.potentialQuadraticForm ∘ Space.val + +lemma potentialFunction_eq : Q.potentialFunction = Q.potentialQuadraticForm ∘ Space.val := rfl + +/-- The potential function, expanded: `½m · ∑ᵢ ωᵢ²xᵢ²`. -/ +lemma potentialFunction_apply (x : Space d) : + Q.potentialFunction x = (2⁻¹ * Q.m) * ∑ i, (Q.ω i) ^ 2 * (x i) ^ 2 := by + show Q.potentialQuadraticForm (Space.val x) = _ + rw [potentialQuadraticForm, Matrix.toQuadraticForm', LinearMap.BilinMap.toQuadraticMap_apply, + Matrix.toLinearMap₂'_apply', potentialMatrix_mulVec, dotProduct, Finset.mul_sum] + refine Finset.sum_congr rfl fun i _ => ?_ + simp only [Pi.smul_apply, Pi.mul_apply, Pi.pow_apply, smul_eq_mul] + ring + +/-- The potential function for the harmonic oscillator is continuous, hence a.e. strongly +measurable. -/ +lemma potentialFunction_continuous : Continuous Q.potentialFunction := by + have heq : Q.potentialFunction = fun x => (2⁻¹ * Q.m) * ∑ i, (Q.ω i) ^ 2 * (x i) ^ 2 := + funext Q.potentialFunction_apply + rw [heq] + fun_prop + +/-- The potential function for the harmonic oscillator is a.e. strongly measurable. -/ +lemma potentialFunction_aestronglyMeasurable : + MeasureTheory.AEStronglyMeasurable Q.potentialFunction volume := + Q.potentialFunction_continuous.aestronglyMeasurable + +end + +/-! +## D. Isotropic oscillators +-/ + +/-- A Harmonic oscillator is isotropic if all natural frequencies are equal. -/ +def IsIsotropic : Prop := ∀ i j, Q.ω i = Q.ω j + +lemma isIsotropic_def : Q.IsIsotropic ↔ ∀ i j, Q.ω i = Q.ω j := Iff.rfl + +lemma isIsotropic_of_one (Q : HarmonicOscillator 1) : Q.IsIsotropic := by simp [isIsotropic_def] + +/-! +## E. Hilbert space +-/ + +/-- The Hilbert space for the quantum harmonic oscillator. -/ +@[nolint unusedArguments] +abbrev HS (_ : HarmonicOscillator d) : Type _ := SpaceDHilbertSpace d + +/-! +## F. Operators +-/ + +/-! +### F.1. Kinetic energy +-/ + +/-- The kinetic energy operator, `p²/2m`. -/ +def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := (2 * Q.m)⁻¹ • momentumSqOperator + +/-! +### F.2. Potential energy +-/ + +section + +open MeasureTheory Complex + +/-- The potential operator which maps `ψ` to `Q.potentialFunction • ψ`. -/ +def potentialOperator : Q.HS →ₗ.[ℂ] Q.HS := 𝓜 volume (ofReal ∘ Q.potentialFunction) + +/-- The potential operator for the harmonic oscillator is self-adjoint. -/ +lemma potentialOperator_isSelfAdjoint : IsSelfAdjoint Q.potentialOperator := + mulOperator_isSelfAdjoint_ofReal + (Complex.continuous_ofReal.comp Q.potentialFunction_continuous).aestronglyMeasurable + (by ext; simp) + +end + +/-! +### F.3. Hamiltonian +-/ + +/-- The Hamiltonian for the harmonic oscillator. -/ +def hamiltonian : Q.HS →ₗ.[ℂ] Q.HS := Q.kineticOperator + Q.potentialOperator + +lemma hamiltonain_eq : Q.hamiltonian = Q.kineticOperator + Q.potentialOperator := rfl + +/-- The Hamiltonian for the harmonic oscillator is essentially self-adjoint. -/ +informal_lemma hamiltonian_essentially_self_adjoint where + deps := [``HarmonicOscillator.hamiltonian] + tag := "QM-HO-hamESA" + +/-! +## G. As a quantum system +-/ + +/-- The `d`-dimensional harmonic oscillator as a quantum system + (self-adjoint Hamiltonian acting on a Hilbert space). -/ +informal_definition toQuantumSystem where + deps := [``HarmonicOscillator.hamiltonian_essentially_self_adjoint] + tag := "QM-HO-sys" + +end HarmonicOscillator +end QuantumMechanics +end diff --git a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean new file mode 100644 index 0000000000..4e6c97aa4c --- /dev/null +++ b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean @@ -0,0 +1,250 @@ +/- +Copyright (c) 2026 Gregory J. Loges. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gregory J. Loges, Tom Diem +-/ +module + +public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Basic +public import Physlib.QuantumMechanics.Operators.Commutation +public import PhyslibAlpha.Mathematics.LadderSystem.SymmetricPower +/-! + +# Ladder operators + +## i. Overview + +The raising/lowering (creation/annihilation) operators of the `d`-dimensional quantum harmonic +oscillator, and the number operators built from them, at the level of Schwartz maps `𝓢(Space d, ℂ)` +-- the same level `Position.lean`/`Momentum.lean`/`AngularMomentum.lean` define `𝐱`, `𝐩`, `𝐋` at. + +Not `†`: the creation operator is named `creationCLM`, not notated with `†`, since `†` is reserved +elsewhere (`Operators/Unbounded.lean`) for a *proved* formal adjoint, and `annihilationCLM`/ +`creationCLM` being mutually adjoint is exactly the TODO left open below -- these operators are +defined only at the Schwartz level (as `𝐱`, `𝐩`, `𝐋` are in `Operators/`), not yet promoted to +(partial) operators on `Q.HS` itself. + +The canonical commutation relations in section A define the `LadderSystem` instance +`toLadderSystem`. Section B obtains the number operator and its commutation relations from the +general `LadderSystem` API. + +## ii. Key results + +Definitions: +- `annihilationCLM` : the annihilation operator for mode `i`, + `𝐚ᵢ ≔ (√2)⁻¹(ξᵢ⁻¹𝐱ᵢ + i(ξᵢ/ℏ)𝐩ᵢ)`. +- `creationCLM` : the creation operator for mode `i`, `𝐚ᵢ⁺ ≔ (√2)⁻¹(ξᵢ⁻¹𝐱ᵢ - i(ξᵢ/ℏ)𝐩ᵢ)`. +- `toLadderSystem` : `annihilationCLM`/`creationCLM` bundled as a genuine + `Physlib.Mathematics.LadderSystem` instance. +- `numberCLM` : the number operator for mode `i`, `𝐍ᵢ ≔ 𝐚ᵢ⁺∘𝐚ᵢ`, via `toLadderSystem.N`. + +Theorems: +- `annihilationCLM_comm_creationCLM` : the canonical commutation relations, `[𝐚ᵢ, 𝐚ⱼ⁺] = δᵢⱼ`. +- `numberCLM_comm_numberCLM` : the number operators commute among themselves, `[𝐍ᵢ, 𝐍ⱼ] = 0`. +- `numberCLM_comm_annihilationCLM`, `numberCLM_comm_creationCLM` : `[𝐍ᵢ, 𝐚ⱼ] = -δᵢⱼ𝐚ᵢ` and + `[𝐍ᵢ, 𝐚ⱼ⁺] = δᵢⱼ𝐚ᵢ⁺`. + +## iii. Table of contents + +- A. Ladder operators + - A.1. Canonical commutation relations +- B. Number operators + - B.1. Commutation relations +- C. Hamiltonian + +## iv. References + +-/ + +@[expose] public section + +TODO "Prove that the raising/lowering operators are mutually adjoint with respect to the L² inner + product (tag as simp?)." + +TODO "Promote `annihilationCLM`/`creationCLM`/`numberCLM` from continuous linear maps on + `𝓢(Space d, ℂ)` to (partial) operators on `Q.HS`, as `Position.lean`/`Momentum.lean` do for + `𝐱`/`𝐩`." + +TODO "Prove that the number operators are symmetric/self-adjoint (needs + annihilationCLM/creationCLM's adjointness, promoted to `Q.HS`)." + +TODO "Define a Hamiltonian in terms of the number operators." + +TODO "Prove the commutation relations between the Hamiltonian and ladder/number operators." + +TODO "Relate the 'number operator' Hamiltonian to the 'K + T' Hamiltonian + (=/≤/≥ depending on their domains)." + +TODO "Prove that the two Hamiltonians define the same quantum system." + +namespace QuantumMechanics +namespace HarmonicOscillator +noncomputable section +open Complex Constants +open KroneckerDelta +open ContinuousLinearMap SchwartzMap + +variable {d : ℕ} (Q : HarmonicOscillator d) (i j : Fin d) + +attribute [local instance 100] LieRing.ofAssociativeRing + +/-! + +## A. Ladder operators + +-/ + +/-- The annihilation operator for mode `i`, `𝐚ᵢ ≔ (√2)⁻¹(ξᵢ⁻¹𝐱ᵢ + i(ξᵢ/ℏ)𝐩ᵢ)`, where `ξᵢ` is the +characteristic length of that mode (`HarmonicOscillator.ξ`). -/ +def annihilationCLM (Q : HarmonicOscillator d) (i : Fin d) : + 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := + (√2 : ℂ)⁻¹ • ((Q.ξ i : ℂ)⁻¹ • 𝐱 i + (I * Q.ξ i / ℏ) • 𝐩 i) + +lemma annihilationCLM_apply_fun (Q : HarmonicOscillator d) (i : Fin d) (ψ : 𝓢(Space d, ℂ)) : + Q.annihilationCLM i ψ = + (√2 : ℂ)⁻¹ • ((Q.ξ i : ℂ)⁻¹ • 𝐱 i ψ + (I * Q.ξ i / ℏ) • 𝐩 i ψ) := rfl + +/-- The creation operator for mode `i`, `𝐚ᵢ⁺ ≔ (√2)⁻¹(ξᵢ⁻¹𝐱ᵢ - i(ξᵢ/ℏ)𝐩ᵢ)`. -/ +def creationCLM (Q : HarmonicOscillator d) (i : Fin d) : + 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := + (√2 : ℂ)⁻¹ • ((Q.ξ i : ℂ)⁻¹ • 𝐱 i - (I * Q.ξ i / ℏ) • 𝐩 i) + +lemma creationCLM_apply_fun (Q : HarmonicOscillator d) (i : Fin d) (ψ : 𝓢(Space d, ℂ)) : + Q.creationCLM i ψ = + (√2 : ℂ)⁻¹ • ((Q.ξ i : ℂ)⁻¹ • 𝐱 i ψ - (I * Q.ξ i / ℏ) • 𝐩 i ψ) := rfl + +/-! + +### A.1. Canonical commutation relations + +-/ + +/-- `[𝐚ᵢ, 𝐚ⱼ] = 0`. -/ +@[simp] +theorem annihilationCLM_comm_annihilationCLM (Q : HarmonicOscillator d) (i j : Fin d) : + (⁅Q.annihilationCLM i, Q.annihilationCLM j⁆ : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = 0 := by + rcases eq_or_ne i j with rfl | hij + · exact lie_self _ + · unfold annihilationCLM + simp [smul_lie, lie_smul, add_lie, lie_add, position_commutation_position, + position_commutation_momentum, momentum_commutation_momentum, ← lie_skew (𝐩[d] _) (𝐱 _), + KroneckerDelta.symm j i, eq_zero_of_ne hij] + +/-- `[𝐚ᵢ⁺, 𝐚ⱼ⁺] = 0`. -/ +@[simp] +theorem creationCLM_comm_creationCLM (Q : HarmonicOscillator d) (i j : Fin d) : + (⁅Q.creationCLM i, Q.creationCLM j⁆ : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = 0 := by + rcases eq_or_ne i j with rfl | hij + · exact lie_self _ + · unfold creationCLM + simp [smul_lie, lie_smul, sub_lie, lie_sub, position_commutation_position, + position_commutation_momentum, momentum_commutation_momentum, ← lie_skew (𝐩[d] _) (𝐱 _), + KroneckerDelta.symm j i, eq_zero_of_ne hij] + +/-- The canonical commutation relations for the ladder operators, `[𝐚ᵢ, 𝐚ⱼ⁺] = δᵢⱼ`. -/ +theorem annihilationCLM_comm_creationCLM (Q : HarmonicOscillator d) (i j : Fin d) : + (⁅Q.annihilationCLM i, Q.creationCLM j⁆ : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = + (δ[i,j] : ℂ) • (ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) := by + have hℏ : (ℏ : ℂ) ≠ 0 := by exact_mod_cast Constants.ℏ_ne_zero + have hsqrt2 : ((√2 : ℝ) : ℂ) ^ 2 = 2 := by + rw [← Complex.ofReal_pow, Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 2)] + norm_num + rcases eq_or_ne i j with rfl | hij + · have hξ : (Q.ξ i : ℂ) ≠ 0 := by exact_mod_cast Q.ξ_ne_zero i + rw [eq_one_of_same, Nat.cast_one, one_smul] + unfold annihilationCLM creationCLM + simp only [smul_lie, lie_smul, add_lie, lie_sub, position_commutation_position, + position_commutation_momentum, momentum_commutation_momentum, ← lie_skew (𝐩[d] _) (𝐱 _), + smul_zero, add_zero, smul_neg, smul_smul] + ext ψ x + simp only [sub_apply, add_apply, neg_apply, zero_apply, smul_apply, + ContinuousLinearMap.id_apply, smul_eq_mul, eq_one_of_same] + field_simp + ring_nf + rw [Complex.I_sq, hsqrt2] + ring + · rw [eq_zero_of_ne hij, Nat.cast_zero, zero_smul] + unfold annihilationCLM creationCLM + simp [smul_lie, lie_smul, add_lie, lie_sub, position_commutation_position, + position_commutation_momentum, momentum_commutation_momentum, ← lie_skew (𝐩[d] _) (𝐱 _), + KroneckerDelta.symm j i, eq_zero_of_ne hij] + +/-! + +## B. Number operators + +-/ + +/-- The annihilation and creation operators on Schwartz space, bundled as a `LadderSystem`. +The number operator and its commutation relations below are obtained from this structure. -/ +def toLadderSystem (Q : HarmonicOscillator d) : LadderSystem ℂ (𝓢(Space d, ℂ)) d where + a i := (Q.annihilationCLM i).toLinearMap + ac i := (Q.creationCLM i).toLinearMap + comm_a_ac i j := by + have h := Q.annihilationCLM_comm_creationCLM i j + apply_fun ContinuousLinearMap.toLinearMap at h + rcases eq_or_ne i j with rfl | hij + · simpa [LieRing.of_associative_ring_bracket, ContinuousLinearMap.mul_def, + ContinuousLinearMap.coe_comp, Module.End.mul_eq_comp, Module.End.one_eq_id, + ContinuousLinearMap.one_def] using h + · simpa [LieRing.of_associative_ring_bracket, ContinuousLinearMap.mul_def, + ContinuousLinearMap.coe_comp, Module.End.mul_eq_comp, hij, + KroneckerDelta.eq_zero_of_ne hij] using h + comm_a_a i j := by + have h := Q.annihilationCLM_comm_annihilationCLM i j + apply_fun ContinuousLinearMap.toLinearMap at h + simpa [LieRing.of_associative_ring_bracket, ContinuousLinearMap.mul_def, + ContinuousLinearMap.coe_comp, Module.End.mul_eq_comp] using h + comm_ac_ac i j := by + have h := Q.creationCLM_comm_creationCLM i j + apply_fun ContinuousLinearMap.toLinearMap at h + simpa [LieRing.of_associative_ring_bracket, ContinuousLinearMap.mul_def, + ContinuousLinearMap.coe_comp, Module.End.mul_eq_comp] using h + +/-- The number operator for mode `i`, `𝐍ᵢ ≔ 𝐚ᵢ⁺ ∘ 𝐚ᵢ`, via `toLadderSystem.N`. -/ +def numberCLM (Q : HarmonicOscillator d) (i : Fin d) : + 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := Q.creationCLM i ∘L Q.annihilationCLM i + +theorem toLadderSystem_N_toLinearMap (Q : HarmonicOscillator d) (i : Fin d) : + Q.toLadderSystem.N i = (Q.numberCLM i).toLinearMap := rfl + +/-! + +### B.1. Commutation relations + +-/ + +/-- `[𝐍ᵢ, 𝐚ⱼ] = -δᵢⱼ𝐚ᵢ`, from the general `LadderSystem.lie_N_a` applied to `toLadderSystem`. -/ +theorem numberCLM_comm_annihilationCLM (Q : HarmonicOscillator d) (i j : Fin d) : + (⁅Q.numberCLM i, Q.annihilationCLM j⁆ : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = + (-δ[i,j] : ℂ) • Q.annihilationCLM i := by + have h := Q.toLadderSystem.lie_N_a i j + rw [toLadderSystem_N_toLinearMap] at h + refine ContinuousLinearMap.ext fun ψ => ?_ + have hx := LinearMap.congr_fun h ψ + simpa [toLadderSystem, LieRing.of_associative_ring_bracket, ContinuousLinearMap.mul_def, + ContinuousLinearMap.coe_comp, Module.End.mul_apply] using hx + +/-- `[𝐍ᵢ, 𝐚ⱼ⁺] = δᵢⱼ𝐚ᵢ⁺`, from the general `LadderSystem.lie_N_ac` applied to `toLadderSystem`. -/ +theorem numberCLM_comm_creationCLM (Q : HarmonicOscillator d) (i j : Fin d) : + (⁅Q.numberCLM i, Q.creationCLM j⁆ : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = + (δ[i,j] : ℂ) • Q.creationCLM i := by + rw [numberCLM, leibniz_lie, creationCLM_comm_creationCLM, zero_comp, add_zero, + annihilationCLM_comm_creationCLM, comp_smul, comp_id] + +/-- `[𝐍ᵢ, 𝐍ⱼ] = 0`, from the general `LadderSystem.lie_N_N` applied to `toLadderSystem`. -/ +@[simp] +theorem numberCLM_comm_numberCLM (Q : HarmonicOscillator d) (i j : Fin d) : + (⁅Q.numberCLM i, Q.numberCLM j⁆ : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = 0 := by + rcases eq_or_ne i j with rfl | hij + · exact lie_self _ + · show (⁅Q.creationCLM i ∘L Q.annihilationCLM i, Q.numberCLM j⁆ : + 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) = _ + rw [leibniz_lie, ← lie_skew (Q.annihilationCLM i) (Q.numberCLM j), + numberCLM_comm_annihilationCLM, ← lie_skew (Q.creationCLM i) (Q.numberCLM j), + numberCLM_comm_creationCLM, KroneckerDelta.symm j i, eq_zero_of_ne hij] + simp + +end +end HarmonicOscillator +end QuantumMechanics diff --git a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean new file mode 100644 index 0000000000..27dea1c4c5 --- /dev/null +++ b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean @@ -0,0 +1,278 @@ +/- +Copyright (c) 2026 Tom Diem. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tom Diem +-/ +module + +public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.LadderOperators +public import Physlib.Mathematics.InnerProductSpace.Gaussian +/-! + +# A vacuum state for the harmonic oscillator + +## i. Overview + +For a `d`-dimensional oscillator `Q`, `vacuumGaussian` is the Gaussian +`exp(-∑ᵢ(xᵢ/ξᵢ)²/2)`, rescaled coordinatewise by the characteristic lengths `ξᵢ` through the +diagonal continuous linear equivalence `diagEquiv`. Every annihilation operator kills this +Schwartz function, so `hasVacuum_vacuumGaussian` supplies a `LadderSystem.HasVacuum` witness +without an isotropy assumption. + +The isotropic unit-length case (`Q.ξ i = 1` for all `i`) is represented by +`stdGaussian (Space d) ℂ`, the function `x ↦ exp(-‖x‖²/2)` from +`Physlib.Mathematics.InnerProductSpace.Gaussian`. +`hasVacuum_stdGaussian_of_forall_xi_eq_one` derives the unit-length case from `vacuumGaussian`. +The theorem `annihilationCLM_stdGaussian_of_xi_eq_one` assumes unit length only in the selected +mode, so it is proved separately. + +## ii. Key results + +- `diagEquiv` : the diagonal rescaling of `Space d` by the characteristic lengths. +- `vacuumGaussian` : the anisotropic vacuum Gaussian, `exp(-∑ᵢ(xᵢ/ξᵢ)²/2)`. +- `annihilationCLM_vacuumGaussian` : every `annihilationCLM i` kills the vacuum Gaussian. +- `hasVacuum_vacuumGaussian` : `Q.vacuumGaussian` is a vacuum for `Q.toLadderSystem`. +- `annihilationCLM_stdGaussian_of_xi_eq_one`, `hasVacuum_stdGaussian_of_forall_xi_eq_one` : the + isotropic-unit-length special case. + +## iii. References + +-/ + +@[expose] public section + +namespace QuantumMechanics +namespace HarmonicOscillator +noncomputable section +open Complex Constants InnerProductSpace +open ContinuousLinearMap SchwartzMap + +variable {d : ℕ} (Q : HarmonicOscillator d) + +/-! + +## The standard Gaussian: derivative and momentum action + +`Q`-free prerequisites about the plain, unscaled Gaussian, reused by both the general anisotropic +case below and the isotropic-unit-length special case at the end of this file. + +-/ + +/-- The real-valued Gaussian `exp(-‖x‖²/2)`'s coordinate derivative, +`∂ᵢ g = -xᵢ · g`. -/ +lemma deriv_realGaussian (x : Space d) (i : Fin d) : + Space.deriv i (fun x : Space d => Real.exp (-2⁻¹ * ‖x‖ ^ 2)) x = + -x i * Real.exp (-2⁻¹ * ‖x‖ ^ 2) := by + have hsq : DifferentiableAt ℝ (fun x : Space d => ‖x‖ ^ 2) x := + Space.norm_sq_differentiable.differentiableAt + have hdiff2 : DifferentiableAt ℝ Real.exp (-2⁻¹ * ‖x‖ ^ 2) := Real.differentiableAt_exp + have hdiff3 : DifferentiableAt ℝ (fun x : Space d => -2⁻¹ * ‖x‖ ^ 2) x := hsq.const_mul _ + change Space.deriv i (Real.exp ∘ (fun x : Space d => -2⁻¹ * ‖x‖ ^ 2)) x = _ + rw [Space.deriv_eq, fderiv_comp x hdiff2 hdiff3, fderiv_const_mul hsq (-2⁻¹ : ℝ), + fderiv_norm_sq_apply] + simp [Real.deriv_exp] + +/-- `stdGaussian (Space d) ℂ`'s pointwise value is the real-valued Gaussian, cast to `ℂ`. -/ +lemma stdGaussian_apply' (x : Space d) : + (stdGaussian (Space d) ℂ : Space d → ℂ) x = Real.exp (-2⁻¹ * ‖x‖ ^ 2) := by + simp [stdGaussian, gaussian₀, gaussian_apply] + +/-- The coordinate derivative of the standard Gaussian, `∂ᵢ Ω = -xᵢ • Ω`. -/ +lemma deriv_stdGaussian (x : Space d) (i : Fin d) : + Space.deriv i (fun x : Space d => (stdGaussian (Space d) ℂ : Space d → ℂ) x) x = + (-x i : ℂ) * (stdGaussian (Space d) ℂ : Space d → ℂ) x := by + have hsq : DifferentiableAt ℝ (fun x : Space d => Real.exp (-2⁻¹ * ‖x‖ ^ 2)) x := by + have hsq' : DifferentiableAt ℝ (fun x : Space d => ‖x‖ ^ 2) x := + Space.norm_sq_differentiable.differentiableAt + exact Real.differentiableAt_exp.comp x (hsq'.const_mul (-2⁻¹ : ℝ)) + have heq : (fun x : Space d => (stdGaussian (Space d) ℂ : Space d → ℂ) x) = + Complex.ofRealCLM ∘ (fun x : Space d => Real.exp (-2⁻¹ * ‖x‖ ^ 2)) := by + funext x + simp + rw [heq, Space.deriv_eq, fderiv_comp x Complex.ofRealCLM.differentiableAt hsq] + simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.fderiv] + rw [show (fderiv ℝ (fun x : Space d => Real.exp (-2⁻¹ * ‖x‖ ^ 2)) x) (Space.basis i) = + Space.deriv i (fun x => Real.exp (-2⁻¹ * ‖x‖ ^ 2)) x from (Space.deriv_eq i _ x).symm, + deriv_realGaussian, stdGaussian_apply', Complex.ofRealCLM_apply] + push_cast + ring + +/-- The momentum operator applied to the standard Gaussian, +`𝐩ᵢ Ω = -iℏ·(-xᵢ)Ω = iℏxᵢ·Ω`. -/ +lemma momentumCLM_stdGaussian (i : Fin d) (x : Space d) : + (𝐩[d] i (stdGaussian (Space d) ℂ) : 𝓢(Space d, ℂ)) x = + (I * ℏ * x i : ℂ) * (stdGaussian (Space d) ℂ : Space d → ℂ) x := by + rw [momentumCLM_apply] + show -I * ℏ * Space.deriv i (fun x => (stdGaussian (Space d) ℂ : Space d → ℂ) x) x = _ + rw [deriv_stdGaussian] + ring + +/-! + +## The general, anisotropic vacuum + +No isotropy assumption needed: every oscillator `Q` (any masses/frequencies, hence any +characteristic lengths `ξᵢ`) has an explicit vacuum, the Gaussian rescaled coordinatewise by `ξ`. + +-/ + +/-- The diagonal rescaling of `Space d` by the characteristic lengths, `(Q.diagEquiv x) i = ξᵢxᵢ`. +Composing the standard Gaussian with its inverse turns the standard Gaussian's isotropic width into +the anisotropic width `ξᵢ` required by a vacuum of `Q`, whether or not `Q` itself is +isotropic (contrast `stdGaussian`/`hasVacuum_stdGaussian_of_forall_xi_eq_one` below, which only +covers `∀ i, ξᵢ = 1`). -/ +noncomputable def diagEquiv (Q : HarmonicOscillator d) : Space d ≃L[ℝ] Space d := + (Space.equivPi d).trans <| + (ContinuousLinearEquiv.piCongrRight + fun i => ContinuousLinearEquiv.smulLeft (Units.mk0 (Q.ξ i) (Q.ξ_ne_zero i))).trans + (Space.equivPi d).symm + +@[simp] theorem diagEquiv_apply (x : Space d) (i : Fin d) : Q.diagEquiv x i = Q.ξ i * x i := rfl + +@[simp] theorem diagEquiv_symm_apply (x : Space d) (i : Fin d) : + Q.diagEquiv.symm x i = (Q.ξ i)⁻¹ * x i := rfl + +/-- The vacuum Gaussian of `Q`: the anisotropic Gaussian `exp(-∑ᵢ(xᵢ/ξᵢ)²/2)`, `Q.diagEquiv` +applied to the standard one. Equals `stdGaussian (Space d) ℂ` exactly when every `ξᵢ = 1`. -/ +noncomputable def vacuumGaussian (Q : HarmonicOscillator d) : 𝓢(Space d, ℂ) := + gaussian₀ ℂ Q.diagEquiv + +lemma vacuumGaussian_apply (x : Space d) : + (Q.vacuumGaussian : Space d → ℂ) x = Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2) := by + simp [vacuumGaussian, gaussian₀, gaussian_apply] + +/-- `Q.diagEquiv.symm` applied to a basis vector rescales it by `(ξᵢ)⁻¹`. -/ +lemma diagEquiv_symm_basis (i : Fin d) : + Q.diagEquiv.symm (Space.basis i) = (Q.ξ i)⁻¹ • Space.basis i := by + ext j + by_cases h : i = j <;> simp [diagEquiv_symm_apply, Space.basis_apply, h] + +/-- The Fréchet derivative of the anisotropic Gaussian's real exponent `‖Q.diagEquiv.symm ·‖²`, +at the CLM level (mirrors `fderiv_norm_sq_apply`, composed with `Q.diagEquiv.symm`). -/ +lemma fderiv_norm_sq_diagEquiv_symm (x : Space d) : + fderiv ℝ (fun x : Space d => ‖Q.diagEquiv.symm x‖ ^ 2) x = + (2 • innerSL ℝ (Q.diagEquiv.symm x)) ∘L (Q.diagEquiv.symm : Space d →L[ℝ] Space d) := by + have hlin : DifferentiableAt ℝ Q.diagEquiv.symm x := Q.diagEquiv.symm.differentiableAt + have hsq : DifferentiableAt ℝ (fun y : Space d => ‖y‖ ^ 2) (Q.diagEquiv.symm x) := + Space.norm_sq_differentiable.differentiableAt + change fderiv ℝ ((fun y : Space d => ‖y‖ ^ 2) ∘ Q.diagEquiv.symm) x = _ + rw [fderiv_comp x hsq hlin, ContinuousLinearEquiv.fderiv, fderiv_norm_sq_apply] + +/-- The real-valued anisotropic Gaussian's coordinate derivative, +`∂ᵢ g = -(xᵢ/ξᵢ²) · g`. -/ +lemma deriv_realGaussian_diag (x : Space d) (i : Fin d) : + Space.deriv i (fun x : Space d => Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2)) x = + -(x i / (Q.ξ i) ^ 2) * Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2) := by + have hsq : DifferentiableAt ℝ (fun x : Space d => ‖Q.diagEquiv.symm x‖ ^ 2) x := + (Space.norm_sq_differentiable.comp Q.diagEquiv.symm.differentiable).differentiableAt + have hdiff2 : DifferentiableAt ℝ Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2) := + Real.differentiableAt_exp + have hdiff3 : DifferentiableAt ℝ (fun x : Space d => -2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2) x := + hsq.const_mul _ + change Space.deriv i (Real.exp ∘ (fun x : Space d => -2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2)) x = _ + rw [Space.deriv_eq, fderiv_comp x hdiff2 hdiff3, fderiv_const_mul hsq (-2⁻¹ : ℝ), + fderiv_norm_sq_diagEquiv_symm] + simp [ContinuousLinearMap.comp_apply, smul_apply, ContinuousLinearEquiv.coe_coe, + Q.diagEquiv_symm_basis i, Space.inner_basis, diagEquiv_symm_apply, + innerSL_apply_apply, Real.deriv_exp] + ring + +/-- The coordinate derivative of the vacuum Gaussian, `∂ᵢ Ω = -(xᵢ/ξᵢ²) • Ω`. -/ +lemma deriv_vacuumGaussian (x : Space d) (i : Fin d) : + Space.deriv i (fun x : Space d => (Q.vacuumGaussian : Space d → ℂ) x) x = + (-(x i / (Q.ξ i) ^ 2 : ℝ) : ℂ) * (Q.vacuumGaussian : Space d → ℂ) x := by + have hsq : DifferentiableAt ℝ + (fun x : Space d => Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2)) x := by + have hsq' : DifferentiableAt ℝ (fun x : Space d => ‖Q.diagEquiv.symm x‖ ^ 2) x := + (Space.norm_sq_differentiable.comp Q.diagEquiv.symm.differentiable).differentiableAt + exact Real.differentiableAt_exp.comp x (hsq'.const_mul (-2⁻¹ : ℝ)) + have heq : (fun x : Space d => (Q.vacuumGaussian : Space d → ℂ) x) = + Complex.ofRealCLM ∘ (fun x : Space d => Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2)) := by + funext x + simp [Q.vacuumGaussian_apply] + rw [heq, Space.deriv_eq, fderiv_comp x Complex.ofRealCLM.differentiableAt hsq] + simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.fderiv] + rw [show (fderiv ℝ (fun x : Space d => Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2)) x) + (Space.basis i) = + Space.deriv i (fun x => Real.exp (-2⁻¹ * ‖Q.diagEquiv.symm x‖ ^ 2)) x + from (Space.deriv_eq i _ x).symm, + deriv_realGaussian_diag, Q.vacuumGaussian_apply, Complex.ofRealCLM_apply] + push_cast + ring + +/-- The momentum operator applied to the vacuum Gaussian, +`𝐩ᵢ Ω = iℏ(xᵢ/ξᵢ²)·Ω`. -/ +lemma momentumCLM_vacuumGaussian (i : Fin d) (x : Space d) : + (𝐩[d] i (Q.vacuumGaussian) : 𝓢(Space d, ℂ)) x = + (I * ℏ * (x i / (Q.ξ i) ^ 2 : ℝ) : ℂ) * (Q.vacuumGaussian : Space d → ℂ) x := by + rw [momentumCLM_apply] + show -I * ℏ * Space.deriv i (fun x => (Q.vacuumGaussian : Space d → ℂ) x) x = _ + rw [deriv_vacuumGaussian] + ring + +/-- Every `annihilationCLM i` kills the vacuum Gaussian, without an isotropy or unit-length +assumption. -/ +theorem annihilationCLM_vacuumGaussian (i : Fin d) : + Q.annihilationCLM i (Q.vacuumGaussian) = 0 := by + have hℏ : (ℏ : ℂ) ≠ 0 := by exact_mod_cast Constants.ℏ_ne_zero + have hξ : (Q.ξ i : ℂ) ≠ 0 := by exact_mod_cast Q.ξ_ne_zero i + ext x + rw [annihilationCLM_apply_fun] + simp only [smul_apply, add_apply, smul_eq_mul, zero_apply, positionCLM_apply] + rw [show (𝐩 i) (Q.vacuumGaussian) x = + (𝐩[d] i (Q.vacuumGaussian) : 𝓢(Space d, ℂ)) x from rfl, + momentumCLM_vacuumGaussian] + push_cast + field_simp + norm_num [Complex.I_sq] + +/-- `Q.vacuumGaussian` is a vacuum for `Q.toLadderSystem`, without an isotropy assumption. -/ +theorem hasVacuum_vacuumGaussian : Q.toLadderSystem.HasVacuum (Q.vacuumGaussian) where + ne_zero := by + intro h + have hpt := congrFun (congrArg DFunLike.coe h) (⟨fun _ => 0⟩ : Space d) + simp [Q.vacuumGaussian_apply] at hpt + ann i := by + show (Q.annihilationCLM i).toLinearMap (Q.vacuumGaussian) = 0 + rw [show (Q.annihilationCLM i).toLinearMap (Q.vacuumGaussian) = + Q.annihilationCLM i (Q.vacuumGaussian) from rfl, + Q.annihilationCLM_vacuumGaussian i] + +/-! + +## The isotropic-unit-length special case + +-/ + +/-- Every `annihilationCLM i` kills the standard Gaussian, provided that mode has unit +characteristic length. Independent of `hasVacuum_vacuumGaussian`/`annihilationCLM_vacuumGaussian` +above: the hypothesis here is genuinely weaker (unit length in mode `i` alone, not every mode), so +this isn't a corollary of the general anisotropic result. -/ +lemma annihilationCLM_stdGaussian_of_xi_eq_one (i : Fin d) (hξ : Q.ξ i = 1) : + Q.annihilationCLM i (stdGaussian (Space d) ℂ) = 0 := by + have hℏ : (ℏ : ℂ) ≠ 0 := by exact_mod_cast Constants.ℏ_ne_zero + ext x + rw [annihilationCLM_apply_fun] + simp only [smul_apply, add_apply, smul_eq_mul, zero_apply, positionCLM_apply] + rw [show (𝐩 i) (stdGaussian (Space d) ℂ) x = + (𝐩[d] i (stdGaussian (Space d) ℂ) : 𝓢(Space d, ℂ)) x from rfl, + momentumCLM_stdGaussian, hξ] + field_simp + norm_num [Complex.I_sq] + +/-- `stdGaussian (Space d) ℂ` is a vacuum for `Q.toLadderSystem` when every mode has unit +characteristic length. -/ +lemma hasVacuum_stdGaussian_of_forall_xi_eq_one (hξ : ∀ i, Q.ξ i = 1) : + Q.toLadderSystem.HasVacuum (stdGaussian (Space d) ℂ) := by + have heq : Q.vacuumGaussian = stdGaussian (Space d) ℂ := by + ext x + have hsymm : Q.diagEquiv.symm x = x := by + ext j + simp [diagEquiv_symm_apply, hξ j] + rw [Q.vacuumGaussian_apply, stdGaussian_apply', hsymm] + rw [← heq] + exact Q.hasVacuum_vacuumGaussian + +end +end HarmonicOscillator +end QuantumMechanics From 4f06dd0e5e6af6914d8becc0fe7cf8a124677405 Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Sun, 20 Sep 2026 22:30:12 +0200 Subject: [PATCH 2/8] feat(ProbabilisticTheory): order-unit spaces Adds the order-unit foundation for a general probabilistic theory: IsOrderUnit/IsOrderUnitElement (OrderUnit/Basic.lean), the positive cone and its order-unit-shift lemma (OrderUnit/Cone.lean), and the Archimedean order-unit norm with its induced normed-space structure and order-closed topology (OrderUnit/Archimedean.lean). Co-Authored-By: Claude Sonnet 5 --- Physlib.lean | 3 + .../OrderUnit/Archimedean.lean | 422 ++++++++++++++++++ .../ProbabilisticTheory/OrderUnit/Basic.lean | 96 ++++ .../ProbabilisticTheory/OrderUnit/Cone.lean | 109 +++++ 4 files changed, 630 insertions(+) create mode 100644 Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean create mode 100644 Physlib/ProbabilisticTheory/OrderUnit/Basic.lean create mode 100644 Physlib/ProbabilisticTheory/OrderUnit/Cone.lean diff --git a/Physlib.lean b/Physlib.lean index e1f45bd088..623cfc1443 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -254,6 +254,9 @@ 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.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 diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean new file mode 100644 index 0000000000..5386b81bed --- /dev/null +++ b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean @@ -0,0 +1,422 @@ +/- +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.Analysis.Normed.Module.Basic +public import Mathlib.Topology.Sequences +public import Mathlib.Topology.Order.OrderClosed +public import Physlib.ProbabilisticTheory.OrderUnit.Basic + +/-! + +# Archimedean order-unit spaces + +## i. Overview + +The Archimedean condition is a regularity assumption on an order-unit space that rules out +infinitesimal elements. With it, the order and the distinguished unit `1` determine a natural +norm, + +`‖A‖₁ = inf {r ≥ 0 | -r • 1 ≤ A ≤ r • 1}`. + +Thus the unit interval sets the scale of the theory: `[-1, 1]` is exactly the closed unit ball. For +self-adjoint matrices, this recovers the usual operator norm. Concretely, this is the Minkowski +functional of the order interval `[-1, 1]`: convexity of that interval gives the triangle +inequality, and its symmetry gives homogeneity, for free. The Archimedean condition is only needed +afterwards, to upgrade this from a seminorm to a genuine norm. + +This file develops this norm and packages a copy of `E` carrying it as `WithOrderUnitNorm E`. + +## ii. Key results + +- `IsArchimedeanOrderUnit.orderUnitNorm_eq_zero_iff` : the order-unit norm separates points. +- `IsArchimedeanOrderUnit.closedIciTopology` : the positive cone is closed in the order-unit-norm + topology. + +## iii. Table of contents + +- A. Archimedean order units +- B. The order-unit bounds and norm +- C. Norm axioms +- D. The induced normed space +- E. Order-closedness of the topology +- F. A separate copy carrying the order-unit norm + +## iv. References + +-/ + +@[expose] public section + +/-! + +## A. Archimedean order units + +-/ + +/-- The distinguished element `1` is an Archimedean order unit. -/ +class IsArchimedeanOrderUnit (E : Type*) [AddCommGroup E] [PartialOrder E] [Module ℝ E] [One E] : + Prop extends IsOrderUnit E where + /-- If `A` is smaller than every positive multiple of `1`, however small, `A` is already + `≤ 0`. -/ + le_zero_of_forall_pos_smul_one_le : ∀ A : E, (∀ ε : ℝ, 0 < ε → A ≤ ε • (1 : E)) → A ≤ 0 + +/-- The real numbers form an Archimedean order-unit space. -/ +instance instIsArchimedeanOrderUnitReal : IsArchimedeanOrderUnit ℝ where + isOrderUnitElement_one := ⟨zero_le_one, fun A => by + obtain ⟨n, hn⟩ := exists_nat_ge A + exact ⟨n, by simpa using hn⟩⟩ + le_zero_of_forall_pos_smul_one_le A hA := by + by_contra h + have hApos : 0 < A := lt_of_not_ge h + have := hA (A / 2) (by positivity) + simp only [smul_eq_mul, mul_one] at this + linarith + +namespace IsArchimedeanOrderUnit + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] + [One E] [IsArchimedeanOrderUnit E] + +/-! + +## B. The order-unit bounds and norm + +-/ + +/-- The nonnegative scalars that bound an element on both sides by the order unit. -/ +def orderUnitBounds (A : E) : Set ℝ := + {r | 0 ≤ r ∧ -(r • (1 : E)) ≤ A ∧ A ≤ r • (1 : E)} + +/-- The order-unit norm is the infimum of the order-unit bounds. -/ +noncomputable def orderUnitNorm (A : E) : ℝ := + sInf (orderUnitBounds A) + +/-- Every element has some order-unit bound: this is just `IsOrderUnit`'s two-sided bound, +repackaged as a natural number in `orderUnitBounds`. -/ +lemma orderUnitBounds_nonempty (A : E) : (orderUnitBounds A).Nonempty := by + obtain ⟨n, hl, hu⟩ := IsOrderUnit.exists_two_sided_bound A + refine ⟨n, Nat.cast_nonneg n, ?_, ?_⟩ + · simpa only [Nat.cast_smul_eq_nsmul] using hl + · simpa only [Nat.cast_smul_eq_nsmul] using hu + +omit [IsOrderedAddMonoid E] [IsArchimedeanOrderUnit E] in +/-- The order-unit bounds are bounded below by `0`, so their infimum (the norm) is well-behaved. -/ +lemma orderUnitBounds_bddBelow (A : E) : BddBelow (orderUnitBounds A) := + ⟨0, fun _ hr ↦ hr.1⟩ + +/-- The order-unit norm is an infimum of nonnegative reals, hence itself nonnegative. -/ +lemma orderUnitNorm_nonneg (A : E) : 0 ≤ orderUnitNorm A := + le_csInf (orderUnitBounds_nonempty A) fun _ hr ↦ hr.1 + +omit [IsOrderedAddMonoid E] [IsArchimedeanOrderUnit E] in +/-- Any order-unit bound on `A` is an upper bound for `A`'s order-unit norm. -/ +lemma orderUnitNorm_le {A : E} {r : ℝ} (hr : r ∈ orderUnitBounds A) : + orderUnitNorm A ≤ r := + csInf_le (orderUnitBounds_bddBelow A) hr + +@[simp] +lemma orderUnitNorm_zero : orderUnitNorm (0 : E) = 0 := by + apply le_antisymm + · exact orderUnitNorm_le ⟨le_rfl, by simp, by simp⟩ + · exact orderUnitNorm_nonneg 0 + +omit [IsArchimedeanOrderUnit E] in +/-- Negation preserves the set of order-unit bounds: a symmetric interval bounding `A` bounds +`-A` too. -/ +lemma orderUnitBounds_neg (A : E) : orderUnitBounds (-A) = orderUnitBounds A := by + ext r + constructor <;> rintro ⟨hr, hl, hu⟩ <;> + exact ⟨hr, by simpa only [neg_neg] using neg_le_neg hu, + by simpa only [neg_smul, neg_neg] using neg_le_neg hl⟩ + +omit [IsArchimedeanOrderUnit E] in +@[simp] +lemma orderUnitNorm_neg (A : E) : orderUnitNorm (-A) = orderUnitNorm A := by + unfold orderUnitNorm + rw [orderUnitBounds_neg] + +omit [IsArchimedeanOrderUnit E] in +/-- Order-unit bounds add: a bound for `A` and a bound for `B` combine to a bound for `A + B`, +which is what drives the triangle inequality for `orderUnitNorm`. -/ +lemma add_mem_orderUnitBounds {A B : E} {r s : ℝ} (hr : r ∈ orderUnitBounds A) + (hs : s ∈ orderUnitBounds B) : r + s ∈ orderUnitBounds (A + B) := by + refine ⟨add_nonneg hr.1 hs.1, ?_, ?_⟩ + · rw [add_smul, neg_add] + exact add_le_add hr.2.1 hs.2.1 + · rw [add_smul] + exact add_le_add hr.2.2 hs.2.2 + +/-- An infimum can always be approximated from above: there is an order-unit bound on `A` within +`ε` of the norm itself. -/ +lemma exists_orderUnitBound_lt (A : E) {ε : ℝ} (hε : 0 < ε) : + ∃ r ∈ orderUnitBounds A, r < orderUnitNorm A + ε := by + apply exists_lt_of_csInf_lt (orderUnitBounds_nonempty A) + exact lt_add_of_pos_right _ hε + +lemma orderUnitNorm_add_le (A B : E) : + orderUnitNorm (A + B) ≤ orderUnitNorm A + orderUnitNorm B := by + apply le_of_forall_pos_le_add + intro ε hε + obtain ⟨r, hr, hrlt⟩ := exists_orderUnitBound_lt A (half_pos hε) + obtain ⟨s, hs, hslt⟩ := exists_orderUnitBound_lt B (half_pos hε) + calc + orderUnitNorm (A + B) ≤ r + s := orderUnitNorm_le (add_mem_orderUnitBounds hr hs) + _ ≤ (orderUnitNorm A + ε / 2) + (orderUnitNorm B + ε / 2) := + add_le_add hrlt.le hslt.le + _ = orderUnitNorm A + orderUnitNorm B + ε := by ring + +/-! + +## C. Norm axioms + +-/ + +variable [PosSMulMono ℝ E] + +/-- Scaling the unit by a larger nonnegative real gives a larger multiple: `r ↦ r • 1` is +monotone. -/ +lemma smul_one_mono {r s : ℝ} (hrs : r ≤ s) : + r • (1 : E) ≤ s • (1 : E) := by + have h : 0 ≤ (s - r) • (1 : E) := + smul_nonneg (sub_nonneg.mpr hrs) IsOrderUnit.one_nonneg + calc + r • (1 : E) = s • (1 : E) - (s - r) • (1 : E) := by + rw [← sub_smul, sub_sub_cancel] + _ ≤ s • (1 : E) := sub_le_self _ h + +/-- The infimum defining the order-unit norm is attained. This is where the Archimedean axiom +is used, to pass from "bounded by `r + ε` for every `ε`" to "bounded by `r`". -/ +lemma le_orderUnitNorm_smul_one (A : E) : A ≤ orderUnitNorm A • (1 : E) := by + apply sub_nonpos.mp + apply le_zero_of_forall_pos_smul_one_le + intro ε hε + obtain ⟨r, hr, hrlt⟩ := exists_orderUnitBound_lt A hε + calc + A - orderUnitNorm A • (1 : E) ≤ r • (1 : E) - orderUnitNorm A • (1 : E) := + sub_le_sub_right hr.2.2 _ + _ = (r - orderUnitNorm A) • (1 : E) := by rw [sub_smul] + _ ≤ ε • (1 : E) := smul_one_mono (by linarith) + +/-- `A` is also bounded below by `-(orderUnitNorm A • 1)`. -/ +lemma neg_orderUnitNorm_smul_one_le (A : E) : -(orderUnitNorm A • (1 : E)) ≤ A := by + have h := le_orderUnitNorm_smul_one (-A) + rw [orderUnitNorm_neg] at h + simpa only [neg_smul, neg_neg] using neg_le_neg h + +/-- The norm itself is an order-unit bound, i.e. the infimum defining `orderUnitNorm` is a +minimum. -/ +lemma orderUnitNorm_mem_orderUnitBounds (A : E) : orderUnitNorm A ∈ orderUnitBounds A := + ⟨orderUnitNorm_nonneg A, neg_orderUnitNorm_smul_one_le A, le_orderUnitNorm_smul_one A⟩ + +/-- An element with order-unit norm strictly below `ε` is itself bounded above by `ε • 1`. -/ +lemma le_smul_one_of_orderUnitNorm_lt {A : E} {ε : ℝ} (h : orderUnitNorm A < ε) : + A ≤ ε • (1 : E) := + (le_orderUnitNorm_smul_one A).trans (smul_one_mono h.le) + +/-- The mirror image of `le_smul_one_of_orderUnitNorm_lt`. -/ +lemma neg_smul_one_le_of_orderUnitNorm_lt {A : E} {ε : ℝ} (h : orderUnitNorm A < ε) : + -(ε • (1 : E)) ≤ A := by + have h' : -A ≤ ε • (1 : E) := le_smul_one_of_orderUnitNorm_lt (by rwa [orderUnitNorm_neg]) + simpa using neg_le_neg h' + +/-- The order-unit norm is characterized exactly by its symmetric order interval. -/ +lemma orderUnitNorm_le_iff {A : E} {r : ℝ} : + orderUnitNorm A ≤ r ↔ 0 ≤ r ∧ -(r • (1 : E)) ≤ A ∧ A ≤ r • (1 : E) := by + constructor + · intro h + refine ⟨(orderUnitNorm_nonneg A).trans h, ?_, ?_⟩ + · exact (neg_le_neg (smul_one_mono h)).trans (neg_orderUnitNorm_smul_one_le A) + · exact (le_orderUnitNorm_smul_one A).trans (smul_one_mono h) + · exact orderUnitNorm_le + +/-- The order-unit norm is definite: `‖A‖₁ = 0` forces `A = 0`. -/ +lemma orderUnitNorm_eq_zero_iff {A : E} : orderUnitNorm A = 0 ↔ A = 0 := by + constructor + · intro hA + have h := orderUnitNorm_mem_orderUnitBounds A + have hu : A ≤ 0 := by simpa [hA] using h.2.2 + have hl : 0 ≤ A := by simpa [hA] using h.2.1 + exact le_antisymm hu hl + · rintro rfl + exact orderUnitNorm_zero + +/-- Nonnegative scalar multiplication scales the order-unit norm from above. -/ +lemma orderUnitNorm_smul_le {r : ℝ} (hr : 0 ≤ r) (A : E) : + orderUnitNorm (r • A) ≤ r * orderUnitNorm A := by + apply orderUnitNorm_le_iff.mpr + refine ⟨mul_nonneg hr (orderUnitNorm_nonneg A), ?_, ?_⟩ + · calc + -((r * orderUnitNorm A) • (1 : E)) = r • -(orderUnitNorm A • (1 : E)) := by + rw [smul_neg, smul_smul] + _ ≤ r • A := + smul_le_smul_of_nonneg_left (neg_orderUnitNorm_smul_one_le A) hr + · calc + r • A ≤ r • (orderUnitNorm A • (1 : E)) := + smul_le_smul_of_nonneg_left (le_orderUnitNorm_smul_one A) hr + _ = (r * orderUnitNorm A) • (1 : E) := by rw [smul_smul] + +/-- Positive scalar multiplication scales the order-unit norm. -/ +lemma orderUnitNorm_smul_of_pos {r : ℝ} (hr : 0 < r) (A : E) : + orderUnitNorm (r • A) = r * orderUnitNorm A := by + apply le_antisymm + · exact orderUnitNorm_smul_le hr.le A + · have h := orderUnitNorm_smul_le (inv_nonneg.mpr hr.le) (r • A) + have hA : orderUnitNorm A ≤ r⁻¹ * orderUnitNorm (r • A) := by + calc + orderUnitNorm A = orderUnitNorm (r⁻¹ • (r • A)) := by + rw [smul_smul, inv_mul_cancel₀ hr.ne', one_smul] + _ ≤ r⁻¹ * orderUnitNorm (r • A) := h + calc + r * orderUnitNorm A ≤ r * (r⁻¹ * orderUnitNorm (r • A)) := + mul_le_mul_of_nonneg_left hA hr.le + _ = orderUnitNorm (r • A) := by + rw [← mul_assoc, mul_inv_cancel₀ hr.ne', one_mul] + +/-- The order-unit norm is absolutely homogeneous. -/ +lemma orderUnitNorm_smul (r : ℝ) (A : E) : + orderUnitNorm (r • A) = |r| * orderUnitNorm A := by + rcases lt_trichotomy r 0 with hr | rfl | hr + · calc + orderUnitNorm (r • A) = orderUnitNorm ((-r) • (-A)) := by + rw [smul_neg, neg_smul, neg_neg] + _ = (-r) * orderUnitNorm (-A) := orderUnitNorm_smul_of_pos (neg_pos.mpr hr) (-A) + _ = (-r) * orderUnitNorm A := by rw [orderUnitNorm_neg] + _ = |r| * orderUnitNorm A := by rw [abs_of_neg hr] + · simp + · rw [orderUnitNorm_smul_of_pos hr, abs_of_pos hr] + +/-- Rescaling any nonzero element down to the unit ball: `(orderUnitNorm A)⁻¹ • A` has norm at +most `1`, and scaling it back up by `orderUnitNorm A` recovers `A`. -/ +lemma exists_orderUnitNorm_le_one_smul_eq {A : E} (hA : orderUnitNorm A ≠ 0) : + ∃ B : E, orderUnitNorm B ≤ 1 ∧ orderUnitNorm A • B = A := by + refine ⟨(orderUnitNorm A)⁻¹ • A, ?_, ?_⟩ + · rw [orderUnitNorm_smul, abs_of_nonneg (inv_nonneg.mpr (orderUnitNorm_nonneg A)), + inv_mul_cancel₀ hA] + · rw [smul_smul, mul_inv_cancel₀ hA, one_smul] + +/-! + +## D. The induced normed space + +-/ + +/-- The order-unit norm packaged as an additive-group norm. -/ +noncomputable def orderUnitAddGroupNorm : AddGroupNorm E where + toFun := orderUnitNorm + map_zero' := orderUnitNorm_zero + add_le' := orderUnitNorm_add_le + neg' := orderUnitNorm_neg + eq_zero_of_map_eq_zero' _ hA := orderUnitNorm_eq_zero_iff.mp hA + +/-- The normed additive group induced by the Archimedean order unit. -/ +@[implicit_reducible] +noncomputable def orderUnitNormedAddCommGroup : NormedAddCommGroup E := + orderUnitAddGroupNorm.toNormedAddCommGroup + +/-- The real normed-space structure induced by the Archimedean order unit. -/ +@[implicit_reducible] +noncomputable def orderUnitNormedSpace : + letI : NormedAddCommGroup E := orderUnitNormedAddCommGroup + NormedSpace ℝ E := by + letI : NormedAddCommGroup E := orderUnitNormedAddCommGroup + refine + { ‹Module ℝ E› with + norm_smul_le := ?_ } + intro r A + change orderUnitNorm (r • A) ≤ ‖r‖ * orderUnitNorm A + rw [orderUnitNorm_smul, Real.norm_eq_abs] + +/-! + +## E. Order-closedness of the topology + +-/ + +/-- No sequence of elements that are all `≥ 0` can converge to something negative. -/ +lemma isClosed_Ici_zero : + letI := orderUnitNormedAddCommGroup (E := E) + IsClosed (Set.Ici (0 : E)) := by + let := orderUnitNormedAddCommGroup (E := E) + apply IsSeqClosed.isClosed + intro x p hx hp + apply neg_nonpos.mp + apply le_zero_of_forall_pos_smul_one_le + intro ε hε + obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp hp ε hε + have hnorm : orderUnitNorm (x N - p) < ε := by + have hdist := hN N le_rfl + rwa [dist_eq_norm] at hdist + calc + -p ≤ x N - p := by simpa using sub_le_sub_right (hx N) p + _ ≤ ε • (1 : E) := le_smul_one_of_orderUnitNorm_lt hnorm + +/-- The same holds relative to any reference `a`, not just `0`: +no sequence of elements that are all `≥ a` can converge to something below `a`. -/ +lemma closedIciTopology : + letI := orderUnitNormedAddCommGroup (E := E) + ClosedIciTopology E := by + let := orderUnitNormedAddCommGroup (E := E) + refine ⟨fun a => ?_⟩ + have hEq : Set.Ici a = (fun A : E => A - a) ⁻¹' Set.Ici (0 : E) := by + ext A + simp [Set.mem_Ici] + rw [hEq] + exact isClosed_Ici_zero.preimage (continuous_id.sub continuous_const) + +end IsArchimedeanOrderUnit + +/-! + +## F. A separate copy carrying the order-unit norm + +-/ + +/-- A separate copy of `E` carrying the order-unit norm. `E` itself is left untouched, so this +stays usable even when `E` already carries a different norm for other purposes — e.g. the +self-adjoint matrices already have their operator norm, and this lets the order-unit norm coexist +with it instead of overwriting it. -/ +def WithOrderUnitNorm (E : Type*) := E + +namespace WithOrderUnitNorm + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] + [PosSMulMono ℝ E] [One E] [IsArchimedeanOrderUnit E] + +-- `WithOrderUnitNorm E` is definitionally `E`, so every algebraic and order structure on `E` +-- transfers across unchanged; only the norm below is genuinely new. +instance : AddCommGroup (WithOrderUnitNorm E) := inferInstanceAs (AddCommGroup E) +instance : Module ℝ (WithOrderUnitNorm E) := inferInstanceAs (Module ℝ E) +instance : PartialOrder (WithOrderUnitNorm E) := inferInstanceAs (PartialOrder E) +instance : IsOrderedAddMonoid (WithOrderUnitNorm E) := inferInstanceAs (IsOrderedAddMonoid E) +instance : PosSMulMono ℝ (WithOrderUnitNorm E) := inferInstanceAs (PosSMulMono ℝ E) +instance : One (WithOrderUnitNorm E) := inferInstanceAs (One E) +instance : IsOrderUnit (WithOrderUnitNorm E) := inferInstanceAs (IsOrderUnit E) +instance : IsArchimedeanOrderUnit (WithOrderUnitNorm E) := + inferInstanceAs (IsArchimedeanOrderUnit E) + +/-- The canonical normed additive group on the order-unit-norm copy. -/ +noncomputable instance : NormedAddCommGroup (WithOrderUnitNorm E) := + IsArchimedeanOrderUnit.orderUnitNormedAddCommGroup (E := E) + +/-- The canonical real normed-space structure on the order-unit-norm copy. -/ +noncomputable instance : NormedSpace ℝ (WithOrderUnitNorm E) := + IsArchimedeanOrderUnit.orderUnitNormedSpace (E := E) + +/-- The identity linear equivalence between `E` and its order-unit-norm copy. -/ +def linearEquiv : E ≃ₗ[ℝ] WithOrderUnitNorm E := LinearEquiv.refl ℝ E + +omit [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [One E] [IsArchimedeanOrderUnit E] + in +@[simp] +lemma linearEquiv_apply (A : E) : linearEquiv A = A := rfl + +/-- The norm on the copy is, by construction, exactly the order-unit norm on the original. -/ +@[simp] +lemma norm_eq_orderUnitNorm (A : WithOrderUnitNorm E) : + ‖A‖ = IsArchimedeanOrderUnit.orderUnitNorm (show E from A) := rfl + +end WithOrderUnitNorm diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean b/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean new file mode 100644 index 0000000000..9a1237ade9 --- /dev/null +++ b/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean @@ -0,0 +1,96 @@ +/- +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.Defs + +/-! + +# Order units + +## i. Overview + +Order-unit spaces capture the basic structure needed for a probabilistic theory: observables, +positivity, effects, states, and probabilities. They do this without assuming that the theory is +classical or quantum, or that observables have any particular algebraic structure. + +In quantum mechanics, the standard example is the real vector space of self-adjoint matrices, +ordered by positive semidefiniteness, with the identity matrix as 1. Keeping only the vector +space, its order, and this distinguished unit gives the abstract order-unit setting. + +## ii. Key results + +- `IsOrderUnit.exists_two_sided_bound` : every observable sits between `-(n • 1)` and `n • 1`, for + some `n`. +- `IsOrderUnit.exists_eq_sub_nonneg` : every observable is a difference of two positive + observables. + +## iii. Table of contents + +- A. Order-unit elements +- B. Consequences of being an order unit + +## iv. References + +-/ + +@[expose] public section + +/-! + +## A. Order-unit elements + +-/ + +/-- A positive element `A` is an order unit if every element is bounded above by a natural +multiple of `A`. -/ +def IsOrderUnitElement {E : Type*} [AddCommMonoid E] [PartialOrder E] (A : E) : Prop := + 0 ≤ A ∧ ∀ B : E, ∃ n : ℕ, B ≤ n • A + +/-- The distinguished element `1 : E` is an order unit. No multiplication is assumed. -/ +class IsOrderUnit (E : Type*) [AddCommMonoid E] [PartialOrder E] [One E] : Prop where + /-- `1` itself satisfies the order-unit condition. -/ + isOrderUnitElement_one : IsOrderUnitElement (1 : E) + +namespace IsOrderUnit + +variable {E : Type*} [AddCommMonoid E] [PartialOrder E] [One E] [IsOrderUnit E] + +/-- The distinguished unit is positive. -/ +lemma one_nonneg : 0 ≤ (1 : E) := + IsOrderUnit.isOrderUnitElement_one.1 + +/-- Every element is bounded by some finite multiple of the identity. -/ +lemma exists_nsmul_one_le (A : E) : ∃ n : ℕ, A ≤ n • (1 : E) := + IsOrderUnit.isOrderUnitElement_one.2 A + +/-! + +## B. Consequences of being an order unit + +-/ + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] + [IsOrderUnit E] + +/-- Every element is bounded on both sides by a natural multiple of the order unit. -/ +lemma exists_two_sided_bound (A : E) : ∃ n : ℕ, -(n • (1 : E)) ≤ A ∧ A ≤ n • (1 : E) := by + obtain ⟨n, hn⟩ := IsOrderUnit.exists_nsmul_one_le A + obtain ⟨m, hm⟩ := IsOrderUnit.exists_nsmul_one_le (-A) + refine ⟨max n m, ?_, hn.trans (nsmul_le_nsmul_left IsOrderUnit.one_nonneg (le_max_left n m))⟩ + have hm' : -A ≤ max n m • (1 : E) := + hm.trans (nsmul_le_nsmul_left IsOrderUnit.one_nonneg (le_max_right n m)) + simpa using neg_le_neg hm' + +/-- Every element is a difference of two positive elements. -/ +lemma exists_eq_sub_nonneg (A : E) : + ∃ Ap An : E, 0 ≤ Ap ∧ 0 ≤ An ∧ A = Ap - An := by + obtain ⟨n, hn⟩ := IsOrderUnit.exists_nsmul_one_le (-A) + refine ⟨A + n • (1 : E), n • (1 : E), ?_, nsmul_nonneg IsOrderUnit.one_nonneg n, ?_⟩ + · simpa using add_le_add_right hn A + · exact (add_sub_cancel_right A (n • (1 : E))).symm + +end IsOrderUnit diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean new file mode 100644 index 0000000000..2d44c417b1 --- /dev/null +++ b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean @@ -0,0 +1,109 @@ +/- +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.Geometry.Convex.Cone.Pointed +public import Mathlib.Data.Real.Basic +public import Mathlib.Data.NNReal.Defs +public import Mathlib.Topology.Order.OrderClosed +public import Physlib.ProbabilisticTheory.OrderUnit.Basic + +/-! +# Ordered positive cones + +## i. Overview + +`PosCone E` collects the positive elements of `E`. In quantum mechanics, `E` is the real vector +space of self-adjoint matrices, whose spectra are real. Its positive cone consists exactly of +those matrices whose spectra are nonnegative. +These elements form a cone: they are closed under addition and scaling by nonnegative reals. + +## ii. Key results + +- `PosCone` : the cone of positive observables, `PointedCone.positive ℝ E`. Its carrier is exactly + `{A | 0 ≤ A}` (`PointedCone.mem_positive`) and it is convex (`PointedCone.convex`). +- `PosCone.isClosed` : the positive cone is closed whenever the order itself is topologically + closed. +- `PosCone.nonneg_add_eq_zero` : the positive cone meets its negation only at `0`. +- `PosCone.exists_real_shift_nonneg` : enough copies of the order unit shift any element into the + cone. + +## iii. Table of contents + +- A. The positive cone +- B. Topological closedness +- C. The order unit + +-/ + +@[expose] public section + +open scoped NNReal + +/-! + +## A. The positive cone + +-/ + +/-- The positive pointed cone of an ordered real module. -/ +abbrev PosCone (E : Type*) [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] + [Module ℝ E] [PosSMulMono ℝ E] : PointedCone ℝ E := + PointedCone.positive ℝ E + +namespace PosCone + +variable {E : Type*} [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] + [Module ℝ E] [PosSMulMono ℝ E] + +/-- The positive cone carries a nonnegative-real scalar action. -/ +instance instModule : Module ℝ≥0 (PosCone E) := + inferInstanceAs (Module {c : ℝ // 0 ≤ c} (PointedCone.positive ℝ E)) + +omit [Module ℝ E] [PosSMulMono ℝ E] in +/-- A nonnegative vector that adds with another nonnegative vector to `0` is itself `0`: the +positive cone meets its negation only at `0`. -/ +lemma nonneg_add_eq_zero {A B : E} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A + B = 0) : A = 0 := + le_antisymm (hAB ▸ le_add_of_nonneg_right hB) hA + +/-! + +## B. Topological closedness + +-/ + +variable [TopologicalSpace E] [ClosedIciTopology E] + +/-- The positive cone is closed whenever the order itself is closed in the topology. -/ +lemma isClosed : IsClosed (PosCone E : Set E) := by + simpa [PosCone, PointedCone.mem_positive] using (isClosed_Ici : IsClosed (Set.Ici (0 : E))) + +/-! + +## C. The order unit + +-/ + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] + [PosSMulMono ℝ E] [One E] [IsOrderUnit E] + +/-- The order unit, as a point of the positive cone. -/ +def unit : PosCone E := ⟨1, IsOrderUnit.one_nonneg⟩ + +@[simp] +lemma coe_unit : ((unit : PosCone E) : E) = (1 : E) := rfl + +omit [PosSMulMono ℝ E] in +/-- Every element becomes nonnegative after adding enough copies of the order unit: the positive +cone reaches everywhere, once you're allowed to shift by the unit. -/ +lemma exists_real_shift_nonneg (A : E) : ∃ r : ℝ, 0 ≤ r • (1 : E) + A := by + obtain ⟨n, hn⟩ := IsOrderUnit.exists_nsmul_one_le (-A) + refine ⟨n, ?_⟩ + rw [← Nat.cast_smul_eq_nsmul ℝ n (1 : E)] at hn + rw [← sub_neg_eq_add] + exact sub_nonneg.mpr hn + +end PosCone From 042c65b24b03371588efeed4759662313d2a24ee Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Wed, 23 Sep 2026 21:03:50 +0200 Subject: [PATCH 3/8] fix(ProbabilisticTheory): address order-unit PR review comments - IsOrderUnitElement is now a class with named fields (nonneg, exists_nsmul_le) instead of a def unfolding to an And, per review. - ArchimedeanOrderUnitSpace.closedIciTopology is now an instance (was a lemma) so it's found by typeclass search once the order-unit-norm NormedAddCommGroup is installed locally via letI. Co-Authored-By: Claude Sonnet 5 --- .../OrderUnit/Archimedean.lean | 126 +++++------------- .../ProbabilisticTheory/OrderUnit/Basic.lean | 57 ++++---- .../ProbabilisticTheory/OrderUnit/Cone.lean | 49 ++++--- 3 files changed, 97 insertions(+), 135 deletions(-) diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean index 5386b81bed..add40c81cf 100644 --- a/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean +++ b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean @@ -28,12 +28,13 @@ functional of the order interval `[-1, 1]`: convexity of that interval gives the inequality, and its symmetry gives homogeneity, for free. The Archimedean condition is only needed afterwards, to upgrade this from a seminorm to a genuine norm. -This file develops this norm and packages a copy of `E` carrying it as `WithOrderUnitNorm E`. +This file develops the norm as an explicit function. When a Mathlib result requires typeclass +norms, the corresponding structures are available for local installation. ## ii. Key results -- `IsArchimedeanOrderUnit.orderUnitNorm_eq_zero_iff` : the order-unit norm separates points. -- `IsArchimedeanOrderUnit.closedIciTopology` : the positive cone is closed in the order-unit-norm +- `ArchimedeanOrderUnitSpace.orderUnitNorm_eq_zero_iff` : the order-unit norm separates points. +- `ArchimedeanOrderUnitSpace.closedIciTopology` : the positive cone is closed in the order-unit-norm topology. ## iii. Table of contents @@ -43,7 +44,6 @@ This file develops this norm and packages a copy of `E` carrying it as `WithOrde - C. Norm axioms - D. The induced normed space - E. Order-closedness of the topology -- F. A separate copy carrying the order-unit norm ## iv. References @@ -57,15 +57,13 @@ This file develops this norm and packages a copy of `E` carrying it as `WithOrde -/ -/-- The distinguished element `1` is an Archimedean order unit. -/ -class IsArchimedeanOrderUnit (E : Type*) [AddCommGroup E] [PartialOrder E] [Module ℝ E] [One E] : - Prop extends IsOrderUnit E where - /-- If `A` is smaller than every positive multiple of `1`, however small, `A` is already - `≤ 0`. -/ +/-- An order-unit space whose distinguished order unit is Archimedean. -/ +class ArchimedeanOrderUnitSpace (E : Type*) extends OrderUnitSpace E where + /-- If `A` is smaller than every positive multiple of `1`, `A` is already `≤ 0`. -/ le_zero_of_forall_pos_smul_one_le : ∀ A : E, (∀ ε : ℝ, 0 < ε → A ≤ ε • (1 : E)) → A ≤ 0 /-- The real numbers form an Archimedean order-unit space. -/ -instance instIsArchimedeanOrderUnitReal : IsArchimedeanOrderUnit ℝ where +instance instArchimedeanOrderUnitSpaceReal : ArchimedeanOrderUnitSpace ℝ where isOrderUnitElement_one := ⟨zero_le_one, fun A => by obtain ⟨n, hn⟩ := exists_nat_ge A exact ⟨n, by simpa using hn⟩⟩ @@ -76,10 +74,11 @@ instance instIsArchimedeanOrderUnitReal : IsArchimedeanOrderUnit ℝ where simp only [smul_eq_mul, mul_one] at this linarith -namespace IsArchimedeanOrderUnit +namespace ArchimedeanOrderUnitSpace -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] - [One E] [IsArchimedeanOrderUnit E] +section OrderUnitSpace + +variable {E : Type*} [OrderUnitSpace E] /-! @@ -95,36 +94,33 @@ def orderUnitBounds (A : E) : Set ℝ := noncomputable def orderUnitNorm (A : E) : ℝ := sInf (orderUnitBounds A) -/-- Every element has some order-unit bound: this is just `IsOrderUnit`'s two-sided bound, +/-- The order-unit bounds are bounded below by `0`, so their infimum (the norm) is well-behaved. -/ +lemma orderUnitBounds_bddBelow (A : E) : BddBelow (orderUnitBounds A) := + ⟨0, fun _ hr ↦ hr.1⟩ + +/-- Any order-unit bound on `A` is an upper bound for `A`'s order-unit norm. -/ +lemma orderUnitNorm_le {A : E} {r : ℝ} (hr : r ∈ orderUnitBounds A) : + orderUnitNorm A ≤ r := + csInf_le (orderUnitBounds_bddBelow A) hr + +/-- Every element has some order-unit bound: this is just `OrderUnitSpace`'s two-sided bound, repackaged as a natural number in `orderUnitBounds`. -/ lemma orderUnitBounds_nonempty (A : E) : (orderUnitBounds A).Nonempty := by - obtain ⟨n, hl, hu⟩ := IsOrderUnit.exists_two_sided_bound A + obtain ⟨n, hl, hu⟩ := OrderUnitSpace.exists_two_sided_bound A refine ⟨n, Nat.cast_nonneg n, ?_, ?_⟩ · simpa only [Nat.cast_smul_eq_nsmul] using hl · simpa only [Nat.cast_smul_eq_nsmul] using hu -omit [IsOrderedAddMonoid E] [IsArchimedeanOrderUnit E] in -/-- The order-unit bounds are bounded below by `0`, so their infimum (the norm) is well-behaved. -/ -lemma orderUnitBounds_bddBelow (A : E) : BddBelow (orderUnitBounds A) := - ⟨0, fun _ hr ↦ hr.1⟩ - /-- The order-unit norm is an infimum of nonnegative reals, hence itself nonnegative. -/ lemma orderUnitNorm_nonneg (A : E) : 0 ≤ orderUnitNorm A := le_csInf (orderUnitBounds_nonempty A) fun _ hr ↦ hr.1 -omit [IsOrderedAddMonoid E] [IsArchimedeanOrderUnit E] in -/-- Any order-unit bound on `A` is an upper bound for `A`'s order-unit norm. -/ -lemma orderUnitNorm_le {A : E} {r : ℝ} (hr : r ∈ orderUnitBounds A) : - orderUnitNorm A ≤ r := - csInf_le (orderUnitBounds_bddBelow A) hr - @[simp] lemma orderUnitNorm_zero : orderUnitNorm (0 : E) = 0 := by apply le_antisymm · exact orderUnitNorm_le ⟨le_rfl, by simp, by simp⟩ · exact orderUnitNorm_nonneg 0 -omit [IsArchimedeanOrderUnit E] in /-- Negation preserves the set of order-unit bounds: a symmetric interval bounding `A` bounds `-A` too. -/ lemma orderUnitBounds_neg (A : E) : orderUnitBounds (-A) = orderUnitBounds A := by @@ -133,13 +129,11 @@ lemma orderUnitBounds_neg (A : E) : orderUnitBounds (-A) = orderUnitBounds A := exact ⟨hr, by simpa only [neg_neg] using neg_le_neg hu, by simpa only [neg_smul, neg_neg] using neg_le_neg hl⟩ -omit [IsArchimedeanOrderUnit E] in @[simp] lemma orderUnitNorm_neg (A : E) : orderUnitNorm (-A) = orderUnitNorm A := by unfold orderUnitNorm rw [orderUnitBounds_neg] -omit [IsArchimedeanOrderUnit E] in /-- Order-unit bounds add: a bound for `A` and a bound for `B` combine to a bound for `A + B`, which is what drives the triangle inequality for `orderUnitNorm`. -/ lemma add_mem_orderUnitBounds {A B : E} {r s : ℝ} (hr : r ∈ orderUnitBounds A) @@ -150,6 +144,10 @@ lemma add_mem_orderUnitBounds {A B : E} {r s : ℝ} (hr : r ∈ orderUnitBounds · rw [add_smul] exact add_le_add hr.2.2 hs.2.2 +end OrderUnitSpace + +variable {E : Type*} [ArchimedeanOrderUnitSpace E] + /-- An infimum can always be approximated from above: there is an order-unit bound on `A` within `ε` of the norm itself. -/ lemma exists_orderUnitBound_lt (A : E) {ε : ℝ} (hε : 0 < ε) : @@ -175,14 +173,12 @@ lemma orderUnitNorm_add_le (A B : E) : -/ -variable [PosSMulMono ℝ E] - /-- Scaling the unit by a larger nonnegative real gives a larger multiple: `r ↦ r • 1` is monotone. -/ lemma smul_one_mono {r s : ℝ} (hrs : r ≤ s) : r • (1 : E) ≤ s • (1 : E) := by have h : 0 ≤ (s - r) • (1 : E) := - smul_nonneg (sub_nonneg.mpr hrs) IsOrderUnit.one_nonneg + smul_nonneg (sub_nonneg.mpr hrs) OrderUnitSpace.one_nonneg calc r • (1 : E) = s • (1 : E) - (s - r) • (1 : E) := by rw [← sub_smul, sub_sub_cancel] @@ -315,16 +311,19 @@ noncomputable def orderUnitAddGroupNorm : AddGroupNorm E where /-- The normed additive group induced by the Archimedean order unit. -/ @[implicit_reducible] noncomputable def orderUnitNormedAddCommGroup : NormedAddCommGroup E := - orderUnitAddGroupNorm.toNormedAddCommGroup + let normed := orderUnitAddGroupNorm.toNormedAddCommGroup + { normed with toAddCommGroup := inferInstance } /-- The real normed-space structure induced by the Archimedean order unit. -/ @[implicit_reducible] noncomputable def orderUnitNormedSpace : letI : NormedAddCommGroup E := orderUnitNormedAddCommGroup NormedSpace ℝ E := by + let module : Module ℝ E := inferInstance letI : NormedAddCommGroup E := orderUnitNormedAddCommGroup + letI : Module ℝ E := module refine - { ‹Module ℝ E› with + { module with norm_smul_le := ?_ } intro r A change orderUnitNorm (r • A) ≤ ‖r‖ * orderUnitNorm A @@ -354,9 +353,8 @@ lemma isClosed_Ici_zero : -p ≤ x N - p := by simpa using sub_le_sub_right (hx N) p _ ≤ ε • (1 : E) := le_smul_one_of_orderUnitNorm_lt hnorm -/-- The same holds relative to any reference `a`, not just `0`: -no sequence of elements that are all `≥ a` can converge to something below `a`. -/ -lemma closedIciTopology : +/-- The same holds relative to any reference `a`, not just `0`. -/ +instance closedIciTopology : letI := orderUnitNormedAddCommGroup (E := E) ClosedIciTopology E := by let := orderUnitNormedAddCommGroup (E := E) @@ -367,56 +365,4 @@ lemma closedIciTopology : rw [hEq] exact isClosed_Ici_zero.preimage (continuous_id.sub continuous_const) -end IsArchimedeanOrderUnit - -/-! - -## F. A separate copy carrying the order-unit norm - --/ - -/-- A separate copy of `E` carrying the order-unit norm. `E` itself is left untouched, so this -stays usable even when `E` already carries a different norm for other purposes — e.g. the -self-adjoint matrices already have their operator norm, and this lets the order-unit norm coexist -with it instead of overwriting it. -/ -def WithOrderUnitNorm (E : Type*) := E - -namespace WithOrderUnitNorm - -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] - [PosSMulMono ℝ E] [One E] [IsArchimedeanOrderUnit E] - --- `WithOrderUnitNorm E` is definitionally `E`, so every algebraic and order structure on `E` --- transfers across unchanged; only the norm below is genuinely new. -instance : AddCommGroup (WithOrderUnitNorm E) := inferInstanceAs (AddCommGroup E) -instance : Module ℝ (WithOrderUnitNorm E) := inferInstanceAs (Module ℝ E) -instance : PartialOrder (WithOrderUnitNorm E) := inferInstanceAs (PartialOrder E) -instance : IsOrderedAddMonoid (WithOrderUnitNorm E) := inferInstanceAs (IsOrderedAddMonoid E) -instance : PosSMulMono ℝ (WithOrderUnitNorm E) := inferInstanceAs (PosSMulMono ℝ E) -instance : One (WithOrderUnitNorm E) := inferInstanceAs (One E) -instance : IsOrderUnit (WithOrderUnitNorm E) := inferInstanceAs (IsOrderUnit E) -instance : IsArchimedeanOrderUnit (WithOrderUnitNorm E) := - inferInstanceAs (IsArchimedeanOrderUnit E) - -/-- The canonical normed additive group on the order-unit-norm copy. -/ -noncomputable instance : NormedAddCommGroup (WithOrderUnitNorm E) := - IsArchimedeanOrderUnit.orderUnitNormedAddCommGroup (E := E) - -/-- The canonical real normed-space structure on the order-unit-norm copy. -/ -noncomputable instance : NormedSpace ℝ (WithOrderUnitNorm E) := - IsArchimedeanOrderUnit.orderUnitNormedSpace (E := E) - -/-- The identity linear equivalence between `E` and its order-unit-norm copy. -/ -def linearEquiv : E ≃ₗ[ℝ] WithOrderUnitNorm E := LinearEquiv.refl ℝ E - -omit [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [One E] [IsArchimedeanOrderUnit E] - in -@[simp] -lemma linearEquiv_apply (A : E) : linearEquiv A = A := rfl - -/-- The norm on the copy is, by construction, exactly the order-unit norm on the original. -/ -@[simp] -lemma norm_eq_orderUnitNorm (A : WithOrderUnitNorm E) : - ‖A‖ = IsArchimedeanOrderUnit.orderUnitNorm (show E from A) := rfl - -end WithOrderUnitNorm +end ArchimedeanOrderUnitSpace diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean b/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean index 9a1237ade9..7065aa7189 100644 --- a/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean +++ b/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean @@ -6,15 +6,16 @@ Authors: Tom Ole Diem module public import Mathlib.Algebra.Order.Module.Defs +public import Mathlib.Data.Real.Basic /-! -# Order units +# Ordered vector spaces and order units ## i. Overview Order-unit spaces capture the basic structure needed for a probabilistic theory: observables, -positivity, effects, states, and probabilities. They do this without assuming that the theory is +positivity, effects, states and probabilities. They do this without assuming that the theory is classical or quantum, or that observables have any particular algebraic structure. In quantum mechanics, the standard example is the real vector space of self-adjoint matrices, @@ -23,9 +24,9 @@ space, its order, and this distinguished unit gives the abstract order-unit sett ## ii. Key results -- `IsOrderUnit.exists_two_sided_bound` : every observable sits between `-(n • 1)` and `n • 1`, for - some `n`. -- `IsOrderUnit.exists_eq_sub_nonneg` : every observable is a difference of two positive +- `OrderUnitSpace.exists_two_sided_bound` : every observable sits between `-(n • 1)` and `n • 1`, + for some `n`. +- `OrderUnitSpace.exists_eq_sub_nonneg` : every observable is a difference of two positive observables. ## iii. Table of contents @@ -41,31 +42,39 @@ space, its order, and this distinguished unit gives the abstract order-unit sett /-! -## A. Order-unit elements +## A. Ordered vector spaces and order-unit elements -/ +/-- An ordered real vector space. -/ +class OrderedVectorSpace (E : Type*) extends AddCommGroup E, PartialOrder E, Module ℝ E, + IsOrderedAddMonoid E, PosSMulMono ℝ E + /-- A positive element `A` is an order unit if every element is bounded above by a natural multiple of `A`. -/ -def IsOrderUnitElement {E : Type*} [AddCommMonoid E] [PartialOrder E] (A : E) : Prop := - 0 ≤ A ∧ ∀ B : E, ∃ n : ℕ, B ≤ n • A - -/-- The distinguished element `1 : E` is an order unit. No multiplication is assumed. -/ -class IsOrderUnit (E : Type*) [AddCommMonoid E] [PartialOrder E] [One E] : Prop where +class IsOrderUnitElement {E : Type*} [AddCommMonoid E] [PartialOrder E] (A : E) : Prop where + /-- An order-unit element is nonnegative. -/ + nonneg : 0 ≤ A + /-- Every element is bounded above by a natural multiple of the order unit. -/ + exists_nsmul_le : ∀ B : E, ∃ n : ℕ, B ≤ n • A + +/-- An ordered real vector space whose distinguished element `1` is an order unit. No +multiplication is assumed. -/ +class OrderUnitSpace (E : Type*) extends OrderedVectorSpace E, One E where /-- `1` itself satisfies the order-unit condition. -/ isOrderUnitElement_one : IsOrderUnitElement (1 : E) -namespace IsOrderUnit +namespace OrderUnitSpace -variable {E : Type*} [AddCommMonoid E] [PartialOrder E] [One E] [IsOrderUnit E] +variable {E : Type*} [OrderUnitSpace E] /-- The distinguished unit is positive. -/ lemma one_nonneg : 0 ≤ (1 : E) := - IsOrderUnit.isOrderUnitElement_one.1 + OrderUnitSpace.isOrderUnitElement_one.nonneg /-- Every element is bounded by some finite multiple of the identity. -/ lemma exists_nsmul_one_le (A : E) : ∃ n : ℕ, A ≤ n • (1 : E) := - IsOrderUnit.isOrderUnitElement_one.2 A + OrderUnitSpace.isOrderUnitElement_one.exists_nsmul_le A /-! @@ -73,24 +82,22 @@ lemma exists_nsmul_one_le (A : E) : ∃ n : ℕ, A ≤ n • (1 : E) := -/ -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] - [IsOrderUnit E] - /-- Every element is bounded on both sides by a natural multiple of the order unit. -/ lemma exists_two_sided_bound (A : E) : ∃ n : ℕ, -(n • (1 : E)) ≤ A ∧ A ≤ n • (1 : E) := by - obtain ⟨n, hn⟩ := IsOrderUnit.exists_nsmul_one_le A - obtain ⟨m, hm⟩ := IsOrderUnit.exists_nsmul_one_le (-A) - refine ⟨max n m, ?_, hn.trans (nsmul_le_nsmul_left IsOrderUnit.one_nonneg (le_max_left n m))⟩ + obtain ⟨n, hn⟩ := OrderUnitSpace.exists_nsmul_one_le A + obtain ⟨m, hm⟩ := OrderUnitSpace.exists_nsmul_one_le (-A) + refine ⟨max n m, ?_, + hn.trans (nsmul_le_nsmul_left OrderUnitSpace.one_nonneg (le_max_left n m))⟩ have hm' : -A ≤ max n m • (1 : E) := - hm.trans (nsmul_le_nsmul_left IsOrderUnit.one_nonneg (le_max_right n m)) + hm.trans (nsmul_le_nsmul_left OrderUnitSpace.one_nonneg (le_max_right n m)) simpa using neg_le_neg hm' /-- Every element is a difference of two positive elements. -/ lemma exists_eq_sub_nonneg (A : E) : ∃ Ap An : E, 0 ≤ Ap ∧ 0 ≤ An ∧ A = Ap - An := by - obtain ⟨n, hn⟩ := IsOrderUnit.exists_nsmul_one_le (-A) - refine ⟨A + n • (1 : E), n • (1 : E), ?_, nsmul_nonneg IsOrderUnit.one_nonneg n, ?_⟩ + obtain ⟨n, hn⟩ := OrderUnitSpace.exists_nsmul_one_le (-A) + refine ⟨A + n • (1 : E), n • (1 : E), ?_, nsmul_nonneg OrderUnitSpace.one_nonneg n, ?_⟩ · simpa using add_le_add_right hn A · exact (add_sub_cancel_right A (n • (1 : E))).symm -end IsOrderUnit +end OrderUnitSpace diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean index 2d44c417b1..01799047e2 100644 --- a/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean +++ b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean @@ -8,8 +8,7 @@ module public import Mathlib.Geometry.Convex.Cone.Pointed public import Mathlib.Data.Real.Basic public import Mathlib.Data.NNReal.Defs -public import Mathlib.Topology.Order.OrderClosed -public import Physlib.ProbabilisticTheory.OrderUnit.Basic +public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean /-! # Ordered positive cones @@ -25,8 +24,8 @@ These elements form a cone: they are closed under addition and scaling by nonneg - `PosCone` : the cone of positive observables, `PointedCone.positive ℝ E`. Its carrier is exactly `{A | 0 ≤ A}` (`PointedCone.mem_positive`) and it is convex (`PointedCone.convex`). -- `PosCone.isClosed` : the positive cone is closed whenever the order itself is topologically - closed. +- `PosCone.isClosed` : the positive cone is closed in the order-unit-norm topology of an + Archimedean order-unit space. - `PosCone.nonneg_add_eq_zero` : the positive cone meets its negation only at `0`. - `PosCone.exists_real_shift_nonneg` : enough copies of the order unit shift any element into the cone. @@ -50,36 +49,44 @@ open scoped NNReal -/ /-- The positive pointed cone of an ordered real module. -/ -abbrev PosCone (E : Type*) [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] - [Module ℝ E] [PosSMulMono ℝ E] : PointedCone ℝ E := +abbrev PosCone (E : Type*) [OrderedVectorSpace E] : PointedCone ℝ E := PointedCone.positive ℝ E namespace PosCone -variable {E : Type*} [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] - [Module ℝ E] [PosSMulMono ℝ E] +section OrderedVectorSpace + +variable {E : Type*} [OrderedVectorSpace E] /-- The positive cone carries a nonnegative-real scalar action. -/ instance instModule : Module ℝ≥0 (PosCone E) := inferInstanceAs (Module {c : ℝ // 0 ≤ c} (PointedCone.positive ℝ E)) -omit [Module ℝ E] [PosSMulMono ℝ E] in /-- A nonnegative vector that adds with another nonnegative vector to `0` is itself `0`: the positive cone meets its negation only at `0`. -/ lemma nonneg_add_eq_zero {A B : E} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A + B = 0) : A = 0 := le_antisymm (hAB ▸ le_add_of_nonneg_right hB) hA +end OrderedVectorSpace + /-! ## B. Topological closedness -/ -variable [TopologicalSpace E] [ClosedIciTopology E] +section ArchimedeanOrderUnitSpace + +variable {E : Type*} [ArchimedeanOrderUnitSpace E] -/-- The positive cone is closed whenever the order itself is closed in the topology. -/ -lemma isClosed : IsClosed (PosCone E : Set E) := by - simpa [PosCone, PointedCone.mem_positive] using (isClosed_Ici : IsClosed (Set.Ici (0 : E))) +/-- The positive cone is closed in the topology induced by the order-unit norm. -/ +lemma isClosed : + letI := ArchimedeanOrderUnitSpace.orderUnitNormedAddCommGroup (E := E) + IsClosed (PosCone E : Set E) := by + simpa [PosCone, PointedCone.mem_positive] using + (ArchimedeanOrderUnitSpace.isClosed_Ici_zero (E := E)) + +end ArchimedeanOrderUnitSpace /-! @@ -87,23 +94,25 @@ lemma isClosed : IsClosed (PosCone E : Set E) := by -/ -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] - [PosSMulMono ℝ E] [One E] [IsOrderUnit E] +section OrderUnitSpace + +variable {E : Type*} [OrderUnitSpace E] -/-- The order unit, as a point of the positive cone. -/ -def unit : PosCone E := ⟨1, IsOrderUnit.one_nonneg⟩ +/-- The order unit, regarded as a point of the positive cone. -/ +instance instOne : One (PosCone E) := ⟨⟨1, OrderUnitSpace.one_nonneg⟩⟩ @[simp] -lemma coe_unit : ((unit : PosCone E) : E) = (1 : E) := rfl +lemma coe_one : ((1 : PosCone E) : E) = (1 : E) := rfl -omit [PosSMulMono ℝ E] in /-- Every element becomes nonnegative after adding enough copies of the order unit: the positive cone reaches everywhere, once you're allowed to shift by the unit. -/ lemma exists_real_shift_nonneg (A : E) : ∃ r : ℝ, 0 ≤ r • (1 : E) + A := by - obtain ⟨n, hn⟩ := IsOrderUnit.exists_nsmul_one_le (-A) + obtain ⟨n, hn⟩ := OrderUnitSpace.exists_nsmul_one_le (-A) refine ⟨n, ?_⟩ rw [← Nat.cast_smul_eq_nsmul ℝ n (1 : E)] at hn rw [← sub_neg_eq_add] exact sub_nonneg.mpr hn +end OrderUnitSpace + end PosCone From 018ab986aa4f93fb2063de3cb375ee09cd68cefb Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Sun, 20 Sep 2026 22:40:53 +0200 Subject: [PATCH 4/8] feat(ProbabilisticTheory): effects Adds effects (Effect/Basic.lean, the sub-unit interval of E), their convex/affine structure and metric (Effect/Convex.lean, Effect/Metric.lean), complementation (Effect/Complement.lean), and sharp effects (Effect/Sharp.lean), building on the order-unit foundation from #1667. Co-Authored-By: Claude Sonnet 5 --- Physlib.lean | 5 + Physlib/ProbabilisticTheory/Effect/Basic.lean | 80 +++++++++++++ .../Effect/Complement.lean | 106 +++++++++++++++++ .../ProbabilisticTheory/Effect/Convex.lean | 57 +++++++++ .../ProbabilisticTheory/Effect/Metric.lean | 110 ++++++++++++++++++ Physlib/ProbabilisticTheory/Effect/Sharp.lean | 89 ++++++++++++++ 6 files changed, 447 insertions(+) create mode 100644 Physlib/ProbabilisticTheory/Effect/Basic.lean create mode 100644 Physlib/ProbabilisticTheory/Effect/Complement.lean create mode 100644 Physlib/ProbabilisticTheory/Effect/Convex.lean create mode 100644 Physlib/ProbabilisticTheory/Effect/Metric.lean create mode 100644 Physlib/ProbabilisticTheory/Effect/Sharp.lean diff --git a/Physlib.lean b/Physlib.lean index 623cfc1443..1f6859188b 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -254,6 +254,11 @@ 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 diff --git a/Physlib/ProbabilisticTheory/Effect/Basic.lean b/Physlib/ProbabilisticTheory/Effect/Basic.lean new file mode 100644 index 0000000000..f8f6fa849b --- /dev/null +++ b/Physlib/ProbabilisticTheory/Effect/Basic.lean @@ -0,0 +1,80 @@ +/- +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. + + +-/ + +@[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*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] + [Module ℝ E] [PosSMulMono ℝ 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] + +variable [IsOrderUnit 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⟩ := IsOrderUnit.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) IsOrderUnit.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 diff --git a/Physlib/ProbabilisticTheory/Effect/Complement.lean b/Physlib/ProbabilisticTheory/Effect/Complement.lean new file mode 100644 index 0000000000..394345b866 --- /dev/null +++ b/Physlib/ProbabilisticTheory/Effect/Complement.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.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*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid 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] + +variable [IsOrderUnit E] + +instance : Zero (Effect E) := ⟨0, le_refl 0, IsOrderUnit.one_nonneg⟩ +instance : One (Effect E) := ⟨1, IsOrderUnit.one_nonneg, le_refl 1⟩ +instance : Nonempty (Effect E) := ⟨0⟩ + +omit [IsOrderedAddMonoid E] in +@[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl + +omit [IsOrderedAddMonoid E] in +@[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] + +/-! + +## B. Monotonicity of the complement + +-/ + +omit [IsOrderUnit E] in +/-- 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 + +variable [Module ℝ E] [PosSMulMono ℝ E] + +/-! + +## C. The complement and mixtures + +-/ + +omit [IsOrderUnit E] in +/-- 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 diff --git a/Physlib/ProbabilisticTheory/Effect/Convex.lean b/Physlib/ProbabilisticTheory/Effect/Convex.lean new file mode 100644 index 0000000000..60ef4e3f0e --- /dev/null +++ b/Physlib/ProbabilisticTheory/Effect/Convex.lean @@ -0,0 +1,57 @@ +/- +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*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] + [Module ℝ E] [PosSMulMono ℝ 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 diff --git a/Physlib/ProbabilisticTheory/Effect/Metric.lean b/Physlib/ProbabilisticTheory/Effect/Metric.lean new file mode 100644 index 0000000000..c65e0f14e7 --- /dev/null +++ b/Physlib/ProbabilisticTheory/Effect/Metric.lean @@ -0,0 +1,110 @@ +/- +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 +(`equivBall`). + +## 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 IsArchimedeanOrderUnit + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] + [PosSMulMono ℝ E] [One E] [IsArchimedeanOrderUnit 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 + +omit [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [IsArchimedeanOrderUnit E] in +/-- 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 + +omit [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [IsArchimedeanOrderUnit E] in +/-- 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 diff --git a/Physlib/ProbabilisticTheory/Effect/Sharp.lean b/Physlib/ProbabilisticTheory/Effect/Sharp.lean new file mode 100644 index 0000000000..7ce70ff1e3 --- /dev/null +++ b/Physlib/ProbabilisticTheory/Effect/Sharp.lean @@ -0,0 +1,89 @@ +/- +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.Complement +public import Physlib.ProbabilisticTheory.Effect.Convex +public import Mathlib.Analysis.Convex.Strict.Extreme + +/-! +# Sharp effects + +## i. Overview + +The effect interval `[0, 1]` is convex. A sharp effect is an extreme point of it: one that cannot +be written as a nontrivial mixture of two distinct effects. Sharp effects generalize projections. + +## ii. Key results + +- `Effect.IsSharp` : an effect that cannot be written as a nontrivial mixture of two distinct + effects. +- `Effect.isSharp_complement_iff` : sharpness is preserved by taking the complement. + +## iii. Table of contents + +- A. Sharp effects + +-/ + +@[expose] public section + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] + [Module ℝ E] [PosSMulMono ℝ E] + +namespace Effect + +variable [IsOrderUnit E] + +/-! + +## A. Sharp effects + +-/ + +/-- An effect is sharp when it is an extreme point of the effect interval: it cannot be written as +a nontrivial mixture of two distinct effects. -/ +def IsSharp (e : Effect E) : Prop := (e : E) ∈ Set.extremePoints ℝ (Set.Icc (0 : E) 1) + +/-- The impossible outcome 0 is sharp. -/ +lemma isSharp_zero : IsSharp (0 : Effect E) := by + refine ⟨⟨le_refl 0, IsOrderUnit.one_nonneg⟩, + fun x₁ hx₁ _ hx₂ ⟨a, b, ha, hb, _, hz⟩ => ?_⟩ + have hax : a • x₁ = 0 := + PosCone.nonneg_add_eq_zero + (smul_nonneg ha.le hx₁.1) (smul_nonneg hb.le hx₂.1) (by simpa using hz) + have := congrArg (a⁻¹ • ·) hax + rwa [inv_smul_smul₀ ha.ne', smul_zero] at this + +omit [PosSMulMono ℝ E] [IsOrderUnit E] in +/-- Sharpness is preserved by taking the complement: +`e ↦ 1 - e` is an affine involution of the effect interval. -/ +lemma isSharp_complement {e : Effect E} (h : IsSharp e) : IsSharp (complement e) := by + refine ⟨(complement e).2, fun x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hz⟩ => ?_⟩ + have hone : a • (1 : E) + b • (1 : E) = 1 := by rw [← add_smul, hab, one_smul] + have key : a • (1 - x₁) + b • (1 - x₂) = (e : E) := by + have hsplit : a • (1 - x₁) + b • (1 - x₂) = + (a • (1 : E) + b • (1 : E)) - (a • x₁ + b • x₂) := by + simp only [smul_sub]; abel + rw [hsplit, hone, hz] + show (1 : E) - (1 - (e : E)) = (e : E) + abel + have x1eq := (mem_extremePoints_iff_left.mp h).2 (1 - x₁) + ⟨sub_nonneg.mpr hx₁.2, sub_le_self 1 hx₁.1⟩ (1 - x₂) + ⟨sub_nonneg.mpr hx₂.2, sub_le_self 1 hx₂.1⟩ ⟨a, b, ha, hb, hab, key⟩ + have hsum : x₁ + (e : E) = 1 := by rw [← x1eq]; abel + exact eq_sub_of_add_eq hsum + +omit [PosSMulMono ℝ E] [IsOrderUnit E] in +/-- Sharpness is preserved by taking the complement, in either direction. -/ +lemma isSharp_complement_iff {e : Effect E} : IsSharp (complement e) ↔ IsSharp e := + ⟨fun h => complement_complement e ▸ isSharp_complement h, isSharp_complement⟩ + +/-- The certain outcome 1 is sharp. -/ +lemma isSharp_one : IsSharp (1 : Effect E) := + complement_zero (E := E) ▸ isSharp_complement isSharp_zero + +end Effect From 27359a7812f7c5efd35628877e19806e8740d238 Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Sun, 20 Sep 2026 23:21:45 +0200 Subject: [PATCH 5/8] fix(ProbabilisticTheory): drop inline lemma citation from Effect.Metric overview Co-Authored-By: Claude Sonnet 5 --- Physlib/ProbabilisticTheory/Effect/Metric.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Physlib/ProbabilisticTheory/Effect/Metric.lean b/Physlib/ProbabilisticTheory/Effect/Metric.lean index c65e0f14e7..1a61d6b7d7 100644 --- a/Physlib/ProbabilisticTheory/Effect/Metric.lean +++ b/Physlib/ProbabilisticTheory/Effect/Metric.lean @@ -18,8 +18,7 @@ Effects sit inside `E`, so pulling back the order-unit norm along the inclusion 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 -(`equivBall`). +`e ↦ 2 • e - 1` that turns `[0, 1]` into the symmetric `[-1, 1]` the norm itself ranges over. ## ii. Key results From 13a2e081396bd0c81010b02a84e4380a58dd001f Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Wed, 23 Sep 2026 21:15:31 +0200 Subject: [PATCH 6/8] fix(ProbabilisticTheory): update Effect files for the OrderUnitSpace API Effect/{Basic,Complement,Convex,Metric,Sharp}.lean used the granular pre-review typeclass bundle (AddCommGroup + PartialOrder + IsOrderedAddMonoid + Module + PosSMulMono + One + IsOrderUnit) and the old IsOrderUnit/IsArchimedeanOrderUnit names. Switch to the merged OrderedVectorSpace/OrderUnitSpace/ArchimedeanOrderUnitSpace classes, dropping the omit-tag dance that the granular version needed. Co-Authored-By: Claude Sonnet 5 --- Physlib/ProbabilisticTheory/Effect/Basic.lean | 17 +++++--- .../Effect/Complement.lean | 42 ++++++++++--------- .../ProbabilisticTheory/Effect/Convex.lean | 3 +- .../ProbabilisticTheory/Effect/Metric.lean | 7 +--- Physlib/ProbabilisticTheory/Effect/Sharp.lean | 19 +++++---- 5 files changed, 49 insertions(+), 39 deletions(-) diff --git a/Physlib/ProbabilisticTheory/Effect/Basic.lean b/Physlib/ProbabilisticTheory/Effect/Basic.lean index f8f6fa849b..1ca3d35bb3 100644 --- a/Physlib/ProbabilisticTheory/Effect/Basic.lean +++ b/Physlib/ProbabilisticTheory/Effect/Basic.lean @@ -51,21 +51,26 @@ abbrev Effect (E : Type*) [PartialOrder E] [One E] [Zero E] := Set.Icc (0 : E) 1 namespace Effect -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] - [Module ℝ E] [PosSMulMono ℝ E] [One E] +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] -variable [IsOrderUnit E] +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⟩ := IsOrderUnit.exists_nsmul_one_le B + 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) := @@ -73,8 +78,10 @@ lemma exists_pos_smul_mem {B : E} (hB : 0 ≤ B) : 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) IsOrderUnit.one_nonneg + 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 diff --git a/Physlib/ProbabilisticTheory/Effect/Complement.lean b/Physlib/ProbabilisticTheory/Effect/Complement.lean index 394345b866..10d8491b36 100644 --- a/Physlib/ProbabilisticTheory/Effect/Complement.lean +++ b/Physlib/ProbabilisticTheory/Effect/Complement.lean @@ -36,7 +36,9 @@ Physically, a state's probability of "no" is always `1` minus its probability of namespace Effect -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] +section OrderedVectorSpace + +variable {E : Type*} [OrderedVectorSpace E] [One E] /-! @@ -53,16 +55,28 @@ lemma complement_complement (e : Effect E) : complement (complement e) = e := by apply Subtype.ext simp [complement] -variable [IsOrderUnit E] +/-! + +## 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, IsOrderUnit.one_nonneg⟩ -instance : One (Effect E) := ⟨1, IsOrderUnit.one_nonneg, le_refl 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⟩ -omit [IsOrderedAddMonoid E] in @[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl -omit [IsOrderedAddMonoid E] in @[simp] lemma coe_one : ((1 : Effect E) : E) = 1 := rfl @[simp] @@ -77,24 +91,10 @@ lemma complement_one : complement (1 : Effect E) = 0 := by /-! -## B. Monotonicity of the complement - --/ - -omit [IsOrderUnit E] in -/-- 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 - -variable [Module ℝ E] [PosSMulMono ℝ E] - -/-! - ## C. The complement and mixtures -/ -omit [IsOrderUnit E] in /-- 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 @@ -103,4 +103,6 @@ lemma complement_mix (e f : Effect E) (t : unitInterval) : = (t : ℝ) • ((1 : E) - (e : E)) + (1 - (t : ℝ)) • ((1 : E) - (f : E)) module +end OrderUnitSpace + end Effect diff --git a/Physlib/ProbabilisticTheory/Effect/Convex.lean b/Physlib/ProbabilisticTheory/Effect/Convex.lean index 60ef4e3f0e..55a106ff64 100644 --- a/Physlib/ProbabilisticTheory/Effect/Convex.lean +++ b/Physlib/ProbabilisticTheory/Effect/Convex.lean @@ -30,8 +30,7 @@ actually run is itself a legitimate measurement. @[expose] public section -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] - [Module ℝ E] [PosSMulMono ℝ E] +variable {E : Type*} [OrderedVectorSpace E] [One E] namespace Effect diff --git a/Physlib/ProbabilisticTheory/Effect/Metric.lean b/Physlib/ProbabilisticTheory/Effect/Metric.lean index 1a61d6b7d7..86e24cb88a 100644 --- a/Physlib/ProbabilisticTheory/Effect/Metric.lean +++ b/Physlib/ProbabilisticTheory/Effect/Metric.lean @@ -34,10 +34,9 @@ Effects also correspond to points of the order-unit-norm ball, by the affine res @[expose] public section -open IsArchimedeanOrderUnit +open ArchimedeanOrderUnitSpace -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module ℝ E] - [PosSMulMono ℝ E] [One E] [IsArchimedeanOrderUnit E] +variable {E : Type*} [ArchimedeanOrderUnitSpace E] namespace Effect @@ -86,12 +85,10 @@ lemma mem_effect_two_inv_smul_one_add (A : {A : E // orderUnitNorm A ≤ 1}) : 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 -omit [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [IsArchimedeanOrderUnit E] in /-- 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 -omit [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [IsArchimedeanOrderUnit E] in /-- 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 diff --git a/Physlib/ProbabilisticTheory/Effect/Sharp.lean b/Physlib/ProbabilisticTheory/Effect/Sharp.lean index 7ce70ff1e3..a8c46b94f9 100644 --- a/Physlib/ProbabilisticTheory/Effect/Sharp.lean +++ b/Physlib/ProbabilisticTheory/Effect/Sharp.lean @@ -31,12 +31,11 @@ be written as a nontrivial mixture of two distinct effects. Sharp effects genera @[expose] public section -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [One E] - [Module ℝ E] [PosSMulMono ℝ E] - namespace Effect -variable [IsOrderUnit E] +section OrderedVectorSpace + +variable {E : Type*} [OrderedVectorSpace E] [One E] /-! @@ -48,9 +47,15 @@ variable [IsOrderUnit E] a nontrivial mixture of two distinct effects. -/ def IsSharp (e : Effect E) : Prop := (e : E) ∈ Set.extremePoints ℝ (Set.Icc (0 : E) 1) +end OrderedVectorSpace + +section OrderUnitSpace + +variable {E : Type*} [OrderUnitSpace E] + /-- The impossible outcome 0 is sharp. -/ lemma isSharp_zero : IsSharp (0 : Effect E) := by - refine ⟨⟨le_refl 0, IsOrderUnit.one_nonneg⟩, + refine ⟨⟨le_refl 0, OrderUnitSpace.one_nonneg⟩, fun x₁ hx₁ _ hx₂ ⟨a, b, ha, hb, _, hz⟩ => ?_⟩ have hax : a • x₁ = 0 := PosCone.nonneg_add_eq_zero @@ -58,7 +63,6 @@ lemma isSharp_zero : IsSharp (0 : Effect E) := by have := congrArg (a⁻¹ • ·) hax rwa [inv_smul_smul₀ ha.ne', smul_zero] at this -omit [PosSMulMono ℝ E] [IsOrderUnit E] in /-- Sharpness is preserved by taking the complement: `e ↦ 1 - e` is an affine involution of the effect interval. -/ lemma isSharp_complement {e : Effect E} (h : IsSharp e) : IsSharp (complement e) := by @@ -77,7 +81,6 @@ lemma isSharp_complement {e : Effect E} (h : IsSharp e) : IsSharp (complement e) have hsum : x₁ + (e : E) = 1 := by rw [← x1eq]; abel exact eq_sub_of_add_eq hsum -omit [PosSMulMono ℝ E] [IsOrderUnit E] in /-- Sharpness is preserved by taking the complement, in either direction. -/ lemma isSharp_complement_iff {e : Effect E} : IsSharp (complement e) ↔ IsSharp e := ⟨fun h => complement_complement e ▸ isSharp_complement h, isSharp_complement⟩ @@ -86,4 +89,6 @@ lemma isSharp_complement_iff {e : Effect E} : IsSharp (complement e) ↔ IsSharp lemma isSharp_one : IsSharp (1 : Effect E) := complement_zero (E := E) ▸ isSharp_complement isSharp_zero +end OrderUnitSpace + end Effect From f0fbc50feff4db41d2667c3aacdf6f070df854bb Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Sun, 20 Sep 2026 22:56:15 +0200 Subject: [PATCH 7/8] feat(ProbabilisticTheory): channels and weights Adds Channel/Basic.lean (UnitalPositiveLinearMap, a positive linear map preserving the order unit -- the Heisenberg-picture notion of a physical channel) and Weight/Basic.lean + Weight/Extension.lean (extended-nonnegative-real weights on the positive cone, which generalize states by dropping normalization and finiteness, plus the unique linear extension of a finite weight off the cone). Co-Authored-By: Claude Sonnet 5 --- Physlib.lean | 3 + .../ProbabilisticTheory/Channel/Basic.lean | 104 +++++++++++ Physlib/ProbabilisticTheory/Weight/Basic.lean | 157 ++++++++++++++++ .../ProbabilisticTheory/Weight/Extension.lean | 170 ++++++++++++++++++ 4 files changed, 434 insertions(+) create mode 100644 Physlib/ProbabilisticTheory/Channel/Basic.lean create mode 100644 Physlib/ProbabilisticTheory/Weight/Basic.lean create mode 100644 Physlib/ProbabilisticTheory/Weight/Extension.lean diff --git a/Physlib.lean b/Physlib.lean index 1f6859188b..fe7b8dc6f5 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -254,6 +254,7 @@ 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 @@ -262,6 +263,8 @@ 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.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 diff --git a/Physlib/ProbabilisticTheory/Channel/Basic.lean b/Physlib/ProbabilisticTheory/Channel/Basic.lean new file mode 100644 index 0000000000..e0350a64cd --- /dev/null +++ b/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, OneHom E F + +attribute [nolint docBlame] UnitalPositiveLinearMap.toOneHom + +/-- 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 diff --git a/Physlib/ProbabilisticTheory/Weight/Basic.lean b/Physlib/ProbabilisticTheory/Weight/Basic.lean new file mode 100644 index 0000000000..494c9e8eda --- /dev/null +++ b/Physlib/ProbabilisticTheory/Weight/Basic.lean @@ -0,0 +1,157 @@ +/- +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.Data.ENNReal.Basic +public import Mathlib.Data.ENNReal.Inv +public import Mathlib.Data.ENNReal.Action +public import Physlib.ProbabilisticTheory.OrderUnit.Basic +public import Physlib.ProbabilisticTheory.OrderUnit.Cone + +/-! +# Weights + +## i. Overview + +A state assigns each positive observable a nonnegative expectation value, normalized so the +certain outcome reads exactly `1`. A *weight* generalizes this by dropping the normalization and +letting the values be extended nonnegative reals, possibly `+∞`. This matters especially in +infinite dimensions: the trace on `B(H)` is only finite on the trace-class operators and genuinely +diverges to `+∞` elsewhere. A state is then the special case that happens to be finite everywhere +and normalized. + +## ii. Key results + +- `Weight.mono` : weights are monotone on the positive cone. +- `Weight.IsFinite.isSemifinite` : a finite weight is automatically semifinite. +- `Weight.IsFinite.normalize_isState` : rescaling a finite weight that's nonzero at the order unit + turns it into a state. + +## iii. Table of contents + +- A. Weights +- B. States as weights + +## iv. References + +- G. Ludwig, *Foundations of Quantum Mechanics I*, Springer, 1983. + + +-/ + +@[expose] public section + +open scoped ENNReal NNReal + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] + [Module ℝ E] [PosSMulMono ℝ E] + +/-! + +## A. Weights + +-/ + +/-- An extended nonnegative linear functional on the positive cone. -/ +abbrev Weight (E : Type*) [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] + [Module ℝ E] [PosSMulMono ℝ E] := PosCone E →ₗ[ℝ≥0] ℝ≥0∞ + +namespace Weight + +@[ext] +lemma ext {w₁ w₂ : Weight E} (h : ∀ A, w₁ A = w₂ A) : w₁ = w₂ := + LinearMap.ext h + +/-- Only the zero positive element has weight zero. -/ +def IsFaithful (w : Weight E) : Prop := ∀ A : PosCone E, w A = 0 → A = 0 + +/-- A weight has no infinite values. -/ +def IsFinite (w : Weight E) : Prop := ∀ A : PosCone E, w A ≠ ⊤ + +/-- A weight is the supremum of its finite values below each positive element. -/ +def IsSemifinite (w : Weight E) : Prop := ∀ A : PosCone E, + w A = ⨆ B : {B : PosCone E // B ≤ A ∧ w B ≠ ⊤}, w B + +/-- Weights are monotone on the positive cone. -/ +lemma mono (w : Weight E) : Monotone (w : PosCone E → ℝ≥0∞) := by + intro A B hAB + have hC : (0 : E) ≤ (B : E) - (A : E) := sub_nonneg.mpr hAB + let C : PosCone E := ⟨(B : E) - (A : E), hC⟩ + have hAC : A + C = B := by + ext + change (A : E) + ((B : E) - (A : E)) = B + abel + calc + w A ≤ w A + w C := le_self_add + _ = w (A + C) := (map_add w A C).symm + _ = w B := by rw [hAC] + +/-- A finite weight is semifinite. -/ +lemma IsFinite.isSemifinite {w : Weight E} (hw : w.IsFinite) : w.IsSemifinite := by + intro A + apply le_antisymm + · exact le_iSup (fun B : {B : PosCone E // B ≤ A ∧ w B ≠ ⊤} => w B) + ⟨A, le_rfl, hw A⟩ + · apply iSup_le + intro B + exact w.mono B.2.1 + +/-- A finite weight's real value is additive. -/ +lemma IsFinite.toReal_map_add {w : Weight E} (hw : w.IsFinite) (A B : PosCone E) : + (w (A + B)).toReal = (w A).toReal + (w B).toReal := by + rw [w.map_add, ENNReal.toReal_add (hw A) (hw B)] + +/-- A weight's real value scales linearly under nonnegative real scaling, whether or not it's +finite: on the infinite side, both sides read `0`. -/ +lemma toReal_map_nnreal_smul (w : Weight E) (k : ℝ≥0) (A : PosCone E) : + (w (k • A)).toReal = k * (w A).toReal := by + rw [w.map_smul, ENNReal.smul_def, smul_eq_mul, ENNReal.toReal_mul, ENNReal.coe_toReal] + +/-- A weight preserves existing directed suprema in the positive cone. -/ +def IsNormal (w : Weight E) : Prop := ∀ (D : Set (PosCone E)) (A : PosCone E), + D.Nonempty → DirectedOn (· ≤ ·) D → IsLUB D A → IsLUB (w '' D) (w A) + +variable [One E] [IsOrderUnit E] + +/-! + +## B. States as weights + +-/ + +/-- A weight that's finite everywhere and gives the certain outcome weight exactly `1`. -/ +structure IsState (w : Weight E) : Prop where + /-- A state is finite everywhere. -/ + finite : w.IsFinite + /-- A state gives the certain outcome weight exactly `1`. -/ + normalized : w PosCone.unit = 1 + +/-- Rescaling a finite weight that's nonzero at the order unit. -/ +noncomputable def IsFinite.normalize {w : Weight E} (_hw : w.IsFinite) (_h : w PosCone.unit ≠ 0) : + Weight E where + toFun A := (w PosCone.unit)⁻¹ * w A + map_add' A B := by rw [map_add, mul_add] + map_smul' c A := by + simp only [map_smul, ENNReal.smul_def, smul_eq_mul, RingHom.id_apply] + ring + +lemma IsFinite.normalize_apply {w : Weight E} (hw : w.IsFinite) (h : w PosCone.unit ≠ 0) + (A : PosCone E) : hw.normalize h A = (w PosCone.unit)⁻¹ * w A := rfl + +/-- Normalizing a finite weight keeps it finite. -/ +lemma IsFinite.normalize_isFinite {w : Weight E} (hw : w.IsFinite) (h : w PosCone.unit ≠ 0) : + (hw.normalize h).IsFinite := fun A => by + rw [normalize_apply] + exact ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr h) (hw A) + +/-- Normalizing a finite weight makes it a state: the order unit is scaled to weight exactly +`1`. -/ +lemma IsFinite.normalize_isState {w : Weight E} (hw : w.IsFinite) (h : w PosCone.unit ≠ 0) : + (hw.normalize h).IsState where + finite := hw.normalize_isFinite h + normalized := by rw [normalize_apply]; exact ENNReal.inv_mul_cancel h (hw PosCone.unit) + +end Weight diff --git a/Physlib/ProbabilisticTheory/Weight/Extension.lean b/Physlib/ProbabilisticTheory/Weight/Extension.lean new file mode 100644 index 0000000000..d6beadf2ad --- /dev/null +++ b/Physlib/ProbabilisticTheory/Weight/Extension.lean @@ -0,0 +1,170 @@ +/- +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.Weight.Basic +public import Mathlib.Tactic.Module + +/-! +# Extending finite weights + +## i. Overview + +A finite weight on the positive cone of an order-unit space extends uniquely to a positive linear +functional on the whole space. Since `1` is an order unit, any `A : E` becomes nonnegative after +adding enough copies of `1`, so we set `toFun A := w (r • 1 + A) - r * w 1` for such an `r`, and +check the result does not depend on the `r` chosen. + +## ii. Key results + +- `Weight.IsFinite.toLinearMap` : the `ℝ`-linear map extending a finite weight to all of `E`. + +## iii. Table of contents + +- A. The raw shifted value +- B. The linear extension + +-/ + +@[expose] public section + +open scoped ENNReal NNReal + +variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] + [Module ℝ E] [PosSMulMono ℝ E] [One E] [IsOrderUnit E] + +namespace Weight + +variable {w : Weight E} + +namespace IsFinite + +/-! + +## A. The raw shifted value + +-/ + +/-- `A` shifted into the cone by `r` copies of the order unit, minus the corresponding multiple +of the weight of the order unit. -/ +noncomputable def rawValue (_hw : w.IsFinite) (A : E) (r : ℝ) (h : 0 ≤ r • (1 : E) + A) : ℝ := + (w ⟨r • (1 : E) + A, h⟩).toReal - r * (w PosCone.unit).toReal + +/-- Shifting by a larger `s` and a smaller `r` agree: the extra `s - r` copies of the unit added +to the cone element are exactly cancelled by the extra `(s - r) * w 1` subtracted off. -/ +lemma rawValue_of_le (hw : w.IsFinite) (A : E) {r s : ℝ} (hr : 0 ≤ r • (1 : E) + A) + (hs : 0 ≤ s • (1 : E) + A) (hrs : r ≤ s) : rawValue hw A s hs = rawValue hw A r hr := by + set t : ℝ≥0 := (s - r).toNNReal with ht_def + have ht : (t : ℝ) = s - r := Real.coe_toNNReal _ (by linarith) + have hcone : (⟨s • (1 : E) + A, hs⟩ : PosCone E) = ⟨r • (1 : E) + A, hr⟩ + t • PosCone.unit := by + apply Subtype.ext + show s • (1 : E) + A = (r • (1 : E) + A) + (t : ℝ) • (1 : E) + rw [ht] + module + unfold rawValue + rw [hcone, hw.toReal_map_add, w.toReal_map_nnreal_smul, ht] + ring + +/-- The shifted value of a finite weight does not depend on the chosen shift. -/ +lemma rawValue_indep (hw : w.IsFinite) (A : E) {r s : ℝ} (hr : 0 ≤ r • (1 : E) + A) + (hs : 0 ≤ s • (1 : E) + A) : rawValue hw A r hr = rawValue hw A s hs := by + rcases le_total r s with hrs | hrs + · exact (rawValue_of_le hw A hr hs hrs).symm + · exact rawValue_of_le hw A hs hr hrs + +/-! + +## B. The linear extension + +-/ + +open Classical in +/-- The linear extension of a finite weight from the positive cone to all of `E`. -/ +noncomputable def toFun (hw : w.IsFinite) (A : E) : ℝ := + rawValue hw A (PosCone.exists_real_shift_nonneg A).choose + (PosCone.exists_real_shift_nonneg A).choose_spec + +/-- The extension can be computed via any valid shift `r`, not just the one `toFun` happens to +pick. -/ +lemma toFun_eq (hw : w.IsFinite) (A : E) {r : ℝ} (h : 0 ≤ r • (1 : E) + A) : + toFun hw A = rawValue hw A r h := + rawValue_indep hw A _ h + +@[simp] +lemma toFun_of_nonneg (hw : w.IsFinite) (A : PosCone E) : toFun hw (A : E) = (w A).toReal := by + have h0 : (0 : E) ≤ (0 : ℝ) • (1 : E) + (A : E) := by + rw [zero_smul, zero_add] + exact (PointedCone.mem_positive (R := ℝ) (E := E)).mp A.2 + rw [toFun_eq hw (A : E) h0, rawValue] + simp + +/-- The extension of a finite weight sends `0` to `0`. -/ +lemma toFun_zero (hw : w.IsFinite) : toFun hw (0 : E) = 0 := by + have h := toFun_of_nonneg hw (0 : PosCone E) + simpa using h + +/-- The extension of a finite weight is additive. -/ +lemma toFun_add (hw : w.IsFinite) (A B : E) : toFun hw (A + B) = toFun hw A + toFun hw B := by + obtain ⟨r, hr⟩ := PosCone.exists_real_shift_nonneg A + obtain ⟨s, hs⟩ := PosCone.exists_real_shift_nonneg B + have hrs : (0 : E) ≤ (r + s) • (1 : E) + (A + B) := by + have heq : (r + s) • (1 : E) + (A + B) = (r • (1 : E) + A) + (s • (1 : E) + B) := by module + rw [heq]; exact add_nonneg hr hs + rw [toFun_eq hw A hr, toFun_eq hw B hs, toFun_eq hw (A + B) hrs] + have hcone : (⟨(r + s) • (1 : E) + (A + B), hrs⟩ : PosCone E) = + ⟨r • (1 : E) + A, hr⟩ + ⟨s • (1 : E) + B, hs⟩ := by + apply Subtype.ext + show (r + s) • (1 : E) + (A + B) = (r • (1 : E) + A) + (s • (1 : E) + B) + module + unfold rawValue + rw [hcone, hw.toReal_map_add] + ring + +/-- The extension of a finite weight negates: a corollary of additivity and `toFun_zero`. -/ +lemma toFun_neg (hw : w.IsFinite) (A : E) : toFun hw (-A) = -toFun hw A := by + have h := toFun_add hw A (-A) + rw [add_neg_cancel, toFun_zero] at h + linarith + +/-- Nonnegative real homogeneity of the finite-weight extension. -/ +lemma toFun_real_nonneg_smul (hw : w.IsFinite) {t : ℝ} (ht : 0 ≤ t) (A : E) : + toFun hw (t • A) = t * toFun hw A := by + obtain ⟨r, hr⟩ := PosCone.exists_real_shift_nonneg A + have hcr : (0 : E) ≤ (t * r) • (1 : E) + t • A := by + have heq : (t * r) • (1 : E) + t • A = t • (r • (1 : E) + A) := by module + rw [heq]; exact smul_nonneg ht hr + rw [toFun_eq hw A hr, toFun_eq hw (t • A) hcr] + have hcone : (⟨(t * r) • (1 : E) + t • A, hcr⟩ : PosCone E) = + t.toNNReal • (⟨r • (1 : E) + A, hr⟩ : PosCone E) := by + apply Subtype.ext + show (t * r) • (1 : E) + t • A = (t.toNNReal : ℝ) • (r • (1 : E) + A) + rw [Real.coe_toNNReal t ht] + module + unfold rawValue + rw [hcone, w.toReal_map_nnreal_smul, Real.coe_toNNReal t ht] + ring + +/-- Full real homogeneity of the finite-weight extension. -/ +lemma toFun_smul (hw : w.IsFinite) (t : ℝ) (A : E) : toFun hw (t • A) = t * toFun hw A := by + rcases le_total (0 : ℝ) t with ht | ht + · exact toFun_real_nonneg_smul hw ht A + · have h1 : t • A = -((-t) • A) := by rw [neg_smul, neg_neg] + rw [h1, toFun_neg, toFun_real_nonneg_smul hw (neg_nonneg.mpr ht) A] + ring + +/-- The `ℝ`-linear map extending a finite weight. -/ +noncomputable def toLinearMap (hw : w.IsFinite) : E →ₗ[ℝ] ℝ where + toFun := toFun hw + map_add' := toFun_add hw + map_smul' := toFun_smul hw + +/-- The linear extension agrees with `toFun` by construction. -/ +@[simp] +lemma toLinearMap_apply (hw : w.IsFinite) (A : E) : toLinearMap hw A = toFun hw A := rfl + +end IsFinite + +end Weight From 408630c107e28c7743a9bcc21eb9dc771ceef7ac Mon Sep 17 00:00:00 2001 From: Tom Diem Date: Wed, 23 Sep 2026 21:33:22 +0200 Subject: [PATCH 8/8] fix(ProbabilisticTheory): update Weight/Channel files for the OrderUnitSpace API Weight/{Basic,Extension}.lean used the granular pre-review typeclass bundle and PosCone.unit, which no longer exist (PosCone now has a One instance instead). Switch to OrderedVectorSpace/OrderUnitSpace and (1 : PosCone E). Co-Authored-By: Claude Sonnet 5 --- Physlib/ProbabilisticTheory/Weight/Basic.lean | 40 ++++++++++++------- .../ProbabilisticTheory/Weight/Extension.lean | 8 ++-- 2 files changed, 30 insertions(+), 18 deletions(-) diff --git a/Physlib/ProbabilisticTheory/Weight/Basic.lean b/Physlib/ProbabilisticTheory/Weight/Basic.lean index 494c9e8eda..3f7961cc63 100644 --- a/Physlib/ProbabilisticTheory/Weight/Basic.lean +++ b/Physlib/ProbabilisticTheory/Weight/Basic.lean @@ -46,21 +46,27 @@ and normalized. open scoped ENNReal NNReal -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] - [Module ℝ E] [PosSMulMono ℝ E] - /-! ## A. Weights -/ +section OrderedVectorSpace + +variable {E : Type*} [OrderedVectorSpace E] + /-- An extended nonnegative linear functional on the positive cone. -/ -abbrev Weight (E : Type*) [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] - [Module ℝ E] [PosSMulMono ℝ E] := PosCone E →ₗ[ℝ≥0] ℝ≥0∞ +abbrev Weight (E : Type*) [OrderedVectorSpace E] := PosCone E →ₗ[ℝ≥0] ℝ≥0∞ + +end OrderedVectorSpace namespace Weight +section OrderedVectorSpace + +variable {E : Type*} [OrderedVectorSpace E] + @[ext] lemma ext {w₁ w₂ : Weight E} (h : ∀ A, w₁ A = w₂ A) : w₁ = w₂ := LinearMap.ext h @@ -114,7 +120,7 @@ lemma toReal_map_nnreal_smul (w : Weight E) (k : ℝ≥0) (A : PosCone E) : def IsNormal (w : Weight E) : Prop := ∀ (D : Set (PosCone E)) (A : PosCone E), D.Nonempty → DirectedOn (· ≤ ·) D → IsLUB D A → IsLUB (w '' D) (w A) -variable [One E] [IsOrderUnit E] +end OrderedVectorSpace /-! @@ -122,36 +128,42 @@ variable [One E] [IsOrderUnit E] -/ +section OrderUnitSpace + +variable {E : Type*} [OrderUnitSpace E] + /-- A weight that's finite everywhere and gives the certain outcome weight exactly `1`. -/ structure IsState (w : Weight E) : Prop where /-- A state is finite everywhere. -/ finite : w.IsFinite /-- A state gives the certain outcome weight exactly `1`. -/ - normalized : w PosCone.unit = 1 + normalized : w 1 = 1 /-- Rescaling a finite weight that's nonzero at the order unit. -/ -noncomputable def IsFinite.normalize {w : Weight E} (_hw : w.IsFinite) (_h : w PosCone.unit ≠ 0) : +noncomputable def IsFinite.normalize {w : Weight E} (_hw : w.IsFinite) (_h : w 1 ≠ 0) : Weight E where - toFun A := (w PosCone.unit)⁻¹ * w A + toFun A := (w 1)⁻¹ * w A map_add' A B := by rw [map_add, mul_add] map_smul' c A := by simp only [map_smul, ENNReal.smul_def, smul_eq_mul, RingHom.id_apply] ring -lemma IsFinite.normalize_apply {w : Weight E} (hw : w.IsFinite) (h : w PosCone.unit ≠ 0) - (A : PosCone E) : hw.normalize h A = (w PosCone.unit)⁻¹ * w A := rfl +lemma IsFinite.normalize_apply {w : Weight E} (hw : w.IsFinite) (h : w 1 ≠ 0) + (A : PosCone E) : hw.normalize h A = (w 1)⁻¹ * w A := rfl /-- Normalizing a finite weight keeps it finite. -/ -lemma IsFinite.normalize_isFinite {w : Weight E} (hw : w.IsFinite) (h : w PosCone.unit ≠ 0) : +lemma IsFinite.normalize_isFinite {w : Weight E} (hw : w.IsFinite) (h : w 1 ≠ 0) : (hw.normalize h).IsFinite := fun A => by rw [normalize_apply] exact ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr h) (hw A) /-- Normalizing a finite weight makes it a state: the order unit is scaled to weight exactly `1`. -/ -lemma IsFinite.normalize_isState {w : Weight E} (hw : w.IsFinite) (h : w PosCone.unit ≠ 0) : +lemma IsFinite.normalize_isState {w : Weight E} (hw : w.IsFinite) (h : w 1 ≠ 0) : (hw.normalize h).IsState where finite := hw.normalize_isFinite h - normalized := by rw [normalize_apply]; exact ENNReal.inv_mul_cancel h (hw PosCone.unit) + normalized := by rw [normalize_apply]; exact ENNReal.inv_mul_cancel h (hw 1) + +end OrderUnitSpace end Weight diff --git a/Physlib/ProbabilisticTheory/Weight/Extension.lean b/Physlib/ProbabilisticTheory/Weight/Extension.lean index d6beadf2ad..9b9ebfb8cb 100644 --- a/Physlib/ProbabilisticTheory/Weight/Extension.lean +++ b/Physlib/ProbabilisticTheory/Weight/Extension.lean @@ -33,8 +33,7 @@ check the result does not depend on the `r` chosen. open scoped ENNReal NNReal -variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] - [Module ℝ E] [PosSMulMono ℝ E] [One E] [IsOrderUnit E] +variable {E : Type*} [OrderUnitSpace E] namespace Weight @@ -51,7 +50,7 @@ namespace IsFinite /-- `A` shifted into the cone by `r` copies of the order unit, minus the corresponding multiple of the weight of the order unit. -/ noncomputable def rawValue (_hw : w.IsFinite) (A : E) (r : ℝ) (h : 0 ≤ r • (1 : E) + A) : ℝ := - (w ⟨r • (1 : E) + A, h⟩).toReal - r * (w PosCone.unit).toReal + (w ⟨r • (1 : E) + A, h⟩).toReal - r * (w 1).toReal /-- Shifting by a larger `s` and a smaller `r` agree: the extra `s - r` copies of the unit added to the cone element are exactly cancelled by the extra `(s - r) * w 1` subtracted off. -/ @@ -59,7 +58,8 @@ lemma rawValue_of_le (hw : w.IsFinite) (A : E) {r s : ℝ} (hr : 0 ≤ r • (1 (hs : 0 ≤ s • (1 : E) + A) (hrs : r ≤ s) : rawValue hw A s hs = rawValue hw A r hr := by set t : ℝ≥0 := (s - r).toNNReal with ht_def have ht : (t : ℝ) = s - r := Real.coe_toNNReal _ (by linarith) - have hcone : (⟨s • (1 : E) + A, hs⟩ : PosCone E) = ⟨r • (1 : E) + A, hr⟩ + t • PosCone.unit := by + have hcone : (⟨s • (1 : E) + A, hs⟩ : PosCone E) = + ⟨r • (1 : E) + A, hr⟩ + t • (1 : PosCone E) := by apply Subtype.ext show s • (1 : E) + A = (r • (1 : E) + A) + (t : ℝ) • (1 : E) rw [ht]