OAI/Probability/ParisiFinite/ChildMomentLimit.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Child Moment Limit.

  1. theorem OAI.FiniteTree.child_moment_limit line 41
  2. theorem OAI.FiniteTree.program_limit_of_child line 55
  3. theorem OAI.FiniteTree.insertion_Gram_limit line 78
  4. theorem OAI.FiniteTree.program_Gram_limit line 106
  5. theorem OAI.FiniteTree.marked_child_moment line 127
  6. theorem OAI.FiniteTree.marked_child_limit line 136
  7. theorem OAI.FiniteTree.marked_child_sum_limit line 143
  8. theorem OAI.FiniteTree.child_sum_centered line 153
  9. theorem OAI.FiniteTree.child_second_limit line 161
  10. theorem OAI.FiniteTree.marked_tensor_limit line 173
  11. theorem OAI.QuantumCLT.inner_creation_coherent line 206
  12. theorem OAI.QuantumCLT.inner_creation_weylProduct line 216
  13. theorem OAI.FiniteTensor.inner_excitation_power line 239
  14. theorem OAI.TensorPackets.inner_plus_term line 262
  15. theorem OAI.TensorPackets.marked_limit line 271
  16. def OAI.FiniteTree.excitation line 290
  17. theorem OAI.FiniteTree.excitation_tensor_limit line 294
  18. theorem OAI.FiniteTree.excitation_program_limit line 306
  19. def OAI.FiniteTree.rootExcitation line 329
  20. theorem OAI.FiniteTree.root_shift_insertion_limit line 334
  21. theorem OAI.FiniteTensor.norm_mixedPower line 363
  22. def OAI.FiniteTensor.vacuumComplement line 374
  23. theorem OAI.FiniteTensor.vacuumComplement_vac line 378
  24. theorem OAI.FiniteTensor.vacuumComplement_norm line 385
  25. def OAI.FiniteTensor.excitedSlot line 393
  26. theorem OAI.FiniteTensor.excitedSlot_power_norm line 398
  27. theorem OAI.FiniteTensor.excitedSlot_power_bound line 408
  28. theorem OAI.QuantumCLT.JetBound.first_bound line 429
  29. def OAI.FiniteTree.wordBound line 457
  30. theorem OAI.FiniteTree.wordBound_nonneg line 460
  31. theorem OAI.FiniteTree.child_word_unitary line 463
  32. theorem OAI.FiniteTree.child_word_vacuum_bound line 477
  33. theorem OAI.FiniteTree.tensor_word_excited_bound line 501
  34. theorem OAI.TensorPackets.norm_term line 523
  35. theorem OAI.TensorPackets.diagonal_constant_term line 527
  36. theorem OAI.TensorPackets.diagonal_constant_packet line 536
  37. theorem OAI.TensorPackets.packet_bound line 545
  38. def OAI.FiniteTree.packetOccupationBound line 564
  39. theorem OAI.FiniteTree.packetOccupationBound_nonneg line 567
  40. theorem OAI.FiniteTree.packet_excited_bound line 574
  41. def OAI.FiniteTree.rootSlot line 584
  42. theorem OAI.FiniteTree.split_rootSlot line 588
  43. def OAI.FiniteTree.topOccupation line 596
  44. theorem OAI.FiniteTree.topOccupation_nonneg line 599
  45. theorem OAI.FiniteTree.insertion_packet line 602
  46. theorem OAI.FiniteTree.insertion_slot_bound line 611
  47. theorem OAI.FiniteTree.insertion_occupation_bound line 619