OAI/Computability/MinUncut/Games/JointInner.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.RowNoise.maskProject_selfadjoint line 24
  2. lemma OAI.MinUncut.RowNoise.maskProject_idempotent line 32
  3. lemma OAI.MinUncut.RowNoise.maskProject_inner line 51
  4. lemma OAI.MinUncut.RowNoise.maskHermite_eq line 61
  5. def OAI.MinUncut.RowNoise.jointInner line 67
  6. def OAI.MinUncut.RowNoise.jointEnergy line 70
  7. lemma OAI.MinUncut.RowNoise.jointEnergy_nonneg line 74
  8. lemma OAI.MinUncut.RowNoise.jointInner_self line 78
  9. lemma OAI.MinUncut.RowNoise.jointInner_symm line 82
  10. lemma OAI.MinUncut.RowNoise.jointInner_maskHermite line 85
  11. lemma OAI.MinUncut.RowNoise.jointInner_source_component line 102
  12. lemma OAI.MinUncut.RowNoise.components_orthogonal line 115
  13. lemma OAI.MinUncut.RowNoise.jointInner_sum_right line 125
  14. lemma OAI.MinUncut.RowNoise.jointInner_sum_left line 138
  15. lemma OAI.MinUncut.RowNoise.selectedProject_source_inner line 145
  16. lemma OAI.MinUncut.RowNoise.selectedProject_energy line 152
  17. lemma OAI.MinUncut.RowNoise.jointEnergy_sub line 170
  18. theorem OAI.MinUncut.RowNoise.selectedProject_energy_le line 181
  19. lemma OAI.MinUncut.RowNoise.selectedProject_sdiff line 190
  20. lemma OAI.MinUncut.RowNoise.selectedProject_loss_energy line 198