OAI/Combinatorics/Coboundary/Spectral.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Self-adjoint operator estimates and the weighted-graph spectral trickling argument.

  1. lemma OAI.CoboundaryExpanders.Spectral.eigenvalue_trickle line 19
  2. theorem OAI.CoboundaryExpanders.Spectral.operator_trickle line 28
  3. structure OAI.CoboundaryExpanders.Spectral.WeightedGraph line 72
  4. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.mass line 82
  5. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.energy line 83
  6. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.pairing line 84
  7. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.action line 85
  8. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.Connected line 86
  9. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.mass_pos line 88
  10. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.mass_ne line 89
  11. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.energy_nonneg line 90
  12. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.swapped_energy line 93
  13. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.energy_difference line 103
  14. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.pairing_le_energy line 120
  15. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.action_pairing line 127
  16. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.fixed_constant line 141
  17. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.coord line 165
  18. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.uncoord line 166
  19. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.matrix line 167
  20. def OAI.CoboundaryExpanders.Spectral.WeightedGraph.operator line 168
  21. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.sqrt_ne line 170
  22. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.coord_uncoord line 171
  23. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.uncoord_coord line 174
  24. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.coord_inner line 178
  25. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.operator_coord line 187
  26. lemma OAI.CoboundaryExpanders.Spectral.WeightedGraph.operator_symmetric line 199
  27. theorem OAI.CoboundaryExpanders.Spectral.WeightedGraph.trickle line 205