OAI/Geometry/CylinderCovering/Radial/Riemann.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.RadialRiemann.step_pos line 10
  2. lemma OAI.CylinderCovering.RadialRiemann.count_step line 14
  3. lemma OAI.CylinderCovering.RadialRiemann.point_zero line 19
  4. lemma OAI.CylinderCovering.RadialRiemann.point_last line 22
  5. lemma OAI.CylinderCovering.RadialRiemann.point_succ line 26
  6. lemma OAI.CylinderCovering.RadialRiemann.point_mem line 31
  7. lemma OAI.CylinderCovering.RadialRiemann.cell_subset line 41
  8. lemma OAI.CylinderCovering.RadialRiemann.cell_nonempty line 49
  9. lemma OAI.CylinderCovering.RadialRiemann.cell_dist_le line 56
  10. lemma OAI.CylinderCovering.RadialRiemann.step_tendsto line 63
  11. lemma OAI.CylinderCovering.RadialRiemann.diagonal_continuous line 70
  12. lemma OAI.CylinderCovering.RadialRiemann.diagonal_cell_integrable line 75
  13. lemma OAI.CylinderCovering.RadialRiemann.integral_mesh_sum line 87
  14. lemma OAI.CylinderCovering.RadialRiemann.mixedSum_error line 98
  15. theorem OAI.CylinderCovering.RadialRiemann.mixedSum_tendsto line 133
  16. lemma OAI.CylinderCovering.RadialRiemann.exists_capMax_tag line 164
  17. lemma OAI.CylinderCovering.RadialRiemann.collarSum_eq_mixed line 172
  18. theorem OAI.CylinderCovering.RadialRiemann.collarSum_tendsto line 184
  19. lemma OAI.CylinderCovering.RadialRiemann.le_capMax line 213
  20. lemma OAI.CylinderCovering.RadialRiemann.capMax_nonneg line 219
  21. lemma OAI.CylinderCovering.RadialRiemann.capMax_le line 226
  22. lemma OAI.CylinderCovering.RadialRiemann.projection_weight_continuousOn line 233
  23. theorem OAI.CylinderCovering.RadialRiemann.physical_collar_tendsto line 241
  24. theorem OAI.CylinderCovering.RadialRiemann.taggedSum_tendsto line 268
  25. lemma OAI.CylinderCovering.RadialRiemann.leftTagged line 278
  26. theorem OAI.CylinderCovering.RadialRiemann.leftSum_tendsto line 286
  27. lemma OAI.CylinderCovering.RadialRiemann.exists_adjacent_interval line 293
  28. lemma OAI.CylinderCovering.RadialRiemann.exists_cell line 307
  29. theorem OAI.CylinderCovering.RadialRiemann.maxPowerSum_tendsto line 312
  30. theorem OAI.CylinderCovering.RadialRiemann.maxPolynomialSum_tendsto line 329
  31. theorem OAI.CylinderCovering.RadialRiemann.mixedSum_lipschitz_error line 356
  32. theorem OAI.CylinderCovering.RadialRiemann.maxPowerSum_lipschitz_error line 373