OAI/Combinatorics/PlanarL1/Increments.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Increment.clamp line 13
  2. lemma OAI.PlanarL1.Increment.clamp_bounds line 15
  3. lemma OAI.PlanarL1.Increment.clamp_lipschitz line 18
  4. lemma OAI.PlanarL1.Increment.clamp_eq line 21
  5. lemma OAI.PlanarL1.Increment.clamp_left line 24
  6. lemma OAI.PlanarL1.Increment.clamp_right line 27
  7. def OAI.PlanarL1.Increment.quadratic line 30
  8. lemma OAI.PlanarL1.Increment.quadratic_lipschitz line 33
  9. def OAI.PlanarL1.Increment.splice line 57
  10. lemma OAI.PlanarL1.Increment.splice_lipschitz line 59
  11. def OAI.PlanarL1.Increment.low line 66
  12. def OAI.PlanarL1.Increment.high line 67
  13. def OAI.PlanarL1.Increment.positivePart line 68
  14. def OAI.PlanarL1.Increment.scalar line 69
  15. lemma OAI.PlanarL1.Increment.low_lipschitz line 71
  16. lemma OAI.PlanarL1.Increment.high_lipschitz line 76
  17. lemma OAI.PlanarL1.Increment.positive_zero line 84
  18. lemma OAI.PlanarL1.Increment.positive_plateau line 88
  19. lemma OAI.PlanarL1.Increment.positive_lipschitz line 97
  20. lemma OAI.PlanarL1.Increment.scalar_lipschitz line 105
  21. lemma OAI.PlanarL1.Increment.positive_far_zero line 115
  22. lemma OAI.PlanarL1.Increment.positive_nonneg line 121
  23. lemma OAI.PlanarL1.Increment.positive_le line 136
  24. lemma OAI.PlanarL1.Increment.scalar_support line 158
  25. lemma OAI.PlanarL1.Increment.scalar_magnitude line 174
  26. lemma OAI.PlanarL1.Increment.scalar_plateau line 183
  27. def OAI.PlanarL1.Increment.taper line 197
  28. lemma OAI.PlanarL1.Increment.taper_bounds line 200
  29. lemma OAI.PlanarL1.Increment.taper_difference line 207
  30. lemma OAI.PlanarL1.Increment.taper_zero line 222
  31. def OAI.PlanarL1.Increment.update line 226
  32. lemma OAI.PlanarL1.Increment.update_lipschitz line 229
  33. lemma OAI.PlanarL1.Increment.update_magnitude line 256
  34. lemma OAI.PlanarL1.Increment.update_zero line 265
  35. lemma OAI.PlanarL1.Increment.update_support line 268
  36. lemma OAI.PlanarL1.Increment.sum_lipschitz_sparse line 273
  37. lemma OAI.PlanarL1.Increment.update_sparse line 304
  38. lemma OAI.PlanarL1.Increment.lifetime_lipschitz line 321
  39. def OAI.PlanarL1.Increment.signedUpdate line 333
  40. lemma OAI.PlanarL1.Increment.signed_lifetime_lipschitz line 336
  41. lemma OAI.PlanarL1.Increment.taper_one line 356
  42. lemma OAI.PlanarL1.Increment.update_plateau line 364
  43. lemma OAI.PlanarL1.Increment.opposite_sign_gain line 371
  44. lemma OAI.PlanarL1.Increment.geometric_separation line 380
  45. def OAI.PlanarL1.Increment.damped line 411

    Source documentation

    The actual increment with an ambient-metric taper. The scalar transverse field is measured intrinsically, while this weight may use the unrestricted metric.

    noncomputable def damped (a r : ℝ) (t w : X → ℝ) (x : X) : ℝ :=
…
  46. lemma OAI.PlanarL1.Increment.damped_lipschitz line 414
  47. def OAI.PlanarL1.Increment.signedDamped line 442
  48. lemma OAI.PlanarL1.Increment.signedDamped_support line 446
  49. lemma OAI.PlanarL1.Increment.damped_lifetime line 453
  50. lemma OAI.PlanarL1.Increment.tapered_magnitude line 491
  51. lemma OAI.PlanarL1.Increment.signed_tapered_magnitude line 505