OAI/Probability/ParisiFinite/Energy.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Energy.

  1. theorem OAI.SeedInitialization.CausalFrame.energy line 40
  2. inductive OAI.GramCalculus.TraceGate line 67
  3. def OAI.GramCalculus.TraceGate.forget line 75
  4. def OAI.GramCalculus.TraceGate.coeffSeed line 80
  5. def OAI.GramCalculus.TraceGate.coeffCost line 83
  6. def OAI.GramCalculus.TraceGate.encode line 87
  7. theorem OAI.GramCalculus.TraceGate.combination_cost line 92
  8. theorem OAI.GramCalculus.TraceGate.basis_sum line 98
  9. theorem OAI.GramCalculus.TraceGate.combination_seed line 103
  10. def OAI.GramCalculus.TraceGate.reindex line 109
  11. def OAI.GramCalculus.TraceWord.forget line 118
  12. def OAI.GramCalculus.TraceWord.encode line 120
  13. def OAI.GramCalculus.TraceWord.Valid line 124
  14. theorem OAI.GramCalculus.TraceWord.op_model line 132
  15. theorem OAI.GramCalculus.TraceWord.forget_reindex line 165
  16. theorem OAI.GramCalculus.TraceWord.valid_reindex line 172
  17. theorem OAI.GramCalculus.TraceWord.op_reindex line 187
  18. structure OAI.SeedInitialization.TaggedFrame line 228
  19. def OAI.SeedInitialization.TaggedFrame.initial line 237
  20. def OAI.SeedInitialization.TaggedFrame.append line 257
  21. theorem OAI.SeedInitialization.TaggedFrame.op_model line 279
  22. def OAI.SeedInitialization.TaggedFrame.record line 295
  23. theorem OAI.GramCalculus.PacketMatch.zero line 326
  24. theorem OAI.GramCalculus.PacketMatch.add line 332
  25. theorem OAI.GramCalculus.ApproxMatch.zero line 360
  26. theorem OAI.GramCalculus.ApproxMatch.add line 362
  27. theorem OAI.GramCalculus.ApproxMatch.smul line 373
  28. theorem OAI.GramCalculus.ApproxMatch.finSum line 379
  29. theorem OAI.SeedInitialization.CausalFrame.combination_packet line 398
  30. theorem OAI.SeedInitialization.amplitude_inverse line 418
  31. theorem OAI.SeedInitialization.amplitude_zero line 420
  32. theorem OAI.SeedInitialization.amplitude_eventually_pos line 422
  33. def OAI.SeedInitialization.reciprocalInitialStage line 425
  34. def OAI.SeedInitialization.initialTrace line 441
  35. theorem OAI.SeedInitialization.initialTrace_forget line 444
  36. theorem OAI.SeedInitialization.initialTrace_valid line 447
  37. theorem OAI.SeedInitialization.combination_initial line 450
  38. theorem OAI.SeedInitialization.initial_lowClose line 462
  39. def OAI.SeedInitialization.initialRecorded line 482
  40. def OAI.SeedInitialization.CausalFrame.centerModel line 505
  41. def OAI.SeedInitialization.CausalFrame.visibility line 509
  42. theorem OAI.SeedInitialization.CausalFrame.center_match line 517
  43. theorem OAI.SeedInitialization.CausalFrame.visibility_limit line 525
  44. theorem OAI.SeedInitialization.CausalFrame.visibility_Z line 541
  45. theorem OAI.SeedInitialization.CausalFrame.visibility_Y line 553
  46. theorem OAI.PointedTree.PacketStage.exists_compensated_transport line 580