OAI/Combinatorics/TriangleRemoval/Process/IncidenceDegree.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpTerminalLeave.algebra_norm_exp_le line 21
  2. theorem OAI.SharpTerminalLeave.rectangular_power_swap line 38
  3. theorem OAI.SharpTerminalLeave.averaging_shift_exp_bound line 47
  4. theorem OAI.SharpTerminalLeave.rectangular_exp_swap line 75
  5. theorem OAI.SharpTerminalLeave.hasDerivAt_rectangular_exp line 91
  6. theorem OAI.SharpTerminalLeave.rectangular_semigroup_bound line 103
  7. theorem OAI.SharpTerminalLeave.matrix_norm_le_of_row_abs_sum_le line 139
  8. def OAI.SharpTerminalLeave.incidenceDegree line 151
  9. def OAI.SharpTerminalLeave.starAverage line 154
  10. theorem OAI.SharpTerminalLeave.incidence_norm_le_two line 157
  11. theorem OAI.SharpTerminalLeave.starAverage_nonneg line 164
  12. theorem OAI.SharpTerminalLeave.starAverage_row_sum line 169
  13. theorem OAI.SharpTerminalLeave.starAverage_norm_le_one line 176
  14. theorem OAI.SharpTerminalLeave.starAverage_mul_diagonal line 183
  15. theorem OAI.SharpTerminalLeave.starAverage_neighbor_norm line 192
  16. theorem OAI.SharpTerminalLeave.star_semigroup_bound line 218