ProbeRestrictionComposition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Combining the two restrictions on the same probe endpoint

theorem OAI.PolycyclicRecognition.map_cell_lift_conditions line 11

Source documentation

Change the cell predicate without changing the chosen pair of lifts.

theorem map_cell_lift_conditions {N D Z : Type*} {cell : Set Z}
    {S : N → D → Prop} {P Q : N → D → Z → Prop}
    (h : ∃ u d, S u d ∧ ∀ z ∈ cell, P u d z)
    (hmap : ∀ u d z, z ∈ cell → P u d z → Q u d z) :
    ∃ u d, S u d ∧ ∀ z ∈ cell, Q u d z := by
…

theorem OAI.PolycyclicRecognition.choose_eventual_probe_lifts line 24

Source documentation

Choose factor lifts everywhere while retaining the simultaneous restrictions wherever the eventual geometric construction applies.

theorem choose_eventual_probe_lifts {J : ℕ → Type*}
    (project : N × D → G) (hsurj : Function.Surjective project)
    (endpoint : ∀ n, J n → G → G) (points : ∀ n, J n → Finset G)
    (P : ∀ n, J n → G → N × D → Prop)
    (h : ∀ᶠ n in Filter.atTop, ∀ j, ∀ x ∈ points n j,
      ∃ p, project p = endpoint n j x ∧ P n j x p) :
    ∃ p : ∀ n, J n → G → N × D,
      (∀ n j x, project (p n j x) = endpoint n j x) ∧
      ∀ᶠ n in Filter.atTop, ∀ j, ∀ x ∈ points n j, P n j x (p n j x) := by
…

theorem OAI.PolycyclicRecognition.exists_two_frame_probe_lift line 54

Source documentation

The first path's quotient condition and the bridged second path's coordinate conditions hold together for one lift of the first endpoint.

theorem exists_two_frame_probe_lift
    (project : N → D → G) (act : G → Q → Q) (oneQ : Q)
    (cell : Set (N × D)) (region : Set Q)
    (base anchor first second : G) (r : ℝ)
    (B : N → D → Prop) (C : D → N × D → Prop)
    (P : N → D → N × D → Prop)
    (hfirst : ∃ u d, project u d = base⁻¹ * first ∧ B u d ∧
      ∀ z ∈ cell, act ((base⁻¹ * first) * project z.1 z.2) oneQ ∈ region ∧ C d z)
    (hsecond : ∀ bridge : G, dist 1 bridge ≤ r →
      ∃ u d, project u d = (anchor⁻¹ * second) * bridge ∧ ∀ z ∈ cell, P u d z)
    (hdist : dist second first ≤ r) :
    ∃ u d, project u d = anchor⁻¹ * first ∧ ∀ z ∈ cell,
…