OAI/Analysis/Unitarizability/AveragedForm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Dixmier.DayDixmier.coefficient line 16
  2. lemma OAI.Dixmier.DayDixmier.coefficient_apply line 27
  3. lemma OAI.Dixmier.DayDixmier.coefficient_norm_le line 30
  4. lemma OAI.Dixmier.DayDixmier.coefficient_add_left line 35
  5. lemma OAI.Dixmier.DayDixmier.coefficient_add_right line 40
  6. lemma OAI.Dixmier.DayDixmier.coefficient_smul_left line 45
  7. lemma OAI.Dixmier.DayDixmier.coefficient_smul_right line 50
  8. lemma OAI.Dixmier.DayDixmier.coefficient_translate line 55
  9. def OAI.Dixmier.DayDixmier.averagedForm line 60
  10. lemma OAI.Dixmier.DayDixmier.averagedForm_bound line 76
  11. lemma OAI.Dixmier.DayDixmier.averagedForm_nonneg line 88
  12. lemma OAI.Dixmier.DayDixmier.averagedForm_lower line 97