ConstantConjugateFreeness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Source quotient unitaries and the concrete conjugated constant embedding.

theorem OAI.KadisonSimilarity.ConstantIntegerMoments.scalarFree line 21
theorem OAI.KadisonSimilarity.tracialUltrapowerMap_constant line 43
theorem OAI.KadisonSimilarity.conjugatedConstantEmbedding_coordinate line 51
theorem OAI.KadisonSimilarity.popaConjugateFreeness_of_constant_moments line 67
Source documentation
Ambient constant freeness supplies the exact published-input proposition, with the witness retained in the source ultrapower.
```
theorem popaConjugateFreeness_of_constant_moments
    (hω : (ω : Filter ℕ) ≤ Filter.cofinite) (ρ : R →⋆ₐ[ℂ] A)
    (u : ℕ → unitary A)
    (hu : ConstantIntegerMoments τB hB ω trB (fun n => mapUnitary φ (u n))) :
    Popa1995ConjugateFreenessInput τA τB hA hB ω trA trB φ hφ hω ρ := by
…
```
Mentions: OAI.KadisonSimilarity.ConstantIntegerMoments, OAI.KadisonSimilarity.Popa1995ConjugateFreenessInput