OAI/Analysis/SegmentLenses/GateRecovery.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Gate coefficients, cone recovery, and energy budgets

  1. def OAI.SegmentLenses.headLinear line 19
  2. def OAI.SegmentLenses.tailLinear line 24
  3. theorem OAI.SegmentLenses.headLinear_apply line 27
  4. theorem OAI.SegmentLenses.tailLinear_apply line 32
  5. theorem OAI.SegmentLenses.tail_unitVector line 37
  6. theorem OAI.SegmentLenses.tail_segmentFunctional line 42
  7. def OAI.SegmentLenses.SegmentFamily.replacement line 56
  8. theorem OAI.SegmentLenses.SegmentFamily.replacement_energy line 59
  9. theorem OAI.SegmentLenses.SegmentFamily.replacement_gate line 64
  10. def OAI.SegmentLenses.Representation.error line 74
  11. theorem OAI.SegmentLenses.Representation.error_value line 77
  12. theorem OAI.SegmentLenses.Representation.error_energy line 89
  13. theorem OAI.SegmentLenses.Representation.error_slack_identity line 94
  14. theorem OAI.SegmentLenses.Representation.energy_nonneg line 103
  15. theorem OAI.SegmentLenses.SegmentFamily.member_unique line 117
  16. def OAI.SegmentLenses.SegmentFamily.gateTail line 128
  17. theorem OAI.SegmentLenses.SegmentFamily.gateTail_of_mem line 131
  18. theorem OAI.SegmentLenses.SegmentFamily.gateTail_segment line 138
  19. theorem OAI.SegmentLenses.SegmentFamily.gateTail_cone line 156
  20. theorem OAI.SegmentLenses.SegmentFamily.exists_gate_of_crossing line 172
  21. theorem OAI.SegmentLenses.SegmentFamily.boundary_tail_expansion line 207
  22. theorem OAI.SegmentLenses.SegmentFamily.tail_replacement line 222
  23. def OAI.SegmentLenses.Representation.scale line 260
  24. theorem OAI.SegmentLenses.Representation.scale_value line 263
  25. theorem OAI.SegmentLenses.Representation.scale_energy line 274
  26. theorem OAI.SegmentLenses.exists_atomic_law line 286
  27. theorem OAI.SegmentLenses.FiniteLaw.expect_apply line 321
  28. theorem OAI.SegmentLenses.FiniteLaw.expect_sum line 326