OAI/Analysis/C0Absorption/Tests.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.C0Absorption.CylinderOperation line 14
  2. def OAI.C0Absorption.CylinderOperation.scale line 21
  3. def OAI.C0Absorption.CylinderOperation.point line 22
  4. def OAI.C0Absorption.CylinderOperation.act line 23
  5. theorem OAI.C0Absorption.CylinderOperation.scale_pos line 26
  6. theorem OAI.C0Absorption.CylinderOperation.act_lipschitz line 28
  7. theorem OAI.C0Absorption.CylinderOperation.act_sup line 34
  8. def OAI.C0Absorption.applyOperations line 43
  9. theorem OAI.C0Absorption.applyOperations_nil line 49
  10. theorem OAI.C0Absorption.applyOperations_cons line 50
  11. theorem OAI.C0Absorption.applyOperations_append line 54
  12. theorem OAI.C0Absorption.applyOperations_lipschitz line 60
  13. theorem OAI.C0Absorption.applyOperations_sup line 69
  14. theorem OAI.C0Absorption.applyOperations_support_bound line 78
  15. structure OAI.C0Absorption.CylinderBases line 90
  16. structure OAI.C0Absorption.GeneratedRepresentation line 102
  17. def OAI.C0Absorption.GeneratedRepresentation.cubeValue line 110
  18. def OAI.C0Absorption.GeneratedRepresentation.value line 113
  19. def OAI.C0Absorption.GeneratedRepresentation.baseRepresentation line 116
  20. theorem OAI.C0Absorption.GeneratedRepresentation.cubeValue_lipschitz line 119
  21. theorem OAI.C0Absorption.GeneratedRepresentation.value_lipschitz line 123
  22. theorem OAI.C0Absorption.GeneratedRepresentation.cubeValue_sup line 127
  23. theorem OAI.C0Absorption.GeneratedRepresentation.value_sup line 131
  24. def OAI.C0Absorption.TClass line 137
  25. structure OAI.C0Absorption.TailOperation line 140
  26. def OAI.C0Absorption.TailOperation.factor line 147
  27. theorem OAI.C0Absorption.TailOperation.factor_abs_le line 151
  28. theorem OAI.C0Absorption.TailOperation.factor_lipschitz line 158
  29. def OAI.C0Absorption.tailProduct line 173
  30. theorem OAI.C0Absorption.tailProduct_nil line 175
  31. theorem OAI.C0Absorption.tailProduct_cons line 176
  32. theorem OAI.C0Absorption.tailProduct_abs_le line 179
  33. theorem OAI.C0Absorption.bounded_product_lipschitz line 186
  34. theorem OAI.C0Absorption.tailProduct_lipschitz line 203
  35. theorem OAI.C0Absorption.tailProduct_lipschitz_bound line 213
  36. def OAI.C0Absorption.VClass line 224
  37. theorem OAI.C0Absorption.TClass_lipschitz line 229
  38. theorem OAI.C0Absorption.TClass_sup line 235
  39. theorem OAI.C0Absorption.VClass_lipschitz line 242
  40. theorem OAI.C0Absorption.VClass_sup line 257
  41. def OAI.C0Absorption.sourceClasses line 265
  42. theorem OAI.C0Absorption.sourceClasses_even line 268
  43. theorem OAI.C0Absorption.sourceClasses_odd line 271
  44. theorem OAI.C0Absorption.tsupport_comp_subset line 276
  45. theorem OAI.C0Absorption.tsupport_product_subset_left line 283
  46. theorem OAI.C0Absorption.GeneratedRepresentation.support_bound line 292
  47. def OAI.C0Absorption.GeneratedRepresentation.append line 300
  48. theorem OAI.C0Absorption.GeneratedRepresentation.append_cubeValue line 310
  49. theorem OAI.C0Absorption.GeneratedRepresentation.eventually_append_allowed line 316