OAI/Analysis/SegmentLenses/LawRecovery.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-law recovery and coefficient representations

  1. def OAI.SegmentLenses.FiniteLaw.expect line 22
  2. theorem OAI.SegmentLenses.FiniteLaw.expect_const line 25
  3. theorem OAI.SegmentLenses.FiniteLaw.expect_add line 29
  4. theorem OAI.SegmentLenses.FiniteLaw.expect_sub line 33
  5. theorem OAI.SegmentLenses.FiniteLaw.expect_smul line 37
  6. theorem OAI.SegmentLenses.FiniteLaw.expect_map line 44
  7. theorem OAI.SegmentLenses.FiniteLaw.expect_scalar line 49
  8. theorem OAI.SegmentLenses.FiniteLaw.mean_sum line 51
  9. theorem OAI.SegmentLenses.FiniteLaw.norm_expect_le line 56
  10. theorem OAI.SegmentLenses.FiniteLaw.mean_sqrt_le line 63
  11. def OAI.SegmentLenses.FiniteLaw.product line 71
  12. theorem OAI.SegmentLenses.FiniteLaw.product_mean line 77
  13. theorem OAI.SegmentLenses.FiniteLaw.product_mul line 82
  14. def OAI.SegmentLenses.FiniteLaw.pooled line 93
  15. theorem OAI.SegmentLenses.FiniteLaw.pooled_expect line 99
  16. def OAI.SegmentLenses.representation line 112
  17. theorem OAI.SegmentLenses.representation_value line 114
  18. theorem OAI.SegmentLenses.representation_energy line 119
  19. def OAI.SegmentLenses.coefficientLaw line 127
  20. def OAI.SegmentLenses.coefficientAtoms line 135
  21. theorem OAI.SegmentLenses.coefficientAtoms_energy line 140
  22. theorem OAI.SegmentLenses.coefficientLaw_mean line 149
  23. theorem OAI.SegmentLenses.FiniteLaw.absolute_mass_identity line 170
  24. theorem OAI.SegmentLenses.FiniteLaw.absolute_mass_bound line 182
  25. theorem OAI.SegmentLenses.FiniteLaw.signed_mass_bound line 197
  26. theorem OAI.SegmentLenses.FiniteLaw.joint_mass_bound line 216
  27. theorem OAI.SegmentLenses.segmentFunctional_unitVector line 229
  28. theorem OAI.SegmentLenses.Representation.apply_unitVector line 237
  29. theorem OAI.SegmentLenses.Representation.apply_of_mem line 241
  30. theorem OAI.SegmentLenses.Representation.apply_nonzero line 251
  31. theorem OAI.SegmentLenses.Representation.gate_energy_le line 263