OAI/Combinatorics/ThinTrees/Representation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.hasDerivAt_det_one_add_smul line 17
  2. lemma OAI.StrongThinTree.hasDerivAt_det_add_smul line 32
  3. lemma OAI.StrongThinTree.differentiable_det line 46
  4. lemma OAI.StrongThinTree.fderiv_det_apply line 52
  5. lemma OAI.StrongThinTree.one_le_det_one_add line 62
  6. lemma OAI.StrongThinTree.posDef_sqrt_factors line 77
  7. lemma OAI.StrongThinTree.det_le_det_add_of_posSemidef line 85
  8. lemma OAI.StrongThinTree.exists_fderiv_norm_lt_of_bddBelow line 113
  9. def OAI.StrongThinTree.basisCov line 167
  10. def OAI.StrongThinTree.packingCov line 170
  11. lemma OAI.StrongThinTree.basisCov_eq_sum line 173
  12. lemma OAI.StrongThinTree.packingCov_eq_sum line 185
  13. lemma OAI.StrongThinTree.differentiable_packingCov line 191
  14. lemma OAI.StrongThinTree.fderiv_packingCov_single line 201
  15. lemma OAI.StrongThinTree.basisCov_posDef line 217
  16. lemma OAI.StrongThinTree.packingCov_posDef line 225
  17. lemma OAI.StrongThinTree.det_basisCov line 230
  18. lemma OAI.StrongThinTree.det_basisCov_le_packingCov line 237
  19. def OAI.StrongThinTree.packingObjective line 247
  20. lemma OAI.StrongThinTree.packingObjective_bddBelow line 250
  21. lemma OAI.StrongThinTree.differentiable_packingObjective line 271
  22. lemma OAI.StrongThinTree.fderiv_packingObjective_single line 281
  23. lemma OAI.StrongThinTree.exists_small_leverages line 310
  24. theorem OAI.StrongThinTree.isotropic_representation line 330
  25. theorem OAI.StrongThinTree.Packing.represented_packing line 394
  26. def OAI.StrongThinTree.MultiGraph.zeroSumSpace line 473
  27. lemma OAI.StrongThinTree.MultiGraph.mem_zeroSumSpace line 476
  28. lemma OAI.StrongThinTree.MultiGraph.incidence_zeroSum line 479
  29. lemma OAI.StrongThinTree.MultiGraph.edgeSpan_le_zeroSum line 484
  30. lemma OAI.StrongThinTree.MultiGraph.connected_span_zeroSum line 487
  31. lemma OAI.StrongThinTree.MultiGraph.zeroSum_finrank line 503
  32. theorem OAI.StrongThinTree.MultiGraph.graph_isotropic_representation line 508
  33. lemma OAI.StrongThinTree.Packing.projected_trace_bound line 546
  34. lemma OAI.StrongThinTree.Packing.lower_frame_span line 588
  35. theorem OAI.StrongThinTree.Packing.projected_trace_base_packing line 602
  36. lemma OAI.StrongThinTree.Packing.span_smul line 642
  37. lemma OAI.StrongThinTree.Packing.span_map line 655
  38. lemma OAI.StrongThinTree.Packing.rank_injective_map line 660
  39. lemma OAI.StrongThinTree.MultiGraph.represented_rank line 674
  40. theorem OAI.StrongThinTree.MultiGraph.represented_frame_treePackable line 688
  41. theorem OAI.StrongThinTree.MultiGraph.projected_trace_treePackable line 746