OAI/Combinatorics/PlanarL1/Dilation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Columns.Model.dilate line 15

    Source documentation

    Change physical units by a positive factor. This scales the actual switch sets and vertical path lengths; the cyclic link graph is not changed.

    noncomputable def dilate : Model n where
…

    Mentions: OAI.PlanarL1.Columns.Model

  2. lemma OAI.PlanarL1.Columns.Model.mem_dilate_set line 33
  3. lemma OAI.PlanarL1.Columns.Model.dilate_mem_heights line 41
  4. lemma OAI.PlanarL1.Columns.Model.dilate_activeGraph line 45
  5. def OAI.PlanarL1.Columns.Model.Path.dilate line 58
  6. lemma OAI.PlanarL1.Columns.Model.Path.dilate_length line 63
  7. def OAI.PlanarL1.Columns.Model.Path.undilate line 70
  8. lemma OAI.PlanarL1.Columns.Model.Path.undilate_length line 76
  9. def OAI.PlanarL1.Columns.Model.Point.dilate line 90
  10. def OAI.PlanarL1.Columns.Model.Point.undilate line 97
  11. lemma OAI.PlanarL1.Columns.Model.Point.dilate_distance line 104
  12. lemma OAI.PlanarL1.Columns.Model.Point.dilate_dist line 125
  13. lemma OAI.PlanarL1.Columns.Model.Point.undilate_dilate line 128
  14. lemma OAI.PlanarL1.Columns.Model.Point.dilate_undilate line 132
  15. lemma OAI.PlanarL1.Columns.Model.Point.undilate_dist line 137
  16. lemma OAI.PlanarL1.Columns.Model.dilate_set_closed line 146
  17. lemma OAI.PlanarL1.Columns.Model.dilate_set_convex line 155
  18. def OAI.PlanarL1.Columns.Model.Field.dilate line 168

    Source documentation

    Field values have length units too. The vertical Lipschitz constant does not change on passing to new physical units.

    noncomputable def dilate (F : M.Field J L) :
    (M.dilate c hc).Field ((fun T => c*T) '' J) L where
…

    Mentions: OAI.PlanarL1.Columns.Model.Field

  19. lemma OAI.PlanarL1.Columns.Model.Field.dilate_eval line 186
  20. lemma OAI.PlanarL1.Columns.Model.Field.dilate_orderedFrom line 190
  21. lemma OAI.PlanarL1.Columns.Model.Point.dilate_radialValue line 204
  22. def OAI.PlanarL1.Columns.Model.OrdinaryData.dilate line 225
  23. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.dilate_comparison line 234
  24. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.dilate_value line 243
  25. def OAI.PlanarL1.Columns.Model.OrderedData.dilate line 253
  26. lemma OAI.PlanarL1.Columns.Model.OrderedData.dilate_value line 263
  27. def OAI.PlanarL1.Columns.Model.BData.dilate line 272
  28. lemma OAI.PlanarL1.Columns.Model.BData.dilate_band line 276
  29. lemma OAI.PlanarL1.Columns.Model.BData.dilate_value line 279
  30. lemma OAI.PlanarL1.Threshold.dilation_preserving line 295
  31. def OAI.PlanarL1.Threshold.Variables.dilate line 315
  32. lemma OAI.PlanarL1.Threshold.Variables.dilate_active line 323
  33. def OAI.PlanarL1.Columns.Model.Activity.dilate line 341
  34. lemma OAI.PlanarL1.Columns.Model.Activity.dilate_indicator line 346
  35. lemma OAI.PlanarL1.Columns.Model.Activity.dilate_graph line 349
  36. lemma OAI.PlanarL1.Columns.Model.Activity.dilate_component line 357
  37. lemma OAI.PlanarL1.Columns.Model.Activity.dilate_vector line 362
  38. lemma OAI.PlanarL1.Columns.Model.Activity.dilate_cost line 369
  39. def OAI.PlanarL1.Columns.Model.SetSystem.dilate line 380

    Source documentation

    Change a cut system's physical units by the same factor as its columns. The measure, height-coordinate variables, and every scalar chart are all scaled; there is no implicit normalization of label mass.

    noncomputable def dilate (A : SetSystem M Ω μ) :
    SetSystem (M.dilate c hc) Ω (ENNReal.ofReal c • μ) where
…

    Mentions: OAI.PlanarL1.Columns.Model.SetSystem

  40. lemma OAI.PlanarL1.Columns.Model.SetSystem.dilate_movement line 393
  41. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.dilate_origin_reachable line 407
  42. lemma OAI.PlanarL1.Columns.Model.BData.dilate_uses line 421
  43. def OAI.PlanarL1.Columns.Model.OrdinaryState.dilate line 431
  44. def OAI.PlanarL1.Columns.Model.BState.dilate line 457