AbelianPrimitives.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Norm-one primitives on abelian von Neumann algebras

The abelian case of the classical type-I input is proved directly. Finite families of projections admit common finite partitions. Their separability homotopies have norm at most one; a bounded weak-* limit is exact on every projection, hence everywhere by density of the span of projections.

lemma OAI.BoundedHochschild.KadisonRingrose.mergeInputs_cons_zero line 28
lemma OAI.BoundedHochschild.KadisonRingrose.mergeInputs_cons_succ line 36
lemma OAI.BoundedHochschild.KadisonRingrose.differentialValue_cons line 44
lemma OAI.BoundedHochschild.KadisonRingrose.first_homotopy_identity line 69
def OAI.BoundedHochschild.KadisonRingrose.partitionHomotopy line 85
lemma OAI.BoundedHochschild.KadisonRingrose.partitionHomotopy_norm line 88
lemma OAI.BoundedHochschild.KadisonRingrose.partitionHomotopy_exact line 109
theorem OAI.BoundedHochschild.KadisonRingrose.abelian_primitive line 148
Source documentation
The abelian case of the classical input, proved with an explicit norm-one bound.
```
theorem abelian_primitive (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {n : ℕ} (f : Cochain M (n + 1)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M n, ‖g‖ ≤ ‖f‖ ∧ ∀ x, differentialValue g x = f x := by
…
```
Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue