OAI/Analysis/InterpolatedFactors/Positive.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Amplification.finiteProjection_trace_div line 13
  2. theorem OAI.FreeGroupFactorMain.Amplification.preferred_scaling_model line 20
  3. theorem OAI.FreeGroupFactorMain.Amplification.allPositiveScaling_both line 52
  4. theorem OAI.FreeGroupFactorMain.Amplification.infinite_allPositiveScaling line 71
  5. theorem OAI.FreeGroupFactorMain.HasNormalTracialIso.symm line 81
  6. theorem OAI.FreeGroupFactorMain.center_scalar_of_iso line 92
  7. theorem OAI.FreeGroupFactorMain.Amplification.rankTwo_smallScaling line 113
  8. theorem OAI.FreeGroupFactorMain.Amplification.rankTwo_center_scalar line 117
  9. theorem OAI.FreeGroupFactorMain.Amplification.rankTwo_allPositiveScaling line 122
  10. theorem OAI.FreeGroupFactorMain.Amplification.positiveRealSelfSimilarity line 128