OAI/Analysis/C0Absorption/Blocks.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.C0Absorption.Level line 14
  2. def OAI.C0Absorption.levelJ line 15
  3. abbrev OAI.C0Absorption.Block line 16
  4. structure OAI.C0Absorption.Label line 18
  5. instance OAI.C0Absorption.(instance at line 23) line 23
  6. instance OAI.C0Absorption.(instance at line 31) line 31
  7. instance OAI.C0Absorption.(instance at line 32) line 32
  8. abbrev OAI.C0Absorption.InputCoordinate line 34
  9. def OAI.C0Absorption.coordinateEnumeration line 36
  10. def OAI.C0Absorption.rowIndex line 38
  11. def OAI.C0Absorption.labelIndex line 39
  12. def OAI.C0Absorption.blockLabel line 40
  13. theorem OAI.C0Absorption.blockLabel_level line 42
  14. theorem OAI.C0Absorption.blockLabel_injective line 44
  15. theorem OAI.C0Absorption.labelIndex_injective line 51
  16. theorem OAI.C0Absorption.rowIndex_injective line 55
  17. theorem OAI.C0Absorption.rowIndex_ne_labelIndex line 59
  18. def OAI.C0Absorption.blockCoordinates line 63
  19. theorem OAI.C0Absorption.mem_blockCoordinates line 67
  20. theorem OAI.C0Absorption.blockCoordinates_nonempty line 78
  21. def OAI.C0Absorption.predecessorCoordinates line 84
  22. def OAI.C0Absorption.radiusCoordinates line 89
  23. theorem OAI.C0Absorption.radiusCoordinates_nonempty line 91
  24. def OAI.C0Absorption.levelSuccessor line 94
  25. def OAI.C0Absorption.coordinateLevels line 96
  26. theorem OAI.C0Absorption.radius_incidence line 102
  27. theorem OAI.C0Absorption.radius_finite_exceptions line 143
  28. def OAI.C0Absorption.finiteProjection line 152
  29. theorem OAI.C0Absorption.finiteProjection_apply line 169
  30. def OAI.C0Absorption.finiteRadius line 174
  31. def OAI.C0Absorption.localRadius line 175
  32. theorem OAI.C0Absorption.finiteRadius_nonneg line 177
  33. theorem OAI.C0Absorption.finiteRadius_le line 179
  34. theorem OAI.C0Absorption.coordinate_le_finiteRadius line 187
  35. theorem OAI.C0Absorption.finiteRadius_lipschitz line 191
  36. theorem OAI.C0Absorption.finiteRadius_le_tau line 199
  37. theorem OAI.C0Absorption.finiteRadius_smul line 209
  38. theorem OAI.C0Absorption.localRadius_tendsto line 213