OAI/Analysis/SegmentLenses/Stability.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Weighted stability and original-coordinate estimates

  1. theorem OAI.SegmentLenses.gate_coordinate_square_sum line 25
  2. def OAI.SegmentLenses.lawDeficit line 55
  3. def OAI.SegmentLenses.lawError line 58
  4. def OAI.SegmentLenses.lawSlack line 61
  5. theorem OAI.SegmentLenses.unit_law_budget line 64
  6. theorem OAI.SegmentLenses.lawDeficit_nonneg line 94
  7. theorem OAI.SegmentLenses.mean_error_norm_le line 102
  8. theorem OAI.SegmentLenses.signed_law_error_le line 114
  9. theorem OAI.SegmentLenses.law_absolute_mass_bound line 123
  10. theorem OAI.SegmentLenses.represented_bounded_multiplier line 176
  11. theorem OAI.SegmentLenses.stable_radical_linear line 209
  12. def OAI.SegmentLenses.FiniteLaw.mixture line 227
  13. theorem OAI.SegmentLenses.FiniteLaw.mixture_mean line 233
  14. theorem OAI.SegmentLenses.FiniteLaw.mixture_expect line 237
  15. theorem OAI.SegmentLenses.FiniteLaw.weight_mul_mean_le line 242
  16. theorem OAI.SegmentLenses.mixture_deficit line 253
  17. theorem OAI.SegmentLenses.represented_weighted_tail line 267
  18. theorem OAI.SegmentLenses.head_tail_commute line 343
  19. theorem OAI.SegmentLenses.weighted_tail_bound line 358
  20. theorem OAI.SegmentLenses.weighted_deficits line 405