OAI/Analysis/C0Absorption/Signs.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.realSign line 13
  2. theorem OAI.C0Absorption.realSign_true line 15
  3. theorem OAI.C0Absorption.realSign_false line 16
  4. theorem OAI.C0Absorption.abs_realSign line 17
  5. theorem OAI.C0Absorption.sum_sign_sq line 19
  6. theorem OAI.C0Absorption.finite_detector_bound line 41
  7. theorem OAI.C0Absorption.no_infinite_detectors line 81
  8. def OAI.C0Absorption.flipSign line 97
  9. theorem OAI.C0Absorption.realSign_not line 103
  10. theorem OAI.C0Absorption.signed_sum_sub_flip line 106
  11. theorem OAI.C0Absorption.seminorm_sign_pair line 118
  12. theorem OAI.C0Absorption.sum_sign_seminorm_sq_ge line 136
  13. theorem OAI.C0Absorption.sum_coordinate_choice_le line 151
  14. theorem OAI.C0Absorption.sum_ciSup_le_of_forall_choice line 181
  15. theorem OAI.C0Absorption.coordinate_envelope_summable line 206
  16. theorem OAI.C0Absorption.square_norm_tendsto_zero line 228
  17. theorem OAI.C0Absorption.exists_nonzero_coordinate line 247