OAI/Probability/FreeIsing/Spectral/SpectralClosure.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.SpectralClosure.norm_apply_le_on_closure_range line 15
  2. def OAI.Problem367.SpectralClosure.rangeClosure line 22
  3. instance OAI.Problem367.SpectralClosure.rangeClosure_completeSpace line 25
  4. lemma OAI.Problem367.SpectralClosure.mem_rangeClosure line 29
  5. lemma OAI.Problem367.SpectralClosure.mapsTo_rangeClosure line 34
  6. def OAI.Problem367.SpectralClosure.restrict line 42
  7. lemma OAI.Problem367.SpectralClosure.restrict_isSymmetric line 46
  8. lemma OAI.Problem367.SpectralClosure.restrict_isSelfAdjoint line 52
  9. lemma OAI.Problem367.SpectralClosure.mapsTo_orthogonal_rangeClosure line 57
  10. lemma OAI.Problem367.SpectralClosure.norm_restrict_le line 69
  11. lemma OAI.Problem367.SpectralClosure.range_domRestrict_eq line 78
  12. lemma OAI.Problem367.SpectralClosure.rangeClosure_domRestrict_eq line 91
  13. lemma OAI.Problem367.SpectralClosure.source_cover_of_kills_direction line 99
  14. lemma OAI.Problem367.SpectralClosure.rangeClosure_ker_eq_of_kills_direction line 110
  15. lemma OAI.Problem367.SpectralClosure.norm_apply_le_of_source_subspace line 115
  16. lemma OAI.Problem367.SpectralClosure.norm_restrict_le_of_source_subspace line 126
  17. lemma OAI.Problem367.SpectralClosure.norm_restrict_le_of_kills_direction line 137