OAI/Combinatorics/ThinTrees/SpectralPacking.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.Spectral.frobSq line 18
  2. lemma OAI.StrongThinTree.Spectral.frobSq_eq_sum line 20
  3. lemma OAI.StrongThinTree.Spectral.frobSq_nonneg line 25
  4. lemma OAI.StrongThinTree.Spectral.frobSq_adjoint line 29
  5. lemma OAI.StrongThinTree.Spectral.trace_bound line 33
  6. lemma OAI.StrongThinTree.Spectral.norm_eigenvector line 43
  7. lemma OAI.StrongThinTree.Spectral.trace_le_singular_sum line 54
  8. lemma OAI.StrongThinTree.Spectral.frobSq_eq_singular_sum line 58
  9. lemma OAI.StrongThinTree.Spectral.projection_symmetric line 63
  10. lemma OAI.StrongThinTree.Spectral.projection_sq line 67
  11. lemma OAI.StrongThinTree.Spectral.projection_trace line 72
  12. lemma OAI.StrongThinTree.Spectral.projection_inner line 77
  13. lemma OAI.StrongThinTree.Spectral.frobSq_projection_le line 82
  14. lemma OAI.StrongThinTree.Spectral.frobSq_projection line 89
  15. lemma OAI.StrongThinTree.Spectral.weighted_tail_le line 103
  16. lemma OAI.StrongThinTree.Spectral.eigenvalue_eq_singular_sq line 161
  17. lemma OAI.StrongThinTree.Spectral.trace_adjoint line 172
  18. lemma OAI.StrongThinTree.Spectral.frobSq_projection_eigenbasis line 180
  19. lemma OAI.StrongThinTree.Spectral.rank_approximation line 198
  20. lemma OAI.StrongThinTree.Spectral.separated_net line 243
  21. lemma OAI.StrongThinTree.Spectral.norm_sub_sq_le_twice line 285
  22. lemma OAI.StrongThinTree.Spectral.range_le_of_basis line 293
  23. lemma OAI.StrongThinTree.Spectral.difference_span_rank line 305
  24. lemma OAI.StrongThinTree.Spectral.spectral_centers_at_radius line 326
  25. def OAI.StrongThinTree.Spectral.tail line 389
  26. def OAI.StrongThinTree.Spectral.block line 390
  27. lemma OAI.StrongThinTree.Spectral.tail_split line 392
  28. lemma OAI.StrongThinTree.Spectral.block_sq_le line 405
  29. lemma OAI.StrongThinTree.Spectral.dyadic_tail_selection line 435
  30. lemma OAI.StrongThinTree.Spectral.singular_tail_selection line 486
  31. lemma OAI.StrongThinTree.Spectral.trace_sq_le_frobSq line 563
  32. lemma OAI.StrongThinTree.Spectral.spectral_packing_log line 576
  33. lemma OAI.StrongThinTree.Spectral.logarithmic_power_bound line 661
  34. lemma OAI.StrongThinTree.Spectral.spectral_packing_power line 699
  35. theorem OAI.StrongThinTree.Spectral.spectral_packing_coordinates line 738