OAI/Analysis/TriangularHilbert/MatrixSupport.lean

GitHub source file

207 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TriangularHilbert.MatrixEnergy.cyclic_sum_insert line 12
  2. theorem OAI.TriangularHilbert.MatrixEnergy.norm_quad_sum_le line 42
  3. theorem OAI.TriangularHilbert.MatrixEnergy.column_sq_sum_le line 61
  4. theorem OAI.TriangularHilbert.MatrixEnergy.row_sq_sum_le line 71
  5. theorem OAI.TriangularHilbert.MatrixEnergy.hermitian_entry_le line 79
  6. theorem OAI.TriangularHilbert.MatrixEnergy.norm_cyclic_tail_le line 86
  7. theorem OAI.TriangularHilbert.MatrixEnergy.norm_weighted_row_le line 113
  8. theorem OAI.TriangularHilbert.MatrixEnergy.norm_twice_tail_le line 135
  9. def OAI.TriangularHilbert.MatrixEnergy.spectralWeight line 159
  10. theorem OAI.TriangularHilbert.MatrixEnergy.spectralWeight_symm line 162
  11. theorem OAI.TriangularHilbert.MatrixEnergy.spectralWeight_diag line 169
  12. theorem OAI.TriangularHilbert.MatrixEnergy.spectralWeight_pair_ge line 178
  13. def OAI.TriangularHilbert.MatrixEnergy.cubicTerm line 192
  14. theorem OAI.TriangularHilbert.MatrixEnergy.cubicTerm_cyclic line 195
  15. theorem OAI.TriangularHilbert.MatrixEnergy.norm_cubicTerm_diag_le line 198
  16. theorem OAI.TriangularHilbert.MatrixEnergy.norm_cubicTerm_twice_le line 210
  17. theorem OAI.TriangularHilbert.MatrixEnergy.norm_cubicTerm_once_le line 223
  18. theorem OAI.TriangularHilbert.MatrixEnergy.spectralWeight_insert_ge line 243
  19. theorem OAI.TriangularHilbert.MatrixEnergy.norm_cubic_sum_le line 265
  20. theorem OAI.TriangularHilbert.MatrixEnergy.trace_cube_mul_diagonal line 306
  21. theorem OAI.TriangularHilbert.MatrixEnergy.norm_trace_cube_mul_diagonal_le line 326
  22. def OAI.TriangularHilbert.MatrixEnergy.traceReal line 342
  23. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_add line 344
  24. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_sub line 346
  25. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_smul line 348
  26. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_zero line 350
  27. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_star line 351
  28. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_mul_comm line 353
  29. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_mul_cycle line 355
  30. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_nonneg line 358
  31. def OAI.TriangularHilbert.MatrixEnergy.hsReal line 361
  32. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_add_left line 363
  33. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_add_right line 366
  34. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_sub_left line 369
  35. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_sub_right line 372
  36. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_smul_left line 375
  37. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_smul_right line 378
  38. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_zero_right line 381
  39. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_symm line 383
  40. def OAI.TriangularHilbert.MatrixEnergy.sylv line 387
  41. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_add_right line 389
  42. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_sub_right line 391
  43. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_smul_right line 393
  44. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_smul_left line 395
  45. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_sub_left line 397
  46. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_zero_right line 399
  47. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_sylv_symm line 401
  48. def OAI.TriangularHilbert.MatrixEnergy.penalty line 408
  49. theorem OAI.TriangularHilbert.MatrixEnergy.penalty_nonneg line 410
  50. theorem OAI.TriangularHilbert.MatrixEnergy.penalty_sub line 420
  51. theorem OAI.TriangularHilbert.MatrixEnergy.penalty_mono line 427
  52. def OAI.TriangularHilbert.MatrixEnergy.variation line 432
  53. def OAI.TriangularHilbert.MatrixEnergy.rootCost line 434
  54. theorem OAI.TriangularHilbert.MatrixEnergy.variation_sylv line 436
  55. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_eq_of_solution line 442
  56. theorem OAI.TriangularHilbert.MatrixEnergy.variation_bddAbove line 457
  57. theorem OAI.TriangularHilbert.MatrixEnergy.variation_le_rootCost line 465
  58. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_nonneg line 471
  59. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_antitone line 475
  60. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_scale line 484
  61. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_eq_sum line 494
  62. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_diagonal_apply line 502
  63. def OAI.TriangularHilbert.MatrixEnergy.diagonalSolution line 509
  64. theorem OAI.TriangularHilbert.MatrixEnergy.diagonalSolution_solves line 512
  65. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_diagonal line 521
  66. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_unitary_conj line 537
  67. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_unitary_conj line 543
  68. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_unitary_conj line 549
  69. theorem OAI.TriangularHilbert.MatrixEnergy.variation_unitary_conj line 553
  70. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_unitary_conj line 558
  71. def OAI.TriangularHilbert.MatrixEnergy.hessianCost line 570
  72. theorem OAI.TriangularHilbert.MatrixEnergy.exists_sylv_solution line 572
  73. theorem OAI.TriangularHilbert.MatrixEnergy.exists_sylv_solution_posDef line 591
  74. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_antitone line 598
  75. def OAI.TriangularHilbert.MatrixEnergy.sylvLinear line 603
  76. def OAI.TriangularHilbert.MatrixEnergy.sylvEquiv line 608
  77. theorem OAI.TriangularHilbert.MatrixEnergy.hasFDerivAt_square line 614
  78. theorem OAI.TriangularHilbert.MatrixEnergy.contDiff_square line 618
  79. theorem OAI.TriangularHilbert.MatrixEnergy.sqrt_smul line 621
  80. theorem OAI.TriangularHilbert.MatrixEnergy.sqrt_smoothWithin_posDef line 627
  81. def OAI.TriangularHilbert.MatrixEnergy.traceRealCLM line 657
  82. theorem OAI.TriangularHilbert.MatrixEnergy.traceRealCLM_apply line 664
  83. def OAI.TriangularHilbert.MatrixEnergy.energy line 667
  84. def OAI.TriangularHilbert.MatrixEnergy.energyGradient line 669
  85. theorem OAI.TriangularHilbert.MatrixEnergy.energyGradient_apply line 672
  86. theorem OAI.TriangularHilbert.MatrixEnergy.traceReal_mul_sylv line 675
  87. theorem OAI.TriangularHilbert.MatrixEnergy.energy_hasFDerivWithinAt line 682
  88. theorem OAI.TriangularHilbert.MatrixEnergy.hsReal_single line 705
  89. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_diagonal_single line 709
  90. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_solvable_diagonal_of_bddAbove line 721
  91. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_solvable_of_bddAbove line 747
  92. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_solvable_mono line 772
  93. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_smul_direction line 782
  94. theorem OAI.TriangularHilbert.MatrixEnergy.penalty_three_identity line 792
  95. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_three_le line 800
  96. theorem OAI.TriangularHilbert.MatrixEnergy.gram_diag_eq_zero_iff line 823
  97. theorem OAI.TriangularHilbert.MatrixEnergy.sylv_solvable_inserted_gram line 830
  98. theorem OAI.TriangularHilbert.MatrixEnergy.trace_unitary_conj line 872
  99. theorem OAI.TriangularHilbert.MatrixEnergy.norm_unitary_conj line 877
  100. theorem OAI.TriangularHilbert.MatrixEnergy.hermitian_unitary_conj line 882
  101. theorem OAI.TriangularHilbert.MatrixEnergy.sqrt_unitary_conj line 889
  102. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_unitary_conj line 898
  103. theorem OAI.TriangularHilbert.MatrixEnergy.sqrt_diagonal_square line 904
  104. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_diagonal_square line 917
  105. theorem OAI.TriangularHilbert.MatrixEnergy.norm_trace_cube_le_hessian line 942
  106. abbrev OAI.TriangularHilbert.MatrixEnergy.Three line 976
  107. abbrev OAI.TriangularHilbert.MatrixEnergy.BlockSpace line 977
  108. abbrev OAI.TriangularHilbert.MatrixEnergy.blocks line 978
  109. theorem OAI.TriangularHilbert.MatrixEnergy.blocks_mul line 982
  110. theorem OAI.TriangularHilbert.MatrixEnergy.blocks_star line 987
  111. theorem OAI.TriangularHilbert.MatrixEnergy.blocks_trace line 991
  112. def OAI.TriangularHilbert.MatrixEnergy.triangleBlocks line 995
  113. def OAI.TriangularHilbert.MatrixEnergy.triangle line 1000
  114. def OAI.TriangularHilbert.MatrixEnergy.blockD line 1001
  115. theorem OAI.TriangularHilbert.MatrixEnergy.triangle_hermitian line 1004
  116. theorem OAI.TriangularHilbert.MatrixEnergy.blockD_hermitian line 1013
  117. theorem OAI.TriangularHilbert.MatrixEnergy.triangle_trace_cube line 1021
  118. def OAI.TriangularHilbert.MatrixEnergy.vertexProj line 1053
  119. theorem OAI.TriangularHilbert.MatrixEnergy.vertexProj_hermitian line 1057
  120. theorem OAI.TriangularHilbert.MatrixEnergy.vertexProj_sq line 1063
  121. theorem OAI.TriangularHilbert.MatrixEnergy.sum_vertexProj line 1070
  122. theorem OAI.TriangularHilbert.MatrixEnergy.vertexProj_commute_blockD line 1077
  123. def OAI.TriangularHilbert.MatrixEnergy.rowStar line 1086
  124. def OAI.TriangularHilbert.MatrixEnergy.starGram line 1088
  125. def OAI.TriangularHilbert.MatrixEnergy.starInsert line 1090
  126. theorem OAI.TriangularHilbert.MatrixEnergy.starGram_eq line 1093
  127. theorem OAI.TriangularHilbert.MatrixEnergy.starInsert_eq line 1099
  128. theorem OAI.TriangularHilbert.MatrixEnergy.sum_starGram line 1110
  129. theorem OAI.TriangularHilbert.MatrixEnergy.sum_starInsert line 1115
  130. theorem OAI.TriangularHilbert.MatrixEnergy.starGram_le line 1120
  131. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_common_three line 1133
  132. theorem OAI.TriangularHilbert.MatrixEnergy.triangle_common_metric line 1148
  133. theorem OAI.TriangularHilbert.MatrixEnergy.triangle_real_trace_le line 1155
  134. def OAI.TriangularHilbert.MatrixEnergy.diagonalUnitary line 1175
  135. theorem OAI.TriangularHilbert.MatrixEnergy.insertedCost_right_unitary line 1188
  136. def OAI.TriangularHilbert.MatrixEnergy.phaseEdge line 1198
  137. def OAI.TriangularHilbert.MatrixEnergy.rowPhase line 1201
  138. theorem OAI.TriangularHilbert.MatrixEnergy.rowPhase_norm line 1206
  139. theorem OAI.TriangularHilbert.MatrixEnergy.rowStar_phase line 1211
  140. theorem OAI.TriangularHilbert.MatrixEnergy.starCost_phase line 1219
  141. theorem OAI.TriangularHilbert.MatrixEnergy.exists_phase_norm line 1230
  142. theorem OAI.TriangularHilbert.MatrixEnergy.mixed_trace_le line 1242
  143. def OAI.TriangularHilbert.MatrixEnergy.regularize line 1263
  144. theorem OAI.TriangularHilbert.MatrixEnergy.regularize_posDef line 1266
  145. theorem OAI.TriangularHilbert.MatrixEnergy.regularize_posSemidef line 1271
  146. theorem OAI.TriangularHilbert.MatrixEnergy.continuous_sqrt_matrix line 1275
  147. theorem OAI.TriangularHilbert.MatrixEnergy.continuous_energyGram line 1280
  148. theorem OAI.TriangularHilbert.MatrixEnergy.energy_unitary_conj line 1288
  149. theorem OAI.TriangularHilbert.MatrixEnergy.sqrt_diagonal_nonneg line 1300
  150. theorem OAI.TriangularHilbert.MatrixEnergy.energy_diagonal line 1311
  151. theorem OAI.TriangularHilbert.MatrixEnergy.energy_spectral line 1315
  152. theorem OAI.TriangularHilbert.MatrixEnergy.energy_eq_of_charpoly_eq line 1321
  153. theorem OAI.TriangularHilbert.MatrixEnergy.energy_gram_flip line 1327
  154. lemma OAI.TriangularHilbert.MatrixEnergy.gradient_gram line 1338
  155. lemma OAI.TriangularHilbert.MatrixEnergy.energyGradient_gram line 1348
  156. lemma OAI.TriangularHilbert.MatrixEnergy.hsReal_nonneg_of_posSemidef line 1363
  157. lemma OAI.TriangularHilbert.MatrixEnergy.sylv_star line 1373
  158. lemma OAI.TriangularHilbert.MatrixEnergy.sylv_solution_isHermitian line 1378
  159. lemma OAI.TriangularHilbert.MatrixEnergy.posSemidef_of_sylv_posSemidef line 1385
  160. lemma OAI.TriangularHilbert.MatrixEnergy.rootCost_le_of_order_posDef line 1410
  161. lemma OAI.TriangularHilbert.MatrixEnergy.regularize_square line 1444
  162. lemma OAI.TriangularHilbert.MatrixEnergy.regularize_square_le line 1450
  163. lemma OAI.TriangularHilbert.MatrixEnergy.continuous_variation_left line 1458
  164. theorem OAI.TriangularHilbert.MatrixEnergy.rootCost_le_of_order line 1464
  165. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_inserted_gram_le line 1509
  166. lemma OAI.TriangularHilbert.MatrixEnergy.blockD_mul line 1545
  167. lemma OAI.TriangularHilbert.MatrixEnergy.blockD_star line 1551
  168. lemma OAI.TriangularHilbert.MatrixEnergy.blockD_posSemidef line 1557
  169. lemma OAI.TriangularHilbert.MatrixEnergy.sqrt_blockD line 1569
  170. lemma OAI.TriangularHilbert.MatrixEnergy.hsReal_blocks_blockD line 1580
  171. lemma OAI.TriangularHilbert.MatrixEnergy.sylv_blockD line 1587
  172. lemma OAI.TriangularHilbert.MatrixEnergy.rootCost_blockD_ge_diagonal line 1596
  173. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_le_of_le_smul line 1620
  174. def OAI.TriangularHilbert.MatrixEnergy.wideRow line 1641
  175. def OAI.TriangularHilbert.MatrixEnergy.gramRow line 1644
  176. def OAI.TriangularHilbert.MatrixEnergy.insertRow line 1645
  177. def OAI.TriangularHilbert.MatrixEnergy.pinchedRow line 1647
  178. lemma OAI.TriangularHilbert.MatrixEnergy.gramRow_eq line 1650
  179. lemma OAI.TriangularHilbert.MatrixEnergy.insertRow_eq line 1654
  180. lemma OAI.TriangularHilbert.MatrixEnergy.gramRow_posSemidef line 1659
  181. lemma OAI.TriangularHilbert.MatrixEnergy.pinchedRow_posSemidef line 1663
  182. lemma OAI.TriangularHilbert.MatrixEnergy.gramRow_le_two_pinchedRow line 1666
  183. theorem OAI.TriangularHilbert.MatrixEnergy.hessianCost_gramRow_ge_edges line 1685
  184. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_blocks line 1717
  185. lemma OAI.TriangularHilbert.MatrixEnergy.starGram_eq_gramRow line 1727
  186. lemma OAI.TriangularHilbert.MatrixEnergy.starInsert_eq_insertRow line 1741
  187. def OAI.TriangularHilbert.MatrixEnergy.centerGram line 1758
  188. lemma OAI.TriangularHilbert.MatrixEnergy.triangleBlocks_adj line 1762
  189. lemma OAI.TriangularHilbert.MatrixEnergy.triangleBlocks_diag line 1767
  190. lemma OAI.TriangularHilbert.MatrixEnergy.centerGram_posSemidef line 1772
  191. lemma OAI.TriangularHilbert.MatrixEnergy.edgeGram_le_centerGram line 1778
  192. theorem OAI.TriangularHilbert.MatrixEnergy.neighbor_comparison line 1786
  193. def OAI.TriangularHilbert.MatrixEnergy.sqrtInverse line 1807
  194. lemma OAI.TriangularHilbert.MatrixEnergy.sqrtInverse_solves line 1812
  195. def OAI.TriangularHilbert.MatrixEnergy.hessianPairPD line 1817
  196. lemma OAI.TriangularHilbert.MatrixEnergy.hessianPairPD_symm line 1820
  197. lemma OAI.TriangularHilbert.MatrixEnergy.hessianPairPD_self line 1828
  198. lemma OAI.TriangularHilbert.MatrixEnergy.two_hessianPairPD_le line 1833
  199. lemma OAI.TriangularHilbert.MatrixEnergy.hessianPairPD_eq_trace line 1847
  200. theorem OAI.TriangularHilbert.MatrixEnergy.energy_path_hasDerivAt line 1852
  201. theorem OAI.TriangularHilbert.MatrixEnergy.energyGradient_path_hasDerivAt line 1857
  202. def OAI.TriangularHilbert.MatrixEnergy.rowNorm line 1879
  203. def OAI.TriangularHilbert.MatrixEnergy.colNorm line 1880
  204. theorem OAI.TriangularHilbert.MatrixEnergy.norm_mul_entry_le line 1883
  205. theorem OAI.TriangularHilbert.MatrixEnergy.colNorm_sq line 1891
  206. theorem OAI.TriangularHilbert.MatrixEnergy.colNorm_sqrt_gram line 1901
  207. theorem OAI.TriangularHilbert.MatrixEnergy.entry_gradient_le line 1910