OAI/Analysis/InterpolatedFactors/Scaling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.unitCornerEquiv line 14
  2. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.one line 24
  3. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.pow line 36
  4. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.of_near_one line 42
  5. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.transport line 65
  6. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.of_recognitions line 90
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.scalar_hasCornerScaling_weighted line 124
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.scalar_hasCornerScaling_near_one line 142
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.scalarTrace_one line 154
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.scalar_hasCornerScaling line 157
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.scalarGroup_hasCornerScaling line 162
  12. theorem OAI.FreeGroupFactorMain.Amplification.smallScaling_transport_group line 175
  13. theorem OAI.FreeGroupFactorMain.Amplification.infinite_hasCornerScaling line 190