OAI/Analysis/C0Absorption/Operations.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.SignedBound line 14
  2. theorem OAI.C0Absorption.SignedBound.initial line 25
  3. theorem OAI.C0Absorption.SignedBound.subsequence line 28
  4. theorem OAI.C0Absorption.SignedBound.nonneg line 31
  5. theorem OAI.C0Absorption.compatible_detectors_false line 36
  6. theorem OAI.C0Absorption.VClass_compatible_false line 87
  7. theorem OAI.C0Absorption.detection_split line 105
  8. def OAI.C0Absorption.CylinderOperation.remainder line 123
  9. theorem OAI.C0Absorption.CylinderOperation.remainder_scale line 124
  10. theorem OAI.C0Absorption.CylinderOperation.remainder_point line 125
  11. theorem OAI.C0Absorption.CylinderOperation.remainder_act line 126
  12. theorem OAI.C0Absorption.CylinderOperation.act_split line 129
  13. theorem OAI.C0Absorption.CylinderOperation.finite_scale_fiber line 140
  14. theorem OAI.C0Absorption.CylinderOperation.constant_or_small line 148
  15. def OAI.C0Absorption.GeneratedRepresentation.subrepresentation line 165
  16. def OAI.C0Absorption.GeneratedRepresentation.sameScales line 174
  17. theorem OAI.C0Absorption.GeneratedRepresentation.length_le_of_prefix line 184
  18. theorem OAI.C0Absorption.VClass_disjoint_false line 194
  19. theorem OAI.C0Absorption.tail_escape_false line 206
  20. theorem OAI.C0Absorption.small_remainders_false line 223
  21. theorem OAI.C0Absorption.TailOperation.ext' line 279
  22. def OAI.C0Absorption.TailOperation.remainder line 283
  23. theorem OAI.C0Absorption.TailOperation.remainder_scaleIndex line 284
  24. theorem OAI.C0Absorption.TailOperation.remainder_tailIndex line 285
  25. theorem OAI.C0Absorption.TailOperation.remainder_isBasic line 286
  26. theorem OAI.C0Absorption.TailOperation.factor_split line 288
  27. theorem OAI.C0Absorption.TailOperation.constant_or_escape line 291
  28. theorem OAI.C0Absorption.tailProduct_append line 305
  29. theorem OAI.C0Absorption.tailProduct_eq_zero line 309
  30. theorem OAI.C0Absorption.full_tail_support line 315