OAI/Dynamics/EntropyCounterexample/RawSpectrumFactor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.RawBase line 13
  2. def OAI.Problem340.rawBaseSquare line 15
  3. def OAI.Problem340.rawBaseProjection line 18
  4. def OAI.Problem340.rawFactorInclusion line 21
  5. theorem OAI.Problem340.continuous_rawBaseSquare line 25
  6. theorem OAI.Problem340.continuous_rawBaseProjection line 31
  7. theorem OAI.Problem340.continuous_rawFactorInclusion line 34
  8. theorem OAI.Problem340.rawNormalForm_eq_factor line 38
  9. theorem OAI.Problem340.rawProjection_factor_eq_square line 41
  10. theorem OAI.Problem340.rawUpdate_homology_pairRadii_subset line 44
  11. theorem OAI.Problem340.bddAbove_rawUpdate_homology_pairRadii line 55
  12. theorem OAI.Problem340.rawUpdate_homology_pairRadii_le_two_of_cubic line 68
  13. theorem OAI.Problem340.bddAbove_rawUpdate_homology_pairRadii_of_cubic line 82