OAI/Combinatorics/PlanarL1/Cuts.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarL1.Columns.Model.Activity line 11

   Source documentation

   One label of a nested-set system. Nesting and exact switching are the set invariants, not any embedding or separation assumption.

   structure Activity {n : ℕ} (M : Model n) where
   …

   Mentions: OAI.PlanarL1.Columns.Model

2. def OAI.PlanarL1.Columns.Model.Activity.graph line 22
3. lemma OAI.PlanarL1.Columns.Model.Activity.graph_le line 31
4. def OAI.PlanarL1.Columns.Model.Activity.component line 35
5. lemma OAI.PlanarL1.Columns.Model.Activity.mem_component_self line 37
6. lemma OAI.PlanarL1.Columns.Model.Activity.component_eq_iff line 39
7. def OAI.PlanarL1.Columns.Model.Activity.vector line 51

   Source documentation

   Active points get a single component coordinate; inactive points get zero. The finite coordinate set consists of all subsets of columns.

   noncomputable def vector (i : Fin n) (H : ℝ) (S : Set (Fin n)) : ℝ :=
   …

8. def OAI.PlanarL1.Columns.Model.Activity.indicator line 54
9. def OAI.PlanarL1.Columns.Model.Activity.cost line 56
10. lemma OAI.PlanarL1.Columns.Model.Activity.cost_nonneg line 59
11. lemma OAI.PlanarL1.Columns.Model.Activity.vector_inactive line 63
12. lemma OAI.PlanarL1.Columns.Model.Activity.vector_active line 67
13. lemma OAI.PlanarL1.Columns.Model.Activity.cost_comm line 71
14. lemma OAI.PlanarL1.Columns.Model.Activity.sum_vector line 77
15. lemma OAI.PlanarL1.Columns.Model.Activity.vector_nonneg line 86
16. lemma OAI.PlanarL1.Columns.Model.Activity.dominates_indicator line 90
17. lemma OAI.PlanarL1.Columns.Model.Activity.cost_triangle line 95
18. lemma OAI.PlanarL1.Columns.Model.Activity.cost_vertical line 101
19. lemma OAI.PlanarL1.Columns.Model.Activity.vector_switch line 119
20. lemma OAI.PlanarL1.Columns.Model.Activity.cost_switch line 129
21. lemma OAI.PlanarL1.Columns.Model.Activity.cost_of_active_distinct line 132
22. lemma OAI.PlanarL1.Columns.Model.Activity.terminal_isolated line 150

    Source documentation

    An inactive terminal tip isolates BOTH of its endpoint columns in the active-link graph. This uses the terminal-switch standing hypothesis.

    lemma terminal_isolated {a b : Fin n} {H : ℝ}
        (hH : H ∈ M.heights a b) (hn : ¬ Consecutive a b) (hA : ¬ A.active a H) :
        (∀ k, ¬ A.graph.Adj a k) ∧ (∀ k, ¬ A.graph.Adj b k) := by
    …

    Mentions: OAI.PlanarL1.Columns.Consecutive

23. lemma OAI.PlanarL1.Columns.Model.Activity.separated_components line 162
24. lemma OAI.PlanarL1.Columns.Model.Activity.terminal_certificate line 181

    Source documentation

    Exact labelwise component-certificate separation (sets:component-refinement). The other switches may change arbitrarily, subject only to the invariants.

    lemma terminal_certificate {a b x y : Fin n} {H s t : ℝ}
        (hH : H ∈ M.heights a b) (hn : ¬ Consecutive a b) (hA : ¬ A.active a H)
        (hx : a < x ∧ x < b) (hy : y < a ∨ b < y)
        (hs : A.active x s) (ht : A.active y t) : A.cost x y s t = 2 :=
    …

    Mentions: OAI.PlanarL1.Columns.Consecutive

25. def OAI.PlanarL1.Columns.Model.Activity.pathCost line 188

    Source documentation

    The unrefined costs of the vertical pieces of an ACTUAL permitted path.

    noncomputable def pathCost {J : Set ℝ} : {i j : Fin n} → M.Path J i j → ℝ → ℝ → ℝ
      | _, _, .nil i, s, t => |A.indicator i s-A.indicator i t|
      | i, _, .cons H _ _ p, s, t => |A.indicator i s-A.indicator i H|+pathCost p H t

26. lemma OAI.PlanarL1.Columns.Model.Activity.cost_le_pathCost line 192
27. structure OAI.PlanarL1.Columns.Model.SetSystem line 212

    Source documentation

    The exact hypotheses in the component-refinement lemma, put on an actual measure space. The vertical bound is the invariant of the cut construction.

    structure SetSystem {n : ℕ} (M : Model n) (Ω : Type*) [MeasurableSpace Ω]
        (μ : Measure Ω) where
    …

    Mentions: OAI.PlanarL1.Columns.Model

28. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_indicator line 225
29. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_adj line 231

    Source documentation

    Compactness and monotonicity reduce active-link measurability to ONE fixed height. There is no uncountable union of switching events.

    lemma measurable_adj (i j : Fin n) :
        MeasurableSet {ω | (A.activity ω).graph.Adj i j} := by
    …

30. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_graph_fiber line 254
31. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_component line 272
32. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_vector line 279
33. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_cost line 286
34. lemma OAI.PlanarL1.Columns.Model.SetSystem.pathCost_integrable line 292
35. lemma OAI.PlanarL1.Columns.Model.SetSystem.integral_pathCost_le line 298
36. lemma OAI.PlanarL1.Columns.Model.SetSystem.cost_integrable line 308
37. lemma OAI.PlanarL1.Columns.Model.SetSystem.integral_cost_le_length line 315
38. lemma OAI.PlanarL1.Columns.Model.SetSystem.integral_cost_le_dist line 321
39. def OAI.PlanarL1.Columns.Model.SetSystem.coordinateDifference line 330
40. lemma OAI.PlanarL1.Columns.Model.SetSystem.measurable_coordinateDifference line 334
41. lemma OAI.PlanarL1.Columns.Model.SetSystem.integrable_coordinateDifference line 340
42. lemma OAI.PlanarL1.Columns.Model.SetSystem.integral_norm_coordinates line 358
43. def OAI.PlanarL1.Columns.Model.SetSystem.refinedMap line 371

    Source documentation

    Subtracting the actual reference point makes the component assignment integrable, even when the original label measure is infinite.

    noncomputable def refinedMap {J : Set ℝ} {root : Fin n} (o x : M.Point J root) :
        Lp ℝ 1 (μ.prod (Measure.count : Measure (Set (Fin n)))) :=
    …

44. lemma OAI.PlanarL1.Columns.Model.SetSystem.norm_refinedMap_sub line 376
45. lemma OAI.PlanarL1.Columns.Model.SetSystem.refinedMap_lipschitz line 397
46. lemma OAI.PlanarL1.Columns.Model.SetSystem.unrefined_integrable line 403
47. lemma OAI.PlanarL1.Columns.Model.SetSystem.refinedMap_dominates line 412
48. lemma OAI.PlanarL1.Columns.Model.SetSystem.refinedMap_terminal_certificate line 424

    Source documentation

    The actual final certificate yields twice its label mass in the refined real L1 map. Its mass is necessarily finite, although μ itself is infinite.

    lemma refinedMap_terminal_certificate {J : Set ℝ} {root : Fin n} (o x y : M.Point J root)
        {a b : Fin n} {H : ℝ} (hH : H ∈ M.heights a b) (hn : ¬ Consecutive a b)
        (hx : a < x.column ∧ x.column < b) (hy : y.column < a ∨ b < y.column)
        (E : Set Ω) (hE : MeasurableSet E)
        (hA : ∀ ω ∈ E, ¬ (A.activity ω).active a H)
        (hX : ∀ ω ∈ E, (A.activity ω).active x.column x.height)
        (hY : ∀ ω ∈ E, (A.activity ω).active y.column y.height) :
        μ E < ⊤ ∧ 2*μ.real E ≤ ‖A.refinedMap o x-A.refinedMap o y‖ := by
    …

    Mentions: OAI.PlanarL1.Columns.Consecutive

49. def OAI.PlanarL1.Columns.Model.Activity.movement line 473

    Source documentation

    Pointwise membership movement; component labels are deliberately not moved.

    noncomputable def movement (A B : Activity M) (i : Fin n) (H : ℝ) : ℝ :=
    …

    Mentions: OAI.PlanarL1.Columns.Model.Activity

50. lemma OAI.PlanarL1.Columns.Model.Activity.movement_nonneg line 476
51. lemma OAI.PlanarL1.Columns.Model.Activity.terminal_survival line 479
52. def OAI.PlanarL1.Columns.Model.SetSystem.movement line 504
53. lemma OAI.PlanarL1.Columns.Model.SetSystem.movement_nonneg line 507
54. lemma OAI.PlanarL1.Columns.Model.SetSystem.movement_triangle line 510
55. lemma OAI.PlanarL1.Columns.Model.SetSystem.refined_certificate_survival line 537

    Source documentation

    Survival of the source's component certificate after arbitrary later unrefined movements at the two vertices and the fixed bridge tip. No estimate on changes of active-component labels is used or assumed.

    lemma refined_certificate_survival [SFinite μ] {J : Set ℝ} {root : Fin n} (o x y : M.Point J root)
        {a b : Fin n} {H : ℝ} (hH : H ∈ M.heights a b) (hn : ¬ Consecutive a b)
        (hx : a<x.column ∧ x.column<b) (hy : y.column<a ∨ b<y.column)
        (E : Set Ω) (hE : MeasurableSet E)
        (ha : ∀ ω ∈ E, ¬ (A.activity ω).active a H)
        (hax : ∀ ω ∈ E, (A.activity ω).active x.column x.height)
        (hay : ∀ ω ∈ E, (A.activity ω).active y.column y.height)
        (hmove : ∀ i H, Integrable (fun ω => (B.activity ω).indicator i H-
          (A.activity ω).indicator i H) μ) :
        2*μ.real E ≤ ‖B.refinedMap o x-B.refinedMap o y‖+
          2*(A.movement B x.column x.height+A.movement B y.column y.height+A.movement B a H) := by
    …

    Mentions: OAI.PlanarL1.Columns.Consecutive