Skip to content

Commit d8282b1

Browse files
markkasaurusmarkkasaurus
committed
Initial release
0 parents  commit d8282b1

56 files changed

Lines changed: 5277 additions & 0 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/pull_request_template.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
## Summary
2+
3+
-
4+
5+
## Verification
6+
7+
- [ ] `./scripts/verify.sh`
8+
9+
## AI assistance disclosure
10+
11+
- [ ] No material generative AI assistance was used in this change.
12+
- [ ] Material generative AI assistance was used and is disclosed below.
13+
14+
If material generative AI assistance was used, name the tool or model and state
15+
the scope of the assistance here.

‎.github/workflows/ci.yml‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
name: CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
jobs:
9+
verify:
10+
runs-on: ubuntu-latest
11+
steps:
12+
- name: Check out repository
13+
uses: actions/checkout@v5
14+
15+
- name: Install elan
16+
run: |
17+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
18+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
19+
20+
- name: Show toolchain
21+
run: cat lean-toolchain
22+
23+
- name: Verify repository
24+
run: ./scripts/verify.sh

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
.DS_Store
2+
.lake/
3+
build/
4+
*.log
5+
paper/

‎Busch/ClassicalBridge.lean‎

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
/-
2+
# Busch/ClassicalBridge.lean — Bridge from Effects to Classical Frame Functions
3+
Every classical projection `P : Projection H` yields an effect
4+
`Effect.ofClassicalProjection P : Effect H`. This file establishes the
5+
translation:
6+
* classical `Projection.zero ↦ (0 : Effect H)`
7+
* classical `Projection.one ↦ (1 : Effect H)`
8+
* classical orthogonality `P ⟂ Q ↦ Busch summability`
9+
* classical sum `Projection.add P Q h ↦ Busch `orthoSum``
10+
Consequence: every Busch `GenFrameFunction H` restricts to a classical
11+
`FrameFunction H`.
12+
This is a compatibility bridge between the effects formulation and the
13+
projection language.
14+
-/
15+
import Busch.ProjectionRestriction
16+
import Classical.Projection
17+
import Classical.FrameFunction
18+
19+
noncomputable section
20+
21+
namespace Busch
22+
23+
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
24+
[FiniteDimensional ℂ H]
25+
26+
/-! ### Lifting classical projections to effects -/
27+
namespace Effect
28+
29+
/-- Every classical `Projection H` is an effect. -/
30+
def ofClassicalProjection (P : Projection H) : Effect H where
31+
op := P.1
32+
isSelfAdjoint := Projection.selfAdjointOp P
33+
nonneg x := by
34+
have hIdem : P.1 * P.1 = P.1 := P.2.1
35+
have hSA : ∀ a b : H, inner (𝕜 := ℂ) (P.1 a) b = inner (𝕜 := ℂ) a (P.1 b) :=
36+
Projection.selfAdjointOp P
37+
have hdiag := inner_self_selfAdjoint_idempotent P.1 hSA hIdem x
38+
rw [hdiag]
39+
exact @inner_self_nonneg ℂ H _ _ _ (P.1 x)
40+
le_one x := by
41+
have hIdem : P.1 * P.1 = P.1 := P.2.1
42+
have hSA : ∀ a b : H, inner (𝕜 := ℂ) (P.1 a) b = inner (𝕜 := ℂ) a (P.1 b) :=
43+
Projection.selfAdjointOp P
44+
exact re_inner_le_self_of_selfAdjoint_idempotent P.1 hSA hIdem x
45+
omit [FiniteDimensional ℂ H] in
46+
@[simp] lemma ofClassicalProjection_op (P : Projection H) :
47+
(ofClassicalProjection P).op = P.1 := rfl
48+
49+
omit [FiniteDimensional ℂ H] in
50+
/-- The lifted projection is a projection-effect (idempotent). -/
51+
lemma ofClassicalProjection_isProjection (P : Projection H) :
52+
IsProjection (ofClassicalProjection P) := by
53+
show (ofClassicalProjection P).op * (ofClassicalProjection P).op = (ofClassicalProjection P).op
54+
simp only [ofClassicalProjection_op]
55+
exact P.2.1
56+
57+
end Effect
58+
59+
/-! ### Wrapping as `ProjectionEffect` -/
60+
namespace ProjectionEffect
61+
62+
/-- Every classical `Projection H` is a Busch projection-effect. -/
63+
def ofClassicalProjection (P : Projection H) : ProjectionEffect H where
64+
effect := Effect.ofClassicalProjection P
65+
is_projection := Effect.ofClassicalProjection_isProjection P
66+
67+
omit [FiniteDimensional ℂ H] in
68+
@[simp] lemma ofClassicalProjection_effect (P : Projection H) :
69+
(ofClassicalProjection P).effect = Effect.ofClassicalProjection P := rfl
70+
71+
omit [FiniteDimensional ℂ H] in
72+
@[simp] lemma ofClassicalProjection_op (P : Projection H) :
73+
(ofClassicalProjection P).effect.op = P.1 := rfl
74+
75+
omit [FiniteDimensional ℂ H] in
76+
/-- Classical orthogonality of projections translates to Busch projection-effect
77+
orthogonality. -/
78+
lemma orthogonal_of_classical {P Q : Projection H} (h : Projection.orthogonal P Q) :
79+
(ofClassicalProjection P).orthogonal (ofClassicalProjection Q) := by
80+
show (Effect.ofClassicalProjection P).op * (Effect.ofClassicalProjection Q).op = 0
81+
simp only [Effect.ofClassicalProjection_op]
82+
exact h
83+
84+
end ProjectionEffect
85+
86+
/-! ### Summability and orthogonal sums from classical data -/
87+
namespace Effect
88+
89+
omit [FiniteDimensional ℂ H] in
90+
/-- Classical orthogonality of projections implies Busch summability of the
91+
lifted effects. -/
92+
lemma summable_ofClassical {P Q : Projection H} (h : Projection.orthogonal P Q) :
93+
Summable (ofClassicalProjection P) (ofClassicalProjection Q) :=
94+
ProjectionEffect.summable_of_orthogonal
95+
(ProjectionEffect.ofClassicalProjection P)
96+
(ProjectionEffect.ofClassicalProjection Q)
97+
(ProjectionEffect.orthogonal_of_classical h)
98+
99+
end Effect
100+
101+
/-! ### Lifting the classical zero/one/add -/
102+
namespace Effect
103+
104+
omit [FiniteDimensional ℂ H] in
105+
/-- The classical zero projection lifts to the zero effect. -/
106+
@[simp] lemma ofClassicalProjection_zero :
107+
ofClassicalProjection (Projection.zero : Projection H) = (0 : Effect H) := by
108+
apply Effect.ext
109+
intro x
110+
show (Projection.zero : Projection H).1 x = (0 : Effect H).op x
111+
show (0 : H →L[ℂ] H) x = (0 : Effect H).op x
112+
simp
113+
114+
omit [FiniteDimensional ℂ H] in
115+
/-- The classical identity projection lifts to the identity effect. -/
116+
@[simp] lemma ofClassicalProjection_one :
117+
ofClassicalProjection (Projection.one : Projection H) = (1 : Effect H) := by
118+
apply Effect.ext
119+
intro x
120+
show (Projection.one : Projection H).1 x = (1 : Effect H).op x
121+
show (1 : H →L[ℂ] H) x = (1 : Effect H).op x
122+
simp
123+
124+
omit [FiniteDimensional ℂ H] in
125+
/-- The classical sum of orthogonal projections lifts to the Busch orthogonal sum. -/
126+
lemma ofClassicalProjection_add {P Q : Projection H} (h : Projection.orthogonal P Q) :
127+
ofClassicalProjection (Projection.add P Q h) =
128+
orthoSum (ofClassicalProjection P) (ofClassicalProjection Q)
129+
(summable_ofClassical h) := by
130+
apply Effect.ext
131+
intro x
132+
show (Projection.add P Q h).1 x
133+
= (ofClassicalProjection P).op x + (ofClassicalProjection Q).op x
134+
show (P.1 + Q.1) x = P.1 x + Q.1 x
135+
rfl
136+
137+
end Effect
138+
139+
/-! ### Classical frame function from a Busch generalized frame function -/
140+
namespace GenFrameFunction
141+
142+
/-- **Restriction theorem**: every Busch generalized frame function restricts to
143+
a classical frame function on projections. -/
144+
def toFrameFunction (f : GenFrameFunction H) : FrameFunction H where
145+
μ P := f.μ (Effect.ofClassicalProjection P)
146+
nonneg P := f.nonneg _
147+
additive P Q h := by
148+
rw [Effect.ofClassicalProjection_add h]
149+
exact f.additive _ _ (Effect.summable_ofClassical h)
150+
normalized := by
151+
show f.μ (Effect.ofClassicalProjection Projection.one) = 1
152+
rw [Effect.ofClassicalProjection_one]
153+
exact f.normalized
154+
@[simp] lemma toFrameFunction_apply (f : GenFrameFunction H) (P : Projection H) :
155+
(f.toFrameFunction).μ P = f.μ (Effect.ofClassicalProjection P) := rfl
156+
157+
end GenFrameFunction
158+
159+
end Busch

‎Busch/ConvexCombination.lean‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
/-
2+
# Busch/ConvexCombination.lean — General Convex Combinations
3+
Generalizes `ConvexLinearity.lean` from t ∈ [0,1] combinations to any
4+
nonneg combinations αE + βF with α + β ≤ 1 (which keeps αE + βF an effect).
5+
This is needed for the linear extension step, where we express any
6+
self-adjoint operator as a difference of scaled effects.
7+
-/
8+
import Busch.ConvexLinearity
9+
10+
noncomputable section
11+
12+
namespace Busch
13+
14+
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
15+
16+
namespace Effect
17+
18+
/-- For `α, β ≥ 0` with `α + β ≤ 1`, `αE + βF` is an effect (summability condition). -/
19+
lemma smulIcc_pair_summable (α β : UnitIcc) (h : α.1 + β.1 ≤ 1) (E F : Effect H) :
20+
Summable (smulIcc α E) (smulIcc β F) := by
21+
intro x
22+
show (inner (𝕜 := ℂ) x
23+
(((α.1 : ℂ) • E.op + (β.1 : ℂ) • F.op) x)).re ≤ _
24+
simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
25+
inner_add_right, inner_smul_right]
26+
simp only [Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im,
27+
zero_mul, sub_zero]
28+
have h_α : α.1 * (inner (𝕜 := ℂ) x (E.op x)).re ≤ α.1 * (inner (𝕜 := ℂ) x x).re :=
29+
mul_le_mul_of_nonneg_left (E.le_one x) α.2.1
30+
have h_β : β.1 * (inner (𝕜 := ℂ) x (F.op x)).re ≤ β.1 * (inner (𝕜 := ℂ) x x).re :=
31+
mul_le_mul_of_nonneg_left (F.le_one x) β.2.1
32+
have h_self_nn : 0 ≤ (inner (𝕜 := ℂ) x x).re := @inner_self_nonneg ℂ H _ _ _ x
33+
have h_ab : α.1 * (inner (𝕜 := ℂ) x x).re + β.1 * (inner (𝕜 := ℂ) x x).re ≤
34+
(inner (𝕜 := ℂ) x x).re := by
35+
have : α.1 + β.1 ≤ 1 := h
36+
nlinarith
37+
linarith
38+
39+
end Effect
40+
41+
namespace GenFrameFunction
42+
43+
/-- **General linear combination**: `μ(αE + βF) = αμ(E) + βμ(F)` for `α, β ≥ 0`
44+
with `α + β ≤ 1`. -/
45+
theorem μ_pair_sum (f : GenFrameFunction H) (α β : Effect.UnitIcc)
46+
(h : α.1 + β.1 ≤ 1) (E F : Effect H) :
47+
f.μ (Effect.orthoSum (Effect.smulIcc α E) (Effect.smulIcc β F)
48+
(Effect.smulIcc_pair_summable α β h E F)) =
49+
α.1 * f.μ E + β.1 * f.μ F := by
50+
rw [f.additive]
51+
rw [f.μ_smulIcc, f.μ_smulIcc]
52+
53+
end GenFrameFunction
54+
55+
end Busch

‎Busch/ConvexLinearity.lean‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
/-
2+
# Busch/ConvexLinearity.lean — Convex Linearity of Frame Functions
3+
This file proves affine behavior of generalized frame functions along convex
4+
combinations of effects. The key input is that `tE` and `(1 - t)F` are
5+
summable whenever `t ∈ [0, 1]`, so additivity and real homogeneity combine to
6+
give convex linearity.
7+
-/
8+
import Busch.RealHomogeneity
9+
10+
noncomputable section
11+
12+
namespace Busch
13+
14+
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
15+
16+
namespace Effect
17+
18+
/-- For `t ∈ [0, 1]`, the pair `(tE, (1-t)F)` is summable for any effects `E, F`. -/
19+
lemma smulIcc_convex_summable (t : UnitIcc) (E F : Effect H) :
20+
Summable (smulIcc t E)
21+
(smulIcc ⟨1 - t.1, by linarith [t.2.2], by linarith [t.2.1]⟩ F) := by
22+
intro x
23+
show (inner (𝕜 := ℂ) x
24+
(((t.1 : ℂ) • E.op + ((1 - t.1 : ℝ) : ℂ) • F.op) x)).re ≤ _
25+
simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
26+
inner_add_right, inner_smul_right]
27+
simp only [Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im,
28+
zero_mul, sub_zero]
29+
have h_t_pos : 0 ≤ t.1 := t.2.1
30+
have h_1t_pos : 0 ≤ 1 - t.1 := by linarith [t.2.2]
31+
have h_E_le : t.1 * (inner (𝕜 := ℂ) x (E.op x)).re ≤ t.1 * (inner (𝕜 := ℂ) x x).re :=
32+
mul_le_mul_of_nonneg_left (E.le_one x) h_t_pos
33+
have h_F_le : (1 - t.1) * (inner (𝕜 := ℂ) x (F.op x)).re ≤
34+
(1 - t.1) * (inner (𝕜 := ℂ) x x).re :=
35+
mul_le_mul_of_nonneg_left (F.le_one x) h_1t_pos
36+
have h_sum : t.1 * (inner (𝕜 := ℂ) x x).re + (1 - t.1) * (inner (𝕜 := ℂ) x x).re
37+
= (inner (𝕜 := ℂ) x x).re := by ring
38+
linarith
39+
40+
/-- **Convex combination as an effect**. -/
41+
def convexComb (t : UnitIcc) (E F : Effect H) : Effect H :=
42+
orthoSum (smulIcc t E)
43+
(smulIcc ⟨1 - t.1, by linarith [t.2.2], by linarith [t.2.1]⟩ F)
44+
(smulIcc_convex_summable t E F)
45+
@[simp] lemma convexComb_op (t : UnitIcc) (E F : Effect H) :
46+
(convexComb t E F).op = (t.1 : ℂ) • E.op + ((1 - t.1 : ℝ) : ℂ) • F.op := rfl
47+
48+
end Effect
49+
50+
namespace GenFrameFunction
51+
52+
/-- **Convex linearity**: `μ(tE + (1-t)F) = t·μ(E) + (1-t)·μ(F)` for `t ∈ [0,1]`. -/
53+
theorem μ_convexComb (f : GenFrameFunction H) (t : Effect.UnitIcc) (E F : Effect H) :
54+
f.μ (Effect.convexComb t E F) = t.1 * f.μ E + (1 - t.1) * f.μ F := by
55+
unfold Effect.convexComb
56+
rw [f.additive]
57+
rw [f.μ_smulIcc, f.μ_smulIcc]
58+
59+
/-- **Linearity on scaled pairs**: `μ(tE ⊕ sF) = tμ(E) + sμ(F)` when `tE + sF ≤ 1`. -/
60+
theorem μ_smulIcc_sum (f : GenFrameFunction H) (t s : Effect.UnitIcc) (E F : Effect H)
61+
(h : Effect.Summable (Effect.smulIcc t E) (Effect.smulIcc s F)) :
62+
f.μ (Effect.orthoSum (Effect.smulIcc t E) (Effect.smulIcc s F) h) =
63+
t.1 * f.μ E + s.1 * f.μ F := by
64+
rw [f.additive]
65+
rw [f.μ_smulIcc, f.μ_smulIcc]
66+
67+
end GenFrameFunction
68+
69+
end Busch

0 commit comments

Comments
 (0)