OAI/Probability/RadialTransition/RangeBounds.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RadialTransition.cellMargin_mono line 16
  2. lemma OAI.RadialTransition.cellReach_mono line 21
  3. lemma OAI.RadialTransition.cellMargin_toNat_le line 24
  4. lemma OAI.RadialTransition.deletionMajorant_le line 33
  5. lemma OAI.RadialTransition.deletionMajorant_grid_sum line 41
  6. lemma OAI.RadialTransition.deletionMajorant_grid_sum_range line 61
  7. def OAI.RadialTransition.referenceMajorant line 74
  8. lemma OAI.RadialTransition.referenceMajorant_nonneg line 77
  9. lemma OAI.RadialTransition.referenceMajorant_row line 83
  10. lemma OAI.RadialTransition.referenceMajorant_support line 92
  11. lemma OAI.RadialTransition.core_le_cellMajorant line 100
  12. lemma OAI.RadialTransition.family_abs_le_referenceMajorant line 113
  13. def OAI.RadialTransition.referenceRowBound line 125
  14. def OAI.RadialTransition.boxPressureConstant line 127
  15. lemma OAI.RadialTransition.referenceRowBound_nonneg line 130
  16. lemma OAI.RadialTransition.boxPressureConstant_nonneg line 136
  17. lemma OAI.RadialTransition.family_aligned_box_comparison line 142
  18. theorem OAI.RadialTransition.finiteGrandPressure_family_box_error line 198
  19. def OAI.RadialTransition.bumpLip line 220
  20. lemma OAI.RadialTransition.lipschitz_bump line 223
  21. lemma OAI.RadialTransition.scaledBump_nonneg line 226
  22. lemma OAI.RadialTransition.continuous_scaledBump line 230
  23. lemma OAI.RadialTransition.integrable_scaledBump line 233
  24. lemma OAI.RadialTransition.scaledBump_bound line 238
  25. lemma OAI.RadialTransition.scaledBump_zero line 244
  26. lemma OAI.RadialTransition.scaledBump_symm line 247
  27. lemma OAI.RadialTransition.scaledBump_oscillation line 251
  28. lemma OAI.RadialTransition.macroOrigin_mem line 263
  29. lemma OAI.RadialTransition.macro_distance_origin line 271
  30. lemma OAI.RadialTransition.macro_difference_dist line 289
  31. lemma OAI.RadialTransition.macroReach_of_dist line 294
  32. def OAI.RadialTransition.macroKernel line 316
  33. def OAI.RadialTransition.macroKernelError line 319
  34. def OAI.RadialTransition.macroKernelUpper line 322
  35. def OAI.RadialTransition.macroKernelLower line 325
  36. lemma OAI.RadialTransition.macroKernelError_nonneg line 328
  37. lemma OAI.RadialTransition.macroKernelUpper_nonneg line 332
  38. lemma OAI.RadialTransition.macroKernelLower_nonneg line 335
  39. lemma OAI.RadialTransition.macroKernel_symm line 337
  40. lemma OAI.RadialTransition.macroKernelError_symm line 340
  41. lemma OAI.RadialTransition.macroKernelUpper_symm line 346
  42. lemma OAI.RadialTransition.macroKernelLower_symm line 351
  43. lemma OAI.RadialTransition.macroKernel_pair_bounds line 356