OAI/Analysis/InterpolatedFactors/Spatial.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.groupPolynomial line 15
  2. theorem OAI.FreeGroupFactorMain.Amplification.groupPolynomial_dense line 18
  3. theorem OAI.FreeGroupFactorMain.Amplification.trace_iso_orbit_total line 40
  4. theorem OAI.FreeGroupFactorMain.Amplification.spatial_of_trace_iso line 65
  5. def OAI.FreeGroupFactorMain.Amplification.nestedSpatialValue line 87
  6. theorem OAI.FreeGroupFactorMain.Amplification.nestedSpatialValue_apply line 91
  7. def OAI.FreeGroupFactorMain.Amplification.nestedSpatial line 94
  8. theorem OAI.FreeGroupFactorMain.Amplification.nestedSpatial_apply line 111
  9. def OAI.FreeGroupFactorMain.Amplification.productSpatial line 114
  10. theorem OAI.FreeGroupFactorMain.Amplification.productSpatial_apply line 118
  11. theorem OAI.FreeGroupFactorMain.Amplification.productSpatial_symm line 123
  12. theorem OAI.FreeGroupFactorMain.Amplification.productSpatial_productSingle line 127
  13. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_spatial line 141
  14. theorem OAI.FreeGroupFactorMain.Amplification.productSpatial_stabilization line 156