OAI/Combinatorics/PlanarL1/Fields.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarL1.Columns.Model.Field line 14

   Source documentation

   A scalar field on the whole band, including all its components. Its only compatibility condition is equality at actual allowed switch heights.

   structure Field (J : Set ℝ) (L : NNReal) where
   …

2. lemma OAI.PlanarL1.Columns.Model.Field.path_bound line 23
3. lemma OAI.PlanarL1.Columns.Model.Field.lipschitz line 39

   Source documentation

   Vertical Lipschitz bounds and switch equality imply the intrinsic bound, by summing on an actual attaining shortest path.

   lemma lipschitz (F : M.Field J L) (hJ : IsClosed J) (root : Fin n) :
       LipschitzWith L (fun x : M.Point J root => F.value x.column ⟨x.height,x.inBand⟩) := by
   …

4. def OAI.PlanarL1.Columns.Model.Point.truncated line 55

   Source documentation

   Truncated point distance on EVERY column. Columns outside the metric component have the constant ceiling.

   noncomputable def truncated (o : M.Point J root) (D : ℝ) (i : Fin n) (H : J) : ℝ := by
   …

5. lemma OAI.PlanarL1.Columns.Model.Point.truncated_of_reachable line 60
6. lemma OAI.PlanarL1.Columns.Model.Point.truncated_le line 65
7. lemma OAI.PlanarL1.Columns.Model.Point.truncated_vertical line 72
8. lemma OAI.PlanarL1.Columns.Model.Point.truncated_switch line 97
9. def OAI.PlanarL1.Columns.Model.Point.truncatedField line 115
10. lemma OAI.PlanarL1.Columns.Model.Point.truncated_root line 120
11. lemma OAI.PlanarL1.Columns.Model.Point.truncated_minimum line 125
12. lemma OAI.PlanarL1.Columns.Model.Point.truncated_sublevel_path line 136

    Source documentation

    The strict sublevel connects to the root by a real shortest switching path; every visited column remains in the same strict sublevel.

    lemma truncated_sublevel_path (hJ : IsClosed J) (o : M.Point J root) (D t : ℝ)
        (ht : t ≤ D) (i : Fin n) (H : J) (hi : o.truncated D i H < t) :
        ∃ w : (M.activeGraph J).Walk i o.column,
          ∀ z ∈ w.support, o.truncated D z H < t := by
    …

13. def OAI.PlanarL1.Columns.Model.Point.supportValue line 158

    Source documentation

    The literal running-minimum projection of point distance, after cutting at the chosen representative of the root.

    noncomputable def supportValue {k : ℕ} {M : Model (k + 1)} {J : Set ℝ} {r : Fin (k + 1)}
        (o w : M.Point J r) (i : Fin (k + 1)) (H : J) : ℝ :=
    …

    Mentions: OAI.PlanarL1.Columns.Model

14. lemma OAI.PlanarL1.Columns.Model.Point.supportValue_vertical line 164
15. lemma OAI.PlanarL1.Columns.Model.Point.supportValue_switch line 168
16. def OAI.PlanarL1.Columns.Model.Point.supportField line 201

    Source documentation

    Ordered support, with actual vertical and switch proofs.

    noncomputable def supportField {k : ℕ} {M : Model (k + 1)} {J : Set ℝ} {r : Fin (k + 1)}
        (hJ : IsClosed J) (o w : M.Point J r) : M.Field J 1 where
    …

    Mentions: OAI.PlanarL1.Columns.Model

17. lemma OAI.PlanarL1.Columns.Model.Point.supportValue_root line 207
18. lemma OAI.PlanarL1.Columns.Model.Point.supportValue_target line 213
19. lemma OAI.PlanarL1.Columns.Model.Point.supportValue_bounds line 219
20. def OAI.PlanarL1.Columns.Model.Field.OrderedFrom line 240

    Source documentation

    Monotonicity on the two arcs, expressed in the circle cut at a. The separate minimum condition records the wrap-around step to index zero.

    def Field.OrderedFrom {k : ℕ} {M : Model (k + 1)} {J : Set ℝ} {L : NNReal}
        (F : M.Field J L) (a b : Fin (k + 1)) : Prop :=
    …

    Mentions: OAI.PlanarL1.Columns.Model

21. lemma OAI.PlanarL1.Columns.Model.Point.supportField_ordered line 250
22. theorem OAI.PlanarL1.Columns.Model.Point.exists_ordered_support line 279

    Source documentation

    Lemma ord:support, on every representative of the whole band. No connectivity of the whole band is assumed. The upper distance bound is on the chosen finite-distance component, just as the source's infinite convention.

    theorem exists_ordered_support {k : ℕ} {M : Model (k + 1)} {J : Set ℝ} {r : Fin (k + 1)}
        (hJ : IsClosed J) (o w : M.Point J r) :
        ∃ F : M.Field J 1, F.OrderedFrom o.column w.column ∧
          (∀ i H, 0 ≤ F.value i H ∧ F.value i H ≤ dist o w) ∧
          F.value o.column ⟨o.height,o.inBand⟩ = 0 ∧
          F.value w.column ⟨w.height,w.inBand⟩ = dist o w ∧
          ∀ x : M.Point J r, F.value x.column ⟨x.height,x.inBand⟩ ≤ dist o x := by
    …

    Mentions: OAI.PlanarL1.Columns.Model

23. def OAI.PlanarL1.Columns.Model.Field.arcSign line 303

    Source documentation

    Signed open-arc membership. Boundary columns have sign zero.

    def arcSign {k : ℕ} (a b i : Fin (k + 1)) : ℝ :=
    …

24. lemma OAI.PlanarL1.Columns.Model.Field.arcSign_cases line 306
25. lemma OAI.PlanarL1.Columns.Model.Field.arcSign_zero_iff line 311
26. lemma OAI.PlanarL1.Columns.Model.Field.abs_arcSign_le line 316
27. def OAI.PlanarL1.Columns.Model.Field.wall line 321

    Source documentation

    Source Z_s in the max metric on R x R: the two boundary images and the images of actual switches between opposite OPEN arcs.

    def wall {k : ℕ} {M : Model (k + 1)} {J : Set ℝ} {L : NNReal}
        (F : M.Field J L) (a b : Fin (k + 1)) : Set (ℝ × ℝ) :=
    …

    Mentions: OAI.PlanarL1.Columns.Model

28. lemma OAI.PlanarL1.Columns.Model.Field.wall_nonempty line 328
29. lemma OAI.PlanarL1.Columns.Model.Field.wall_of_boundary line 332
30. lemma OAI.PlanarL1.Columns.Model.Field.wall_of_switch line 339
31. def OAI.PlanarL1.Columns.Model.Field.transverseValue line 358
32. lemma OAI.PlanarL1.Columns.Model.Field.coordinate_lipschitz line 362
33. lemma OAI.PlanarL1.Columns.Model.Field.transverse_vertical line 373
34. lemma OAI.PlanarL1.Columns.Model.Field.transverse_switch line 384
35. def OAI.PlanarL1.Columns.Model.Field.transverse line 396

    Source documentation

    The transverse field. Its slope bound is inherited from the original field (and at least one), with the switch identity proved.

    noncomputable def transverse {k : ℕ} {M : Model (k + 1)} {J : Set ℝ} {L : NNReal}
        (F : M.Field J L) (hL : 1 ≤ L) (a b : Fin (k + 1)) : M.Field J L where
    …

    Mentions: OAI.PlanarL1.Columns.Model

36. lemma OAI.PlanarL1.Columns.Model.Field.transverse_abs line 402
37. def OAI.PlanarL1.Columns.Model.Path.trace line 419

    Source documentation

    The actual set of representatives visited by a finite switching path, including every point of its vertical segments.

    def trace : {i j : Fin n} → M.Path J i j → ℝ → ℝ → Set (Fin n × ℝ)
      | i, _, .nil _, a, b => {z | z.1 = i ∧ z.2 ∈ Set.uIcc a b}
      | i, _, .cons H _ _ p, a, b => {z | z.1 = i ∧ z.2 ∈ Set.uIcc a H} ∪ p.trace H b

38. lemma OAI.PlanarL1.Columns.Model.Path.trace_column line 423
39. lemma OAI.PlanarL1.Columns.Model.Path.trace_height line 433
40. lemma OAI.PlanarL1.Columns.Model.Path.abs_split line 442
41. lemma OAI.PlanarL1.Columns.Model.Path.trace_split line 457

    Source documentation

    A visit admits an exact-length prefix and suffix, not just an unrelated path to the same column.

    lemma trace_split {i j : Fin n} (p : M.Path J i j) {a b : ℝ} {z : Fin n × ℝ}
        (hz : z ∈ p.trace a b) : ∃ (q : M.Path J i z.1) (r : M.Path J z.1 j),
          q.length a z.2 + r.length z.2 b = p.length a b := by
    …

42. lemma OAI.PlanarL1.Columns.Model.Field.vertical_intermediate line 481
43. lemma OAI.PlanarL1.Columns.Model.Field.path_intermediate line 495

    Source documentation

    Every intermediate scalar value on a switching path is attained on its actual trace. Switch compatibility supplies continuity across the joins.

    lemma path_intermediate (F : M.Field J L) (hJ : Set.OrdConnected J) {i j : Fin n}
        (p : M.Path J i j) (a b : J) {c : ℝ} (ha : F.value i a ≤ c) (hb : c ≤ F.value j b) :
        ∃ (v : Fin n) (T : J), (v,T.val) ∈ p.trace a.val b.val ∧ F.value v T = c := by
    …

44. abbrev OAI.PlanarL1.Columns.Model.Component line 516

    Source documentation

    The metric component is precisely the separation quotient of the intrinsic pseudometric on representatives. No additional edges are inserted.

    abbrev Component (J : Set ℝ) (root : Fin n) := SeparationQuotient (M.Point J root)
    …

45. def OAI.PlanarL1.Columns.Model.Point.extendValue line 534

    Source documentation

    A Lipschitz scalar on one intrinsic component, continued constantly on the other components, is a genuine vertical/switch-compatible field.

    noncomputable def extendValue (f : M.Point J root → ℝ) (i : Fin n) (H : J) : ℝ := by
    …

46. lemma OAI.PlanarL1.Columns.Model.Point.extendValue_point line 538
47. lemma OAI.PlanarL1.Columns.Model.Point.extendValue_vertical line 542
48. lemma OAI.PlanarL1.Columns.Model.Point.extendValue_switch line 556
49. def OAI.PlanarL1.Columns.Model.Point.extendField line 574
50. lemma OAI.PlanarL1.Columns.Model.Point.intermediate_between line 582

    Source documentation

    A continuous scalar intermediate value is attained on an actual shortest switching path, with the exact metric betweenness identity.

    lemma intermediate_between {K : ℝ≥0} (f : M.Point J root → ℝ) (hf : LipschitzWith K f)
        (hJ : IsClosed J) (hI : Set.OrdConnected J) (x y : M.Point J root) {c : ℝ}
        (hx : f x ≤ c) (hy : c ≤ f y) :
        ∃ z : M.Point J root, f z=c ∧ dist x z+dist z y=dist x y := by
    …