OAI/Combinatorics/ThinTrees/Duality.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.Duality.strictUpperImage line 15
  2. lemma OAI.StrongThinTree.Duality.strictUpperImage_isOpen line 19
  3. lemma OAI.StrongThinTree.Duality.strictUpperImage_convex line 28
  4. lemma OAI.StrongThinTree.Duality.functional_coordinates line 48
  5. lemma OAI.StrongThinTree.Duality.convex_alternative line 62
  6. lemma OAI.StrongThinTree.Duality.slater_certificate line 126
  7. lemma OAI.StrongThinTree.Duality.strict_feasible_of_dual_bound line 180
  8. lemma OAI.StrongThinTree.MatrixDual.quadratic_symm line 201
  9. lemma OAI.StrongThinTree.MatrixDual.solve line 206
  10. lemma OAI.StrongThinTree.MatrixDual.inverse_quadratic_variational line 210
  11. lemma OAI.StrongThinTree.MatrixDual.inverse_quadratic_attained line 221
  12. lemma OAI.StrongThinTree.MatrixDual.posDef_convex line 227
  13. lemma OAI.StrongThinTree.MatrixDual.inverse_quadratic_convex line 234
  14. lemma OAI.StrongThinTree.MatrixDual.cut_quadratic_convex line 256
  15. lemma OAI.StrongThinTree.MatrixDual.posDef_sqrt line 263
  16. lemma OAI.StrongThinTree.MatrixDual.congr_posDef line 269
  17. lemma OAI.StrongThinTree.MatrixDual.trace_objective_attained line 274
  18. lemma OAI.StrongThinTree.MatrixDual.sqrt_tendsto line 319
  19. lemma OAI.StrongThinTree.MatrixDual.traceRoot_tendsto line 326
  20. lemma OAI.StrongThinTree.MatrixDual.trace_objective_approx line 344
  21. lemma OAI.StrongThinTree.Polar.sqrt_eq_real_cfc line 382
  22. lemma OAI.StrongThinTree.Polar.trace_sqrt_roots line 388
  23. lemma OAI.StrongThinTree.Polar.trace_sqrt_mul_comm line 397
  24. lemma OAI.StrongThinTree.Polar.trace_sqrt_gram line 411
  25. lemma OAI.StrongThinTree.Polar.cfc_continuousOn line 417
  26. lemma OAI.StrongThinTree.Polar.inverse_sqrt_scalar line 422
  27. lemma OAI.StrongThinTree.Polar.inverse_sqrt_scalar_bound line 431
  28. lemma OAI.StrongThinTree.Polar.polar_optimizer line 440
  29. lemma OAI.StrongThinTree.Polar.norm_sq_mulVec_le line 473
  30. lemma OAI.StrongThinTree.Polar.dual_trace_rectangular line 484
  31. lemma OAI.StrongThinTree.Polar.signed_diag_orthogonal line 501
  32. lemma OAI.StrongThinTree.Polar.positive_optimizer line 513
  33. def OAI.StrongThinTree.ShortcutDual.boundaryMatrix line 559
  34. def OAI.StrongThinTree.ShortcutDual.boundaryAverage line 562
  35. def OAI.StrongThinTree.ShortcutDual.objectiveMatrix line 566
  36. def OAI.StrongThinTree.ShortcutDual.cutMatrix line 569
  37. lemma OAI.StrongThinTree.ShortcutDual.outer_posSemidef line 573
  38. lemma OAI.StrongThinTree.ShortcutDual.boundaryMatrix_posSemidef line 578
  39. lemma OAI.StrongThinTree.ShortcutDual.objectiveMatrix_posSemidef line 585
  40. lemma OAI.StrongThinTree.ShortcutDual.cutMatrix_posSemidef line 590
  41. lemma OAI.StrongThinTree.ShortcutDual.trace_outer_mul line 595
  42. lemma OAI.StrongThinTree.ShortcutDual.boundaryAverage_convex line 600
  43. lemma OAI.StrongThinTree.ShortcutDual.trace_objectiveMatrix line 613
  44. lemma OAI.StrongThinTree.ShortcutDual.trace_cutMatrix line 619
  45. lemma OAI.StrongThinTree.ShortcutDual.cut_slater line 624
  46. lemma OAI.StrongThinTree.ShortcutDual.shortcut_of_trace_bound line 639
  47. lemma OAI.StrongThinTree.ShortcutDual.weighted_rows_bound line 672
  48. def OAI.StrongThinTree.ShortcutDual.edgeWeight line 720
  49. lemma OAI.StrongThinTree.ShortcutDual.objectiveMatrix_eq_sum_edges line 724
  50. lemma OAI.StrongThinTree.ShortcutDual.weighted_gram line 737
  51. lemma OAI.StrongThinTree.ShortcutDual.objectiveMatrix_gram line 750
  52. lemma OAI.StrongThinTree.ShortcutDual.nuclear_bound_of_embedding_bound line 763
  53. lemma OAI.StrongThinTree.ShortcutDual.sqrt_smul_real line 780
  54. lemma OAI.StrongThinTree.ShortcutDual.traceRoot_sq_smul line 787
  55. lemma OAI.StrongThinTree.ShortcutDual.traceRoot_sq_tendsto line 799
  56. lemma OAI.StrongThinTree.ShortcutDual.cutMatrix_smul line 811
  57. lemma OAI.StrongThinTree.ShortcutDual.trace_bound_of_nat_weights line 815
  58. def OAI.StrongThinTree.ShortcutDual.replicaMatrix line 849
  59. lemma OAI.StrongThinTree.ShortcutDual.replicaMatrix_binary line 854
  60. lemma OAI.StrongThinTree.ShortcutDual.replicaMatrix_gram line 859
  61. lemma OAI.StrongThinTree.ShortcutDual.replicaMatrix_energy line 870
  62. lemma OAI.StrongThinTree.ShortcutDual.shortcut_of_binary_bound line 880