OAI/Analysis/Crouzeix/SteinMetric.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Stein Metric.

  1. theorem OAI.CrouzeixHilbert.Metric.eventually_norm_pow_le line 19
  2. theorem OAI.CrouzeixHilbert.Metric.summable_norm_pow line 35
  3. def OAI.CrouzeixHilbert.Metric.steinSeries line 52
  4. theorem OAI.CrouzeixHilbert.Metric.summable_steinSeries line 55
  5. theorem OAI.CrouzeixHilbert.Metric.steinSeries_nonneg line 70
  6. theorem OAI.CrouzeixHilbert.Metric.steinSeries_eq_one_add line 74
  7. theorem OAI.CrouzeixHilbert.Metric.one_le_steinSeries line 87
  8. theorem OAI.CrouzeixHilbert.Metric.steinSeries_sub line 93
  9. theorem OAI.CrouzeixHilbert.Metric.exists_strict_stein_metric line 98
  10. structure OAI.CrouzeixHilbert.Metric.Feasible line 126
  11. theorem OAI.CrouzeixHilbert.Metric.Feasible.nonneg line 131
  12. theorem OAI.CrouzeixHilbert.Metric.Feasible.selfAdjoint line 134
  13. theorem OAI.CrouzeixHilbert.Metric.Feasible.isStrictlyPositive line 137
  14. theorem OAI.CrouzeixHilbert.Metric.Feasible.one_le line 142
  15. theorem OAI.CrouzeixHilbert.Metric.Feasible.norm_le line 146
  16. theorem OAI.CrouzeixHilbert.Metric.steinSeries_feasible line 150
  17. theorem OAI.CrouzeixHilbert.Metric.exists_minimizing_metric line 157
  18. theorem OAI.CrouzeixHilbert.Metric.norm_le_one_iff_star_mul_self_le line 193
  19. theorem OAI.CrouzeixHilbert.Metric.Feasible.sqrt_similarity line 201
  20. theorem OAI.CrouzeixHilbert.Metric.Feasible.sqrt_spectrum line 236
  21. theorem OAI.CrouzeixHilbert.Metric.feasible_of_contractive_similarity line 243
  22. theorem OAI.CrouzeixHilbert.Metric.optimal_similarity line 282