RegularOperators.lean`

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireRegular.mem_l2_reindex line 23
Source documentation
Permuting the coordinates of a square-summable family preserves membership, without requiring a countable set of coordinates.
```
theorem mem_l2_reindex (e : α ≃ β) (f : ℓ²(α, ℂ)) :
    Memℓp (fun j => f (e.symm j)) 2 := by
…
```
def OAI.KervaireRegular.reindexLinear line 29
Source documentation
Coordinate permutation before adding the isometric structure.
```
def reindexLinear (e : α ≃ β) : ℓ²(α, ℂ) ≃ₗ[ℂ] ℓ²(β, ℂ) where
…
```
theorem OAI.KervaireRegular.reindexLinear_apply line 37
def OAI.KervaireRegular.reindex line 41
Source documentation
The unitary permutation representation on ℓ², for arbitrary index types.
```
def reindex (e : α ≃ β) : ℓ²(α, ℂ) ≃ₗᵢ[ℂ] ℓ²(β, ℂ) :=
…
```
theorem OAI.KervaireRegular.reindex_apply line 47
theorem OAI.KervaireRegular.reindex_symm line 50
theorem OAI.KervaireRegular.reindex_trans line 54
def OAI.KervaireRegular.delta line 60
Source documentation
The standard delta vector used for the finite trace.
```
def delta (i : α) : ℓ²(α, ℂ) := by classical exact lp.single 2 i 1
```
theorem OAI.KervaireRegular.reindex_delta line 62
theorem OAI.KervaireRegular.inner_delta_left line 68
theorem OAI.KervaireRegular.inner_delta_right line 73
def OAI.KervaireRegular.left line 81
Source documentation
L(a) δ_x = δ_(ax) including infinite and uncountable groups.
```
def left (a : A) : ℓ²(A, ℂ) ≃ₗᵢ[ℂ] ℓ²(A, ℂ) := reindex (Equiv.mulLeft a)
```
Mentions: OAI.KervaireRegular.reindex
def OAI.KervaireRegular.right line 83
theorem OAI.KervaireRegular.left_apply line 85
theorem OAI.KervaireRegular.right_apply line 88
theorem OAI.KervaireRegular.left_delta line 91
theorem OAI.KervaireRegular.right_delta line 94
theorem OAI.KervaireRegular.left_mul line 97
theorem OAI.KervaireRegular.right_mul line 100
theorem OAI.KervaireRegular.left_right line 104
Source documentation
The commuting left and right regular actions.
```
theorem left_right (a b : A) (f : ℓ²(A, ℂ)) :
    left a (right b f) = right b (left a f) := by ext x; simp [mul_assoc]
```
Mentions: OAI.KervaireRegular.left, OAI.KervaireRegular.right
abbrev OAI.KervaireRegular.Operator line 107
instance OAI.KervaireRegular.operator_real_smulCommClass line 109
instance OAI.KervaireRegular.operator_real_isScalarTower line 112
def OAI.KervaireRegular.InCommutant line 116
Source documentation
The commutant of the right regular representation.
```
def InCommutant (T : Operator A) : Prop :=
…
```
Mentions: OAI.KervaireRegular.Operator
theorem OAI.KervaireRegular.right_star line 119
theorem OAI.KervaireRegular.right_one line 125
theorem OAI.KervaireRegular.apply_delta_eq_right line 130
Source documentation
Translation equivariance determines every matrix coefficient from one column.
```
theorem apply_delta_eq_right {T : Operator A} (hT : InCommutant T) (y : A) :
    T (delta y) = right y⁻¹ (T (delta 1)) := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant, OAI.KervaireRegular.delta, OAI.KervaireRegular.right
theorem OAI.KervaireRegular.matrix_coefficient line 135
def OAI.KervaireRegular.trace line 140
Source documentation
The (unnormalized for one copy) vector trace.
```
def trace : Operator A →L[ℂ] ℂ :=
…
```
Mentions: OAI.KervaireRegular.Operator
theorem OAI.KervaireRegular.trace_apply line 143
theorem OAI.KervaireRegular.trace_eq_coefficient line 146
theorem OAI.KervaireRegular.trace_one line 149
theorem OAI.KervaireRegular.star_coefficient line 154
Source documentation
The reflected coefficient identity needed to evaluate a product trace.
```
theorem star_coefficient {T : Operator A} (hT : InCommutant T) (x : A) :
    star (star T (delta 1) x) = T (delta 1) x⁻¹ := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant, OAI.KervaireRegular.delta
theorem OAI.KervaireRegular.trace_mul_eq_tsum line 164
theorem OAI.KervaireRegular.trace_mul_comm line 175
Source documentation
Cyclicity uses a bijection of the entire index set; countability is unnecessary.
```
theorem trace_mul_comm {S T : Operator A} (hS : InCommutant S) (hT : InCommutant T) :
    trace (S * T) = trace (T * S) := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant, OAI.KervaireRegular.trace
theorem OAI.KervaireRegular.eq_zero_of_delta_one line 186
Source documentation
The vector at the identity is separating for the right regular commutant.
```
theorem eq_zero_of_delta_one {T : Operator A} (hT : InCommutant T)
    (h : T (delta 1) = 0) : T = 0 := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant, OAI.KervaireRegular.delta
theorem OAI.KervaireRegular.trace_star_mul_self_eq_zero_iff line 202
Source documentation
Faithfulness in positive-square form, the part needed for positive operators.
```
theorem trace_star_mul_self_eq_zero_iff {T : Operator A} (hT : InCommutant T) :
    trace (star T * T) = 0 ↔ T = 0 := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant, OAI.KervaireRegular.trace
theorem OAI.KervaireRegular.InCommutant.sqrt line 218
Source documentation
The commutant is closed under the nonnegative continuous square root.
```
theorem InCommutant.sqrt {T : Operator A} (hT : InCommutant T) :
    InCommutant (CFC.sqrt T) := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant
theorem OAI.KervaireRegular.trace_nonneg line 224
Source documentation
Positivity of the vector functional.
```
theorem trace_nonneg {T : Operator A} (hT : 0 ≤ T) : 0 ≤ (trace T).re :=
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.trace
theorem OAI.KervaireRegular.trace_eq_zero_iff_of_nonneg line 228
Source documentation
Faithfulness for every nonnegative operator in the commutant.
```
theorem trace_eq_zero_iff_of_nonneg {T : Operator A} (hT : InCommutant T)
    (hpos : 0 ≤ T) : trace T = 0 ↔ T = 0 := by
…
```
Mentions: OAI.KervaireRegular.Operator, OAI.KervaireRegular.InCommutant, OAI.KervaireRegular.trace