OAI/Analysis/Crouzeix/BoundaryFibers.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Boundary Fibers.

  1. theorem OAI.CrouzeixHilbert.Compression.fibres_of_integral_interpolation line 26
  2. def OAI.CrouzeixHilbert.matrixOperatorMap line 70
  3. theorem OAI.CrouzeixHilbert.matrixOperatorMap_apply line 73
  4. def OAI.CrouzeixHilbert.matrixBaseField line 76
  5. theorem OAI.CrouzeixHilbert.matrixBaseField_star_mul line 82
  6. theorem OAI.CrouzeixHilbert.matrixBaseField_mass line 91
  7. theorem OAI.CrouzeixHilbert.matrixBaseField_sandwich line 108
  8. theorem OAI.CrouzeixHilbert.norm_coefficientField_le_one line 118
  9. theorem OAI.CrouzeixHilbert.vectorization_inj line 128
  10. theorem OAI.CrouzeixHilbert.matrix_fibres_of_integral_interpolation line 137
  11. def OAI.CrouzeixHilbert.Boundary.matrixDensityRoot line 175
  12. theorem OAI.CrouzeixHilbert.Boundary.matrixDensityRoot_star_mul line 180
  13. theorem OAI.CrouzeixHilbert.Boundary.densityLp_ordered line 187
  14. theorem OAI.CrouzeixHilbert.Boundary.matrixMean_cross_zero line 209
  15. theorem OAI.CrouzeixHilbert.Boundary.trace_matrixMean_self_one line 214