OAI/Analysis/SegmentLenses/TailBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Signed-product recovery and the finite midpoint tail bound

  1. theorem OAI.SegmentLenses.tail_expect_smul line 21
  2. theorem OAI.SegmentLenses.norm_signed_tail_expect_le line 31
  3. theorem OAI.SegmentLenses.signed_replacement_recovery line 41
  4. theorem OAI.SegmentLenses.norm_signed_replacement_le line 59
  5. theorem OAI.SegmentLenses.represented_joint_bound line 81
  6. theorem OAI.SegmentLenses.dual_ext_coordinates line 177
  7. theorem OAI.SegmentLenses.head_eq_iff line 183
  8. theorem OAI.SegmentLenses.head_eq_of_subset line 196
  9. theorem OAI.SegmentLenses.norm_center_le line 205
  10. theorem OAI.SegmentLenses.finite_main_tail line 221