OAI/Analysis/InterpolatedFactors/Absorption.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.RectangularAbsorption.part line 13
  2. def OAI.FreeGroupFactorMain.RectangularAbsorption.remainder line 14
  3. def OAI.FreeGroupFactorMain.RectangularAbsorption.shifted line 15
  4. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.part_supported line 19
  5. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.remainder_compression line 25
  6. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.shifted_zero_compression line 30
  7. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.shifted_succ_compression line 34
  8. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.recover line 38
  9. def OAI.FreeGroupFactorMain.RectangularAbsorption.paired line 47
  10. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.paired_compression line 49
  11. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.paired_shifted_zero line 53
  12. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.paired_shifted_succ line 60
  13. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.recover_paired line 68
  14. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.recover_supported_paired line 80
  15. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.generation_equivalence line 89
  16. structure OAI.FreeGroupFactorMain.RectangularAbsorption.Data line 117
  17. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.p_square line 135
  18. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.p_star line 137
  19. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.q_square line 139
  20. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.q_star line 141
  21. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.trace_pa line 143
  22. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.trace_pap line 144
  23. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.part_part line 147
  24. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.part_remainder line 158
  25. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.remainder_part line 170
  26. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.remainder_remainder line 175
  27. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.part_D line 192
  28. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.D_part line 199
  29. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.remainder_D line 206
  30. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.D_remainder line 210
  31. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Data.shifted_covariance line 214
  32. def OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal line 241
  33. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.add_left line 246
  34. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.sub_left line 249
  35. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.add_right line 252
  36. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.sub_right line 255
  37. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.symm line 258
  38. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.sandwich_left line 262
  39. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.sandwich_right line 269
  40. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.part_left line 272
  41. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.part_right line 274
  42. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.remainder_left line 276
  43. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.remainder_right line 278
  44. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.shifted_left line 281
  45. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.shifted_right line 287
  46. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Orthogonal.shifted line 292
  47. structure OAI.FreeGroupFactorMain.RectangularAbsorption.Family line 301
  48. def OAI.FreeGroupFactorMain.RectangularAbsorption.Family.output line 311
  49. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Family.output_cross line 314
  50. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Family.output_covariance line 320
  51. theorem OAI.FreeGroupFactorMain.RectangularAbsorption.Family.output_generation line 330