OAI/Analysis/InterpolatedFactors/Mixed.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.WeightedFock.residualCreation_filled_annihilation line 13
  2. def OAI.FreeGroupFactorMain.WeightedFock.normalizedResidual line 27
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedResidual_filled_covariance line 30
  4. def OAI.FreeGroupFactorMain.WeightedFock.residualPair line 42
  5. theorem OAI.FreeGroupFactorMain.WeightedFock.residualPair_eq line 45
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.residualPair_mem_ambient line 49
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedResidual_paired_mem line 55
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.residualPair_none_none line 61
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.residualLeg_sum line 67
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.filledLabel_generation line 72
  11. theorem OAI.FreeGroupFactorMain.GaussianExtension.orthogonality_extension line 103
  12. def OAI.FreeGroupFactorMain.GaussianOrthogonal.Relation line 119
  13. theorem OAI.FreeGroupFactorMain.GaussianOrthogonal.symm line 121
  14. theorem OAI.FreeGroupFactorMain.GaussianOrthogonal.sandwich_left line 126
  15. theorem OAI.FreeGroupFactorMain.GaussianOrthogonal.sandwich_right line 133
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_edge_orthogonal line 140
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.splitBlock_weightedDefect line 147
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_diagonal_filled line 154
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_split_filled line 164
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.split_diagonal_filled line 176
  21. theorem OAI.FreeGroupFactorMain.GaussianOrthogonal.smul_left line 194
  22. theorem OAI.FreeGroupFactorMain.GaussianOrthogonal.smul_right line 197
  23. def OAI.FreeGroupFactorMain.WeightedFock.legAsFilled line 206
  24. def OAI.FreeGroupFactorMain.WeightedFock.residualLegAsFilled line 208
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.normalized_fresh_diagonal line 211
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.normalized_fresh_residual line 220
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.normalized_residual_diagonal line 235
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedCreation_annihilate line 250
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedResidual_annihilate line 256
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.transportedDiagonal_annihilate line 262
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedDiagonal_annihilate line 270