IntervalGluing.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Elementary interval-gluing facts for the affine-label construction.

theorem OAI.Problem326.IntervalGluing.exists_maximal_subfamily line 11

Source documentation

Removing nonmaximal members of a finite family preserves its union.

theorem exists_maximal_subfamily {α : Type uAlpha} {β : Type uBeta} (S : Finset α) (U : α → Set β) :
    ∃ T : Finset α, T ⊆ S ∧
      (∀ x ∈ S, ∃ y ∈ T, U x ⊆ U y) ∧
      (∀ x ∈ T, ∀ y ∈ T, U x ⊆ U y → U y ⊆ U x) := by
…

theorem OAI.Problem326.IntervalGluing.endpoints_order_of_noncontainment line 30

Source documentation

For centered intervals, noncontainment forces both endpoints to follow the order of the centers.

theorem endpoints_order_of_noncontainment {t u r s : ℝ}
    (htu : t < u)
    (hntu : ¬ Set.Ioo (t-r) (t+r) ⊆ Set.Ioo (u-s) (u+s))
    (hnut : ¬ Set.Ioo (u-s) (u+s) ⊆ Set.Ioo (t-r) (t+r)) :
    t-r < u-s ∧ t+r < u+s := by
…

theorem OAI.Problem326.IntervalGluing.center_eq_of_mutual_subset line 48

Source documentation

Two nonempty centered intervals with mutual inclusion have equal centers.

theorem center_eq_of_mutual_subset {t u r s : ℝ} (hr : 0 < r) (hs : 0 < s)
    (h₁ : Set.Ioo (t-r) (t+r) ⊆ Set.Ioo (u-s) (u+s))
    (h₂ : Set.Ioo (u-s) (u+s) ⊆ Set.Ioo (t-r) (t+r)) : t = u := by
…

theorem OAI.Problem326.IntervalGluing.exists_ordered_interval_cover line 58

Source documentation

An arbitrary positive radius function on a compact interval has a finite centered subcover whose centers and both endpoint lists are strictly ordered. No continuity of the radius function is required.

theorem exists_ordered_interval_cover {a b : ℝ} (hab : a ≤ b)
    (r : ℝ → ℝ) (hr : ∀ t ∈ Set.Icc a b, 0 < r t) :
    ∃ n : ℕ, ∃ t : Fin (n+1) → ℝ,
      StrictMono t ∧ (∀ i, t i ∈ Set.Icc a b) ∧
      StrictMono (fun i => t i - r (t i)) ∧
      StrictMono (fun i => t i + r (t i)) ∧
      (∀ x ∈ Set.Icc a b, ∃ i, x ∈ Set.Ioo (t i-r (t i)) (t i+r (t i))) := by
…

theorem OAI.Problem326.IntervalGluing.exists_overlap_cut line 115

Source documentation

Overlapping intervals with ordered centers admit a transition cut inside both intervals and strictly between their centers.

theorem exists_overlap_cut {t u L R L' R' : ℝ}
    (htu : t < u) (hLt : L < t) (htR : t < R)
    (hLu : L' < u) (huR : u < R') (hoverlap : L' < R) :
    ∃ q : ℝ, t < q ∧ q < u ∧ q ∈ Set.Ioo L R ∧ q ∈ Set.Ioo L' R' := by
…

theorem OAI.Problem326.IntervalGluing.consecutive_overlap line 130

Source documentation

In an ordered interval cover, neighboring intervals overlap. Ordering both endpoints is the property obtained by deleting contained intervals.

theorem consecutive_overlap {n : ℕ} {a b : ℝ}
    (t L R : Fin (n + 1) → ℝ)
    (hL : StrictMono L) (hR : StrictMono R)
    (hcenter : ∀ j, L j < t j ∧ t j < R j)
    (hcenter_mem : ∀ j, t j ∈ Set.Icc a b)
    (hcover : ∀ x ∈ Set.Icc a b, ∃ j, x ∈ Set.Ioo (L j) (R j))
    (i : Fin n) : L i.succ < R i.castSucc := by
…

theorem OAI.Problem326.IntervalGluing.exists_consecutive_cuts line 154

Source documentation

A simultaneous choice of all transition cuts in an ordered interval cover.

theorem exists_consecutive_cuts {n : ℕ} {a b : ℝ}
    (t L R : Fin (n + 1) → ℝ)
    (ht : StrictMono t) (hL : StrictMono L) (hR : StrictMono R)
    (hcenter : ∀ j, L j < t j ∧ t j < R j)
    (hcenter_mem : ∀ j, t j ∈ Set.Icc a b)
    (hcover : ∀ x ∈ Set.Icc a b, ∃ j, x ∈ Set.Ioo (L j) (R j)) :
    ∃ q : Fin n → ℝ, ∀ i,
      t i.castSucc < q i ∧ q i < t i.succ ∧
      q i ∈ Set.Ioo (L i.castSucc) (R i.castSucc) ∧
      q i ∈ Set.Ioo (L i.succ) (R i.succ) := by
…

theorem OAI.Problem326.IntervalGluing.endpoint_membership line 177

Source documentation

In an ordered centered cover, the first and last intervals contain the corresponding endpoints of the covered compact interval.

theorem endpoint_membership {n : ℕ} {a b : ℝ} (hab : a ≤ b)
    (t L R : Fin (n+1) → ℝ) (hL : StrictMono L) (hR : StrictMono R)
    (hcenter : ∀ j, L j < t j ∧ t j < R j)
    (hcenter_mem : ∀ j, t j ∈ Set.Icc a b)
    (hcover : ∀ x ∈ Set.Icc a b, ∃ j, x ∈ Set.Ioo (L j) (R j)) :
    a ∈ Set.Ioo (L 0) (R 0) ∧
    b ∈ Set.Ioo (L (Fin.last n)) (R (Fin.last n)) := by
…

theorem OAI.Problem326.IntervalGluing.exists_interval_gluing line 196

Source documentation

Finite interval gluing data for an arbitrary positive radius function. The chosen transition cuts lie in both adjacent intervals and strictly between adjacent centers. Together with endpoint membership this covers every closed piece between successive cuts by its designated interval.

theorem exists_interval_gluing {a b : ℝ} (hab : a ≤ b)
    (r : ℝ → ℝ) (hr : ∀ t ∈ Set.Icc a b, 0 < r t) :
    ∃ n : ℕ, ∃ t : Fin (n+1) → ℝ, ∃ q : Fin n → ℝ,
      StrictMono t ∧ (∀ i, t i ∈ Set.Icc a b) ∧
      (a ∈ Set.Ioo (t 0-r (t 0)) (t 0+r (t 0))) ∧
      (b ∈ Set.Ioo (t (Fin.last n)-r (t (Fin.last n)))
        (t (Fin.last n)+r (t (Fin.last n)))) ∧
      (∀ i, t i.castSucc < q i ∧ q i < t i.succ ∧
        q i ∈ Set.Ioo (t i.castSucc-r (t i.castSucc))
          (t i.castSucc+r (t i.castSucc)) ∧
        q i ∈ Set.Ioo (t i.succ-r (t i.succ)) (t i.succ+r (t i.succ))) := by
…