OAI/Geometry/UnitDistances/HeightTransfer.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarUnitDistances.GridShift.fract_integrableOn line 10
  2. lemma OAI.PlanarUnitDistances.GridShift.floor_integrableOn line 17
  3. lemma OAI.PlanarUnitDistances.GridShift.fract_shift_integral line 26
  4. lemma OAI.PlanarUnitDistances.GridShift.floor_difference_integral line 32
  5. def OAI.PlanarUnitDistances.GridShift.mismatch line 55
  6. lemma OAI.PlanarUnitDistances.GridShift.mismatch_integrableOn line 57
  7. lemma OAI.PlanarUnitDistances.GridShift.mismatch_nonneg line 67
  8. lemma OAI.PlanarUnitDistances.GridShift.mismatch_le_one line 69
  9. lemma OAI.PlanarUnitDistances.GridShift.mismatch_symm line 71
  10. lemma OAI.PlanarUnitDistances.GridShift.mismatch_integral_le_abs line 74
  11. lemma OAI.PlanarUnitDistances.GridShift.mismatch_integral_le line 91
  12. def OAI.PlanarUnitDistances.GridShift.unitShift line 108
  13. instance OAI.PlanarUnitDistances.GridShift.(instance at line 109) line 109
  14. def OAI.PlanarUnitDistances.GridShift.squareShift line 110
  15. instance OAI.PlanarUnitDistances.GridShift.(instance at line 111) line 111
  16. def OAI.PlanarUnitDistances.GridShift.gridLabel line 113
  17. def OAI.PlanarUnitDistances.GridShift.gridMismatch line 116
  18. lemma OAI.PlanarUnitDistances.GridShift.gridLabel_measurable line 119
  19. lemma OAI.PlanarUnitDistances.GridShift.gridMismatch_measurable line 123
  20. lemma OAI.PlanarUnitDistances.GridShift.gridMismatch_integrable line 127
  21. lemma OAI.PlanarUnitDistances.GridShift.gridMismatch_le_coordinates line 134
  22. lemma OAI.PlanarUnitDistances.GridShift.coordinate_mismatch_measurable line 142
  23. lemma OAI.PlanarUnitDistances.GridShift.coordinate_mismatch_integrable line 146
  24. lemma OAI.PlanarUnitDistances.GridShift.integral_mismatch_fst line 153
  25. lemma OAI.PlanarUnitDistances.GridShift.integral_mismatch_snd line 158
  26. lemma OAI.PlanarUnitDistances.GridShift.gridMismatch_integral_le line 163
  27. lemma OAI.PlanarUnitDistances.GridShift.abs_sub_lt_one_of_floor_eq line 190
  28. lemma OAI.PlanarUnitDistances.GridShift.norm_le_of_same_grid line 199
  29. lemma OAI.PlanarUnitDistances.GridShift.tail_le_gridMismatch line 209
  30. lemma OAI.PlanarUnitDistances.GridShift.kernel_continuous line 223
  31. lemma OAI.PlanarUnitDistances.GridShift.exp_neg_posLog_control line 226
  32. lemma OAI.PlanarUnitDistances.GridShift.kernel_integral_le line 231
  33. lemma OAI.PlanarUnitDistances.GridShift.kernel_setIntegral_le line 259
  34. lemma OAI.PlanarUnitDistances.GridShift.tail_iff_threshold line 264
  35. lemma OAI.PlanarUnitDistances.GridShift.tail_integrableOn line 274
  36. lemma OAI.PlanarUnitDistances.GridShift.tail_setIntegral line 281
  37. def OAI.PlanarUnitDistances.LocalHeightTransfer.left line 303
  38. def OAI.PlanarUnitDistances.LocalHeightTransfer.dis line 305
  39. def OAI.PlanarUnitDistances.LocalHeightTransfer.LabelControl line 307
  40. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.label_control_any line 312
  41. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.left_nonneg line 324
  42. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.grid_level line 327
  43. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.weighted_tails_integrable line 371
  44. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.weighted_tails_integral line 375
  45. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.weighted_kernel_integrable line 383
  46. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.weighted_kernel_integral_le line 387
  47. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.log_two_control line 396
  48. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.archimedean_transfer line 403
  49. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.nonarchimedean_level line 460
  50. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.nonarchimedean_transfer line 484
  51. lemma OAI.PlanarUnitDistances.LocalHeightTransfer.control_nonneg line 507
  52. lemma OAI.PlanarUnitDistances.HeightTransfer.weighted_finite_support line 523
  53. lemma OAI.PlanarUnitDistances.HeightTransfer.weighted_height_identity line 529
  54. theorem OAI.PlanarUnitDistances.HeightTransfer.height_transfer line 559
  55. theorem OAI.PlanarUnitDistances.GlobalLabelControl.constants line 621
  56. lemma OAI.PlanarUnitDistances.ActualHeightTransfer.label_control line 655
  57. theorem OAI.PlanarUnitDistances.ActualHeightTransfer.from_expansion line 686
  58. lemma OAI.PlanarUnitDistances.ActualHeightTransfer.pair_height line 700
  59. lemma OAI.PlanarUnitDistances.FiniteLaw.exists_le_average line 715