OAI/Analysis/Steinitz/Gain.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Contraction and gain potentials for positive semidefinite matrices.

  1. lemma OAI.EuclideanSteinitz.Gain.transpose_bound line 12
  2. lemma OAI.EuclideanSteinitz.Gain.cube_le_eight line 26
  3. lemma OAI.EuclideanSteinitz.Gain.relative_sqrt_bound line 38
  4. def OAI.EuclideanSteinitz.Gain.inverseSqrt line 107
  5. lemma OAI.EuclideanSteinitz.Gain.inverseSqrt_psd line 109
  6. lemma OAI.EuclideanSteinitz.Gain.inverseSqrt_transpose line 112
  7. lemma OAI.EuclideanSteinitz.Gain.sqrt_transpose line 115
  8. lemma OAI.EuclideanSteinitz.Gain.inverseSqrt_mul_sqrt line 118
  9. lemma OAI.EuclideanSteinitz.Gain.sqrt_mul_inverseSqrt line 124
  10. lemma OAI.EuclideanSteinitz.Gain.inverseSqrt_sandwich line 130
  11. lemma OAI.EuclideanSteinitz.Gain.inverseSqrt_unit line 138
  12. lemma OAI.EuclideanSteinitz.Gain.congruence_mono line 143
  13. lemma OAI.EuclideanSteinitz.Gain.trace_power_bound line 149
  14. lemma OAI.EuclideanSteinitz.Gain.direct_coefficient_bound line 162
  15. def OAI.EuclideanSteinitz.GainScalar.rate line 223
  16. def OAI.EuclideanSteinitz.GainScalar.extendedRate line 226
  17. def OAI.EuclideanSteinitz.GainScalar.primitive line 228
  18. lemma OAI.EuclideanSteinitz.GainScalar.rate_eq line 230
  19. lemma OAI.EuclideanSteinitz.GainScalar.extendedRate_eq line 239
  20. lemma OAI.EuclideanSteinitz.GainScalar.continuous_extendedRate line 242
  21. lemma OAI.EuclideanSteinitz.GainScalar.rate_continuousOn line 246
  22. lemma OAI.EuclideanSteinitz.GainScalar.primitive_eq line 251
  23. lemma OAI.EuclideanSteinitz.GainScalar.primitive_derivative line 257
  24. lemma OAI.EuclideanSteinitz.GainScalar.rate_derivative line 263
  25. lemma OAI.EuclideanSteinitz.GainScalar.rate_derivative_lower line 278
  26. lemma OAI.EuclideanSteinitz.GainScalar.rate_add_linear_monotone line 292
  27. lemma OAI.EuclideanSteinitz.GainScalar.extendedRate_add_linear_monotone line 304
  28. lemma OAI.EuclideanSteinitz.GainScalar.convexified_derivative line 320
  29. lemma OAI.EuclideanSteinitz.GainScalar.convexified_convex line 324
  30. lemma OAI.EuclideanSteinitz.Gain.finite_spectrum_continuous line 339
  31. lemma OAI.EuclideanSteinitz.Gain.sqrt_eq_cfc_real line 344
  32. lemma OAI.EuclideanSteinitz.Gain.inverseSqrt_add_one line 351
  33. lemma OAI.EuclideanSteinitz.Gain.relative_rate_coefficient line 364
  34. lemma OAI.EuclideanSteinitz.Gain.direct_coefficient_bound_rate line 397
  35. lemma OAI.EuclideanSteinitz.Spectral.trace_semiconvex_affine_derivative line 412
  36. lemma OAI.EuclideanSteinitz.Spectral.trace_gainPotential_affine_derivative line 440
  37. def OAI.EuclideanSteinitz.Gain.relativeMoment line 472
  38. def OAI.EuclideanSteinitz.Gain.gainValue line 475
  39. def OAI.EuclideanSteinitz.Gain.gainConstant line 477
  40. lemma OAI.EuclideanSteinitz.Gain.two_rpow_exponent line 479
  41. lemma OAI.EuclideanSteinitz.Gain.gainConstant_pos line 486
  42. lemma OAI.EuclideanSteinitz.Gain.sandwich_psd line 490
  43. lemma OAI.EuclideanSteinitz.Gain.sandwich_affine line 495
  44. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_derivative line 500
  45. lemma OAI.EuclideanSteinitz.Gain.gainValue_derivative line 532
  46. lemma OAI.EuclideanSteinitz.Gain.rate_nonneg line 545
  47. lemma OAI.EuclideanSteinitz.Gain.gainValue_monotone line 554
  48. lemma OAI.EuclideanSteinitz.Gain.gain_derivative_bound line 565
  49. lemma OAI.EuclideanSteinitz.conditional_derivative_comparison line 590
  50. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_gain line 627
  51. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_nonneg line 673
  52. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_zero line 681
  53. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_contraction line 685
  54. structure OAI.EuclideanSteinitz.Gain.Move line 732
  55. def OAI.EuclideanSteinitz.Gain.Move.old line 736
  56. def OAI.EuclideanSteinitz.Gain.Move.next line 739
  57. def OAI.EuclideanSteinitz.Gain.Move.Admissible line 741
  58. def OAI.EuclideanSteinitz.Gain.follow line 744
  59. def OAI.EuclideanSteinitz.Gain.gainCost line 748
  60. lemma OAI.EuclideanSteinitz.Gain.Move.old_add line 753
  61. lemma OAI.EuclideanSteinitz.Gain.Move.old_psd line 757
  62. lemma OAI.EuclideanSteinitz.Gain.Move.next_psd line 762
  63. lemma OAI.EuclideanSteinitz.Gain.Move.gain_nonneg line 765
  64. lemma OAI.EuclideanSteinitz.Gain.gainCost_nonneg line 771
  65. lemma OAI.EuclideanSteinitz.Gain.follow_psd line 780
  66. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_path line 789