OAI/Analysis/SignedDisk/LocalCancellation5.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedDisk.LocalCancellation.cone_negative_le_error line 22
  2. lemma OAI.SignedDisk.LocalCancellation.general_moment_integrable line 32
  3. lemma OAI.SignedDisk.LocalCancellation.correcting_pairing line 45
  4. lemma OAI.SignedDisk.LocalCancellation.general_kernel_pairing_sub line 62
  5. lemma OAI.SignedDisk.LocalCancellation.corrected_kernel_integrable line 73
  6. lemma OAI.SignedDisk.LocalCancellation.corrected_kernel_pairing_sub line 86
  7. lemma OAI.SignedDisk.LocalCancellation.interior_mass_le_kernel line 99
  8. lemma OAI.SignedDisk.DiskScales.width_add line 119
  9. lemma OAI.SignedDisk.DiskScales.sum_width_tail line 123
  10. lemma OAI.SignedDisk.DiskScales.dist_width_tail line 132
  11. lemma OAI.SignedDisk.LocalCancellation.moment_kernel_pairing_sub line 147
  12. lemma OAI.SignedDisk.LocalCancellation.total_correction line 158
  13. lemma OAI.SignedDisk.LocalCancellation.balanced_kernel_gap_identity line 169
  14. lemma OAI.SignedDisk.LocalCancellation.kernel_error_bound line 205
  15. lemma OAI.SignedDisk.LocalCancellation.coarse_bound_scaled line 218
  16. lemma OAI.SignedDisk.LocalCancellation.scaled_ordinary_inactive line 224
  17. lemma OAI.SignedDisk.LocalCancellation.scaled_corrected_inactive line 239
  18. lemma OAI.SignedDisk.LocalCancellation.scaled_corrected_active line 254
  19. lemma OAI.SignedDisk.DiskScales.successor_discount line 272
  20. lemma OAI.SignedDisk.DiskScales.geometric_den_pos line 280
  21. lemma OAI.SignedDisk.DiskScales.coarse_error_scale line 283
  22. lemma OAI.SignedDisk.LocalCancellation.inactive_kernel_distance line 315
  23. lemma OAI.SignedDisk.LocalCancellation.kernel_gap_errors line 333
  24. lemma OAI.SignedDisk.LocalCancellation.corrected_kernel_gap line 380