PublishedLocalizedEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The localized published amenable embedding

Cameron--Christensen--Sinclair--Smith--White--Wiggins, Kadison--Kastler stable factors, Duke Math. J. 163 (2014), Theorem 3.3(i), printed p.13, arXiv:1209.4116v3. The unitary belongs to (P ∪ B)'' and has displacement at most 150 * γ. This retains that location, needed for the second preparation step, and omits the unused pointwise 100 * γ estimate.

def OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding line 22
Source documentation
Precisely the inclusion, displacement and localization portions of the published one-sided embedding theorem.
```
def PublishedLocalizedAmenableEmbedding : Prop :=
…
```
theorem OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding.forget_location line 30
theorem OAI.KadisonKastler.exists_prepared_right_correction line 39
Source documentation
The second published embedding preserves the first common inclusion. The distance estimate is expressed on the original Hilbert space.
```
theorem exists_prepared_right_correction
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding