OAI/Analysis/InterpolatedFactors/Diffuse.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.OrthogonalSpectralSum.Op line 12
  2. theorem OAI.FreeGroupFactorMain.OrthogonalSpectralSum.projection_inner line 14
  3. theorem OAI.FreeGroupFactorMain.OrthogonalSpectralSum.eigen_root_zero line 22
  4. theorem OAI.FreeGroupFactorMain.SpectralSeparation.cross_zero line 58
  5. theorem OAI.FreeGroupFactorMain.SpectralSeparation.separated_projection_mem line 87
  6. theorem OAI.FreeGroupFactorMain.CornerRerouting.single_edge_corner_commute line 118
  7. theorem OAI.FreeGroupFactorMain.CornerRerouting.single_edge_corner_generated line 160
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_mul_P line 209
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_mul_defect line 213
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.defect_mul_edgeRange line 216
  11. def OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle line 221
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_selfAdjoint line 224
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_left line 228
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_right line 234
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.range_mul_defectSemicircle line 240
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_mul_range line 244
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_leftModulus line 250
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.leftModulus_mul_P line 253
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_defectSemicircle line 257
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_mul_P line 261
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.compressed_edge_formula line 266
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_smul line 274
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_mem_ambient line 284
  24. def OAI.FreeGroupFactorMain.WeightedFock.oldBaseShift line 294
  25. def OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator line 297
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator_selfAdjoint line 300
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator_left line 307
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator_right line 312
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator_mem_ambient line 317
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator_eigen_root_zero line 323
  31. def OAI.FreeGroupFactorMain.Bicommutant.algebra line 340
  32. theorem OAI.FreeGroupFactorMain.Bicommutant.subset line 342
  33. theorem OAI.FreeGroupFactorMain.Bicommutant.mono line 345
  34. theorem OAI.FreeGroupFactorMain.Bicommutant.generated_le line 348
  35. def OAI.FreeGroupFactorMain.WeightedFock.diffuseBase line 362
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mem_diffuseBase line 365
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseGenerator_mem_diffuseBase line 368
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_mem_diffuseBase line 372
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.leftModulus_mem_diffuseBase line 384
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_mem_diffuseBase line 396
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_mem_diffuseBase line 400
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.edge_corner_mem_diffuseBase line 410