OAI/Analysis/Steinitz/Coefficients.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Filtered coefficients and their quadratic energy bounds.

  1. lemma OAI.EuclideanSteinitz.Gain.relativeMoment_controls_gain line 12
  2. lemma OAI.EuclideanSteinitz.Gain.accumulated_gain_bound line 28
  3. def OAI.EuclideanSteinitz.PotentialScalar.rate line 73
  4. def OAI.EuclideanSteinitz.PotentialScalar.primitive line 74
  5. lemma OAI.EuclideanSteinitz.PotentialScalar.continuous_rate line 76
  6. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_nonneg line 84
  7. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_small line 86
  8. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_large line 92
  9. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_eq line 101
  10. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_zero_of_nonpos line 109
  11. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_eq line 112
  12. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_derivative line 118
  13. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_monotone line 123
  14. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_zero_of_nonpos line 127
  15. lemma OAI.EuclideanSteinitz.PotentialScalar.large_add_linear_monotone line 137
  16. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_add_linear_monotone line 158
  17. lemma OAI.EuclideanSteinitz.PotentialScalar.convexified_derivative line 179
  18. lemma OAI.EuclideanSteinitz.PotentialScalar.convexified_convex line 183
  19. lemma OAI.EuclideanSteinitz.PotentialScalar.sizeWeight_small line 196
  20. lemma OAI.EuclideanSteinitz.PotentialScalar.sizeWeight_large line 203
  21. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_small line 207
  22. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_nonneg line 214
  23. lemma OAI.EuclideanSteinitz.PotentialScalar.primitive_sub_le line 220
  24. lemma OAI.EuclideanSteinitz.PotentialScalar.rate_le_inverse_sq line 230
  25. lemma OAI.EuclideanSteinitz.PotentialScalar.direct_scalar_bound line 236
  26. lemma OAI.EuclideanSteinitz.Spectral.trace_primitive_monotone line 295
  27. lemma OAI.EuclideanSteinitz.Spectral.cfc_primitive_eq line 309
  28. lemma OAI.EuclideanSteinitz.Spectral.trace_potential_direct line 315
  29. lemma OAI.EuclideanSteinitz.Endpoint.diag_le line 358
  30. lemma OAI.EuclideanSteinitz.Endpoint.diagonalize line 362
  31. lemma OAI.EuclideanSteinitz.Endpoint.inverse_spectral line 369
  32. lemma OAI.EuclideanSteinitz.Endpoint.sandwich_diagonal_apply line 376
  33. lemma OAI.EuclideanSteinitz.Endpoint.overlap_conjugate line 383
  34. lemma OAI.EuclideanSteinitz.Endpoint.overlap_row_weight line 392
  35. lemma OAI.EuclideanSteinitz.Endpoint.overlap_inverse_conjugate line 400
  36. lemma OAI.EuclideanSteinitz.Endpoint.diagonalize_inverse line 408
  37. lemma OAI.EuclideanSteinitz.Endpoint.overlap_col_inverse_weight line 415
  38. lemma OAI.EuclideanSteinitz.Endpoint.overlap_ratio_row line 430
  39. lemma OAI.EuclideanSteinitz.Endpoint.overlap_ratio_col line 437
  40. lemma OAI.EuclideanSteinitz.Endpoint.trace_cfc_mul_diag line 452
  41. lemma OAI.EuclideanSteinitz.Endpoint.gain_new_coordinates line 466
  42. lemma OAI.EuclideanSteinitz.Endpoint.gain_endpoint line 481
  43. def OAI.EuclideanSteinitz.Endpoint.transportBasis line 504
  44. lemma OAI.EuclideanSteinitz.Endpoint.transport_row_matrix line 508
  45. lemma OAI.EuclideanSteinitz.Endpoint.transport_col_matrix line 516
  46. lemma OAI.EuclideanSteinitz.Endpoint.transport_row_bound line 524
  47. lemma OAI.EuclideanSteinitz.Endpoint.transport_col_bound line 533
  48. lemma OAI.EuclideanSteinitz.Endpoint.transport_spectral line 543
  49. lemma OAI.EuclideanSteinitz.Endpoint.transport_row_weight line 551
  50. lemma OAI.EuclideanSteinitz.Endpoint.congruence_inverse line 557
  51. lemma OAI.EuclideanSteinitz.Endpoint.transport_inverse_spectral line 566
  52. lemma OAI.EuclideanSteinitz.Endpoint.transport_col_inverse_weight line 575
  53. lemma OAI.EuclideanSteinitz.Endpoint.transport_ratio_row line 587
  54. lemma OAI.EuclideanSteinitz.Endpoint.transport_ratio_col line 593
  55. lemma OAI.EuclideanSteinitz.Endpoint.trace_cfc_transport_product line 607
  56. lemma OAI.EuclideanSteinitz.Endpoint.contraction_distance_identity line 627
  57. lemma OAI.EuclideanSteinitz.Endpoint.contraction_endpoint_spectral line 658
  58. def OAI.EuclideanSteinitz.Coefficient.lift line 691
  59. def OAI.EuclideanSteinitz.Coefficient.weightedSq line 694
  60. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_nonneg line 698
  61. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_weight_add line 705
  62. lemma OAI.EuclideanSteinitz.Coefficient.weighted_cross_symm line 710
  63. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_sub line 716
  64. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_triangle line 724
  65. lemma OAI.EuclideanSteinitz.Coefficient.lift_transpose line 735
  66. lemma OAI.EuclideanSteinitz.Coefficient.lift_sub line 740
  67. lemma OAI.EuclideanSteinitz.Coefficient.weighted_lift_cross line 745
  68. lemma OAI.EuclideanSteinitz.Coefficient.weighted_lift line 754
  69. lemma OAI.EuclideanSteinitz.Coefficient.cfc_transpose line 760
  70. lemma OAI.EuclideanSteinitz.Coefficient.cfc_square line 766
  71. lemma OAI.EuclideanSteinitz.Coefficient.cfc_affine line 776
  72. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_cfc line 781
  73. lemma OAI.EuclideanSteinitz.Coefficient.cfc_mul_same line 787
  74. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_cfc_affine line 793
  75. lemma OAI.EuclideanSteinitz.Coefficient.contraction_endpoint line 801
  76. lemma OAI.EuclideanSteinitz.Coefficient.weightedSq_sub_zero line 823
  77. lemma OAI.EuclideanSteinitz.Coefficient.gain_endpoint_lift line 829
  78. lemma OAI.EuclideanSteinitz.Coefficient.endpoint_comparison line 844