OAI/Probability/ParisiFinite/TermNormSub.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Term Norm Sub.

  1. theorem OAI.TensorPackets.term_norm_sub line 46
  2. theorem OAI.TensorPackets.packet_norm_sub_limit line 56
  3. def OAI.FiniteTree.FullRoot.deletion line 78
  4. theorem OAI.FiniteTree.FullRoot.delete_tensorState line 81
  5. theorem OAI.FiniteTree.FullRoot.delete_tensorState_error line 87
  6. theorem OAI.FiniteTree.FullRoot.deletion_program_error line 110
  7. def OAI.FiniteTree.FullRoot.edgeIndex line 139
  8. def OAI.FiniteTree.FullRoot.edgeSplit line 153
  9. theorem OAI.FiniteTree.FullRoot.edgeSplit_apply line 159
  10. def OAI.FiniteTree.FullRoot.edgeEmbed line 165
  11. theorem OAI.FiniteTree.FullRoot.edgeEmbed_apply line 169
  12. theorem OAI.FiniteTree.FullRoot.edgeSplit_term line 172
  13. theorem OAI.FiniteTree.FullRoot.edgeSplit_vac line 191
  14. theorem OAI.FiniteTree.FullRoot.edgeEmbed_vac line 202
  15. theorem OAI.FiniteTree.FullRoot.edgeSplit_deletion line 206
  16. theorem OAI.TwoHalfTree.tensor_smul_left line 235
  17. theorem OAI.TwoHalfTree.tensor_smul_right line 242
  18. theorem OAI.TwoHalfTree.tensor_sub_right line 249
  19. theorem OAI.TwoHalfTree.norm_tensor line 254
  20. theorem OAI.TwoHalfTree.nonvacuum_tensor line 261
  21. theorem OAI.TwoHalfTree.nonvacuum_tensor_norm line 266
  22. theorem OAI.TwoHalfTree.vacuum_remainder_bound line 271
  23. theorem OAI.TwoHalfTree.nonvacuum_tensor_bound line 294
  24. def OAI.FiniteTree.FullRoot.edgeVector line 311
  25. theorem OAI.FiniteTree.FullRoot.edgeVector_centered line 314
  26. theorem OAI.FiniteTree.FullRoot.edgeVector_norm line 319
  27. theorem OAI.FiniteTree.FullRoot.edge_contract line 324
  28. theorem OAI.FiniteTree.FullRoot.edge_deletion_limit line 332
  29. theorem OAI.FiniteTree.FullRoot.edgeSplit_term_nonvacuum line 344
  30. theorem OAI.FiniteTree.FullRoot.edgeSplit_packet_nonvacuum line 361
  31. theorem OAI.FiniteTree.FullRoot.edge_nonvacuum_bound line 382
  32. theorem OAI.TwoHalfTree.replacement_pairing line 400
  33. theorem OAI.TwoHalfTree.edge_replacement line 419
  34. theorem OAI.FiniteTree.FullRoot.excitation_pure line 444
  35. theorem OAI.FiniteTree.FullRoot.marked_term line 454
  36. theorem OAI.FiniteTree.FullRoot.marked_packet line 475
  37. theorem OAI.FiniteTree.FullRoot.marked_edge line 486
  38. def OAI.FiniteTree.FullRoot.edgeValue line 507
  39. def OAI.FiniteTree.FullRoot.sideValue line 510
  40. def OAI.FiniteTree.FullRoot.deletionError line 514
  41. theorem OAI.FiniteTree.FullRoot.edgeValue_error_bound line 518
  42. theorem OAI.FiniteTree.FullRoot.edge_side_difference_limit line 549
  43. theorem OAI.FiniteTree.FullRoot.sideValue_marked line 562
  44. theorem OAI.FiniteTree.FullRoot.sideValue_limit line 574
  45. theorem OAI.FiniteTree.FullRoot.edgeValue_limit line 588
  46. theorem OAI.SKQAOA.Locality.relevantEdges_qaoa_angles line 604
  47. lemma OAI.SKQAOA.SiteHistories.interaction_scale line 617
  48. lemma OAI.SKQAOA.SiteHistories.delta_scale line 623
  49. lemma OAI.SKQAOA.SiteHistories.edgeKernel_scale line 628
  50. lemma OAI.SKQAOA.SiteHistories.rawGraphCoefficient_scale line 638
  51. theorem OAI.SKQAOA.SiteHistories.graphCoefficient_zero_of_not_cone line 651
  52. theorem OAI.SKQAOA.SiteHistories.graphCoefficientLimit_zero_of_not_cone line 680