OAI/Analysis/Steinitz/MatrixEnergy.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Scalar potentials and spectral endpoint inequalities.

  1. def OAI.EuclideanSteinitz.MatrixEnergy.exponent line 12
  2. def OAI.EuclideanSteinitz.MatrixEnergy.cutoff line 14
  3. def OAI.EuclideanSteinitz.MatrixEnergy.weight line 18
  4. def OAI.EuclideanSteinitz.MatrixEnergy.potential line 20
  5. def OAI.EuclideanSteinitz.MatrixEnergy.gainPotential line 23
  6. def OAI.EuclideanSteinitz.MatrixEnergy.sizeWeight line 26
  7. def OAI.EuclideanSteinitz.MatrixEnergy.scalarRemainder line 28
  8. lemma OAI.EuclideanSteinitz.MatrixEnergy.exponent_pos line 33
  9. lemma OAI.EuclideanSteinitz.MatrixEnergy.weight_of_le_one line 35
  10. lemma OAI.EuclideanSteinitz.MatrixEnergy.weight_of_one_le line 42
  11. lemma OAI.EuclideanSteinitz.MatrixEnergy.integrand_of_le_one line 47
  12. lemma OAI.EuclideanSteinitz.MatrixEnergy.integrand_of_one_le line 53
  13. lemma OAI.EuclideanSteinitz.MatrixEnergy.potential_small line 59
  14. lemma OAI.EuclideanSteinitz.MatrixEnergy.small_integrable line 72
  15. lemma OAI.EuclideanSteinitz.MatrixEnergy.large_integrable line 80
  16. lemma OAI.EuclideanSteinitz.MatrixEnergy.potential_large line 92
  17. lemma OAI.EuclideanSteinitz.MatrixEnergy.fourth_rpow_exponent line 114
  18. def OAI.EuclideanSteinitz.MatrixEnergy.rootWeight line 119
  19. lemma OAI.EuclideanSteinitz.MatrixEnergy.weight_fourth line 122
  20. lemma OAI.EuclideanSteinitz.MatrixEnergy.root_endpoint line 132
  21. lemma OAI.EuclideanSteinitz.MatrixEnergy.root_remainder line 184
  22. lemma OAI.EuclideanSteinitz.MatrixEnergy.fourth_ratio_polynomial line 195
  23. lemma OAI.EuclideanSteinitz.MatrixEnergy.weight_nonneg line 202
  24. lemma OAI.EuclideanSteinitz.MatrixEnergy.root_remainder_quadratic line 205
  25. lemma OAI.EuclideanSteinitz.MatrixEnergy.scalar_remainder_lower line 221
  26. lemma OAI.EuclideanSteinitz.MatrixEnergy.scalar_remainder_nonneg line 234
  27. lemma OAI.EuclideanSteinitz.MatrixEnergy.scalar_remainder_reverse_lower line 241
  28. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_nonneg line 250
  29. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_le_one line 254
  30. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_dist_le_one line 258
  31. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_dist_of_le line 265
  32. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_dist line 271
  33. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_zero_of_not_band line 278
  34. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_ne_band line 282
  35. lemma OAI.EuclideanSteinitz.MatrixEnergy.weight_band line 288
  36. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_weighted_distance line 297
  37. lemma OAI.EuclideanSteinitz.MatrixEnergy.scalar_comparison line 341
  38. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_square_le_weight line 366
  39. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_weighted_square_le_weight line 378
  40. lemma OAI.EuclideanSteinitz.MatrixEnergy.cutoff_scaled_square_le_weight line 393
  41. lemma OAI.EuclideanSteinitz.MatrixEnergy.sum_row line 414
  42. lemma OAI.EuclideanSteinitz.MatrixEnergy.sum_col line 418
  43. lemma OAI.EuclideanSteinitz.MatrixEnergy.contraction_deficit_identity line 423
  44. lemma OAI.EuclideanSteinitz.MatrixEnergy.contraction_spectral_bound line 446
  45. lemma OAI.EuclideanSteinitz.MatrixEnergy.gain_deficit_identity line 485
  46. lemma OAI.EuclideanSteinitz.MatrixEnergy.gain_spectral_bound line 508
  47. def OAI.EuclideanSteinitz.MatrixEnergy.hsSquared line 546
  48. lemma OAI.EuclideanSteinitz.MatrixEnergy.hermitian_dot line 550
  49. lemma OAI.EuclideanSteinitz.MatrixEnergy.le_of_square_le line 557
  50. lemma OAI.EuclideanSteinitz.MatrixEnergy.sqrt_le_sqrt line 595
  51. lemma OAI.EuclideanSteinitz.MatrixEnergy.inv_le_inv line 600
  52. lemma OAI.EuclideanSteinitz.MatrixEnergy.trace_mul_nonneg line 617
  53. lemma OAI.EuclideanSteinitz.MatrixEnergy.trace_mul_mono_right line 626