OAI/Analysis/Crouzeix/DensityCompatibility.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Density Compatibility.

  1. def OAI.CrouzeixHilbert.Boundary.toHSCLM line 20
  2. theorem OAI.CrouzeixHilbert.Boundary.toHSCLM_apply line 26
  3. def OAI.CrouzeixHilbert.Boundary.weightedPartialTraceCLM line 28
  4. theorem OAI.CrouzeixHilbert.Boundary.weightedPartialTraceCLM_apply line 34
  5. theorem OAI.CrouzeixHilbert.Boundary.integral_weightedPartialTrace line 37
  6. def OAI.CrouzeixHilbert.Boundary.densityContinuous line 43
  7. def OAI.CrouzeixHilbert.Boundary.densityLp line 48
  8. theorem OAI.CrouzeixHilbert.Boundary.densityLp_apply_ae line 51
  9. theorem OAI.CrouzeixHilbert.Boundary.matrixMean_densityLp line 55
  10. theorem OAI.CrouzeixHilbert.Boundary.matrixMean_densityLp_mass_one line 74
  11. theorem OAI.CrouzeixHilbert.Boundary.densityLp_block_posSemidef line 79
  12. theorem OAI.CrouzeixHilbert.Boundary.densityLp_self_hermitian line 95
  13. theorem OAI.CrouzeixHilbert.inner_vectorization line 106
  14. theorem OAI.CrouzeixHilbert.weightedPartialTrace_testing line 116