OAI/Analysis/InterpolatedFactors/Gaussian.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.algebraCyclic line 11
  2. theorem OAI.FreeGroupFactorMain.algebraCyclic_invariant line 21
  3. theorem OAI.FreeGroupFactorMain.algebraCyclic_closure_invariant line 27
  4. theorem OAI.FreeGroupFactorMain.projection_commutes_of_invariant line 34
  5. theorem OAI.FreeGroupFactorMain.bicommutant_vector_mem_cyclic line 45
  6. def OAI.FreeGroupFactorMain.PairCyclic.diag line 74
  7. theorem OAI.FreeGroupFactorMain.PairCyclic.diag_apply line 78
  8. theorem OAI.FreeGroupFactorMain.PairCyclic.diag_star line 80
  9. def OAI.FreeGroupFactorMain.PairCyclic.coord line 89
  10. def OAI.FreeGroupFactorMain.PairCyclic.embed line 92
  11. theorem OAI.FreeGroupFactorMain.PairCyclic.coord_diag line 96
  12. theorem OAI.FreeGroupFactorMain.PairCyclic.diag_embed line 99
  13. theorem OAI.FreeGroupFactorMain.PairCyclic.pair_decompose line 103
  14. def OAI.FreeGroupFactorMain.PairCyclic.block line 108
  15. theorem OAI.FreeGroupFactorMain.PairCyclic.block_commute line 110
  16. theorem OAI.FreeGroupFactorMain.PairCyclic.diag_commute_of_blocks line 116
  17. def OAI.FreeGroupFactorMain.PairCyclic.orbit line 130
  18. theorem OAI.FreeGroupFactorMain.PairCyclic.orbit_invariant line 140
  19. theorem OAI.FreeGroupFactorMain.PairCyclic.closure_invariant line 145
  20. theorem OAI.FreeGroupFactorMain.PairCyclic.bicommutant_mem_closure line 151
  21. theorem OAI.FreeGroupFactorMain.PairCyclic.invariant_bicommutant line 179
  22. def OAI.FreeGroupFactorMain.GaussianExtension.creationWord line 208
  23. def OAI.FreeGroupFactorMain.GaussianExtension.pairNormal line 211
  24. def OAI.FreeGroupFactorMain.GaussianExtension.creationWordSpan line 214
  25. theorem OAI.FreeGroupFactorMain.GaussianExtension.creationWord_coeff line 217
  26. theorem OAI.FreeGroupFactorMain.GaussianExtension.creationWord_create line 221
  27. theorem OAI.FreeGroupFactorMain.GaussianExtension.creationWord_annihilate_nil line 226
  28. theorem OAI.FreeGroupFactorMain.GaussianExtension.creationWord_annihilate_cons line 230
  29. theorem OAI.FreeGroupFactorMain.GaussianExtension.pairNormal_coeff line 235
  30. theorem OAI.FreeGroupFactorMain.GaussianExtension.pairNormal_create line 239
  31. theorem OAI.FreeGroupFactorMain.GaussianExtension.pairNormal_semicircle_mem line 244
  32. theorem OAI.FreeGroupFactorMain.GaussianExtension.span_invariant_of_family line 269
  33. theorem OAI.FreeGroupFactorMain.GaussianExtension.closure_invariant_of_family line 278
  34. theorem OAI.FreeGroupFactorMain.GaussianExtension.bicommutant_pair_creationWord line 287
  35. def OAI.FreeGroupFactorMain.GaussianExtension.constraint line 313
  36. theorem OAI.FreeGroupFactorMain.GaussianExtension.constraint_apply line 317
  37. theorem OAI.FreeGroupFactorMain.GaussianExtension.covariance_extension line 322
  38. theorem OAI.FreeGroupFactorMain.GaussianExtension.annihilation_extension line 372