OAI/Analysis/Crouzeix/Compression.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Compression.

  1. def OAI.CrouzeixHilbert.Compression.fieldAction line 20
  2. theorem OAI.CrouzeixHilbert.Compression.fieldAction_apply_ae line 50
  3. theorem OAI.CrouzeixHilbert.Compression.norm_fieldAction_le line 57
  4. theorem OAI.CrouzeixHilbert.Compression.adjoint_fieldAction line 69
  5. def OAI.CrouzeixHilbert.Compression.orbit line 93
  6. def OAI.CrouzeixHilbert.Compression.lift line 98
  7. theorem OAI.CrouzeixHilbert.Compression.lift_apply_ae line 102
  8. theorem OAI.CrouzeixHilbert.Compression.inner_lift line 106
  9. def OAI.CrouzeixHilbert.Compression.isometry line 120
  10. theorem OAI.CrouzeixHilbert.Compression.isometry_apply line 124
  11. theorem OAI.CrouzeixHilbert.Compression.integral_eq_compression line 128
  12. theorem OAI.CrouzeixHilbert.Compression.norm_integral_le line 152
  13. def OAI.CrouzeixHilbert.Compression.densityRoot line 170
  14. theorem OAI.CrouzeixHilbert.Compression.densityRoot_star_mul line 175
  15. def OAI.CrouzeixHilbert.Compression.densityIsometry line 180
  16. theorem OAI.CrouzeixHilbert.Compression.densityIsometry_apply_ae line 184