IntervalChain.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.IntervalChain.exists_irredundant_subcover line 13

Source documentation

A finite cover can be reduced so that no selected set is contained in another selected set.

theorem exists_irredundant_subcover {ι : Type uIota} {X : Type uX}
    (s : Finset ι) (U : ι → Set X) (K : Set X)
    (hcover : ∀ x ∈ K, ∃ i ∈ s, x ∈ U i) :
    ∃ t : Finset ι, t ⊆ s ∧
      (∀ x ∈ K, ∃ i ∈ t, x ∈ U i) ∧
      ∀ i ∈ t, ∀ j ∈ t, i ≠ j → ¬ U i ⊆ U j := by
…

theorem OAI.Problem326.IntervalChain.exists_finite_center_cover line 35

Source documentation

Compactness supplies finitely many centers from the original interval.

theorem exists_finite_center_cover {a b : ℝ} (ρ : ℝ → ℝ)
    (hρ : ∀ t ∈ Set.Icc a b, 0 < ρ t) :
    ∃ s : Finset ℝ,
      (∀ t ∈ s, t ∈ Set.Icc a b) ∧
      ∀ x ∈ Set.Icc a b, ∃ t ∈ s, x ∈ Set.Ioo (t - ρ t) (t + ρ t) := by
…

theorem OAI.Problem326.IntervalChain.endpoints_strictMono line 58

Source documentation

Noncontainment forces the interval endpoints to be ordered in the same way as their centers.

theorem endpoints_strictMono {u v ru rv : ℝ}
    (huv : u < v)
    (hnot : ¬ Set.Ioo (u - ru) (u + ru) ⊆ Set.Ioo (v - rv) (v + rv))
    (hnot' : ¬ Set.Ioo (v - rv) (v + rv) ⊆ Set.Ioo (u - ru) (u + ru)) :
    u - ru < v - rv ∧ u + ru < v + rv := by
…

theorem OAI.Problem326.IntervalChain.adjacent_overlap line 77

Source documentation

Successive selected intervals overlap when their union covers the whole interval and their endpoint order follows their center order.

theorem adjacent_overlap {a b : ℝ} {ρ : ℝ → ℝ} {s : Finset ℝ}
    (hcenters : ∀ t ∈ s, t ∈ Set.Icc a b)
    (hρ : ∀ t ∈ s, 0 < ρ t)
    (hcover : ∀ x ∈ Set.Icc a b, ∃ t ∈ s, x ∈ Set.Ioo (t - ρ t) (t + ρ t))
    (horder : ∀ u ∈ s, ∀ v ∈ s, u < v →
      u - ρ u < v - ρ v ∧ u + ρ u < v + ρ v)
    {u v : ℝ} (hu : u ∈ s) (hv : v ∈ s) (huv : u < v)
    (hadj : ∀ w ∈ s, u < w → v ≤ w) :
    v - ρ v < u + ρ u := by
…

theorem OAI.Problem326.IntervalChain.exists_transition_cut line 107

Source documentation

An overlapping pair admits a transition cut in both neighborhoods and strictly between the two centers.

theorem exists_transition_cut {u v ru rv : ℝ}
    (huv : u < v) (hru : 0 < ru) (hrv : 0 < rv)
    (hoverlap : v - rv < u + ru) :
    ∃ q : ℝ, u < q ∧ q < v ∧
      q ∈ Set.Ioo (u - ru) (u + ru) ∧
      q ∈ Set.Ioo (v - rv) (v + rv) := by
…

theorem OAI.Problem326.IntervalChain.left_endpoint_mem line 125

Source documentation

The first selected neighborhood contains the left endpoint.

theorem left_endpoint_mem {a b : ℝ} {ρ : ℝ → ℝ} {s : Finset ℝ}
    (hab : a ≤ b)
    (hcenters : ∀ t ∈ s, t ∈ Set.Icc a b)
    (hρ : ∀ t ∈ s, 0 < ρ t)
    (hcover : ∀ x ∈ Set.Icc a b, ∃ t ∈ s, x ∈ Set.Ioo (t - ρ t) (t + ρ t))
    (horder : ∀ u ∈ s, ∀ v ∈ s, u < v →
      u - ρ u < v - ρ v ∧ u + ρ u < v + ρ v)
    {u : ℝ} (hu : u ∈ s) (hmin : ∀ w ∈ s, u ≤ w) :
    a ∈ Set.Ioo (u - ρ u) (u + ρ u) := by
…

theorem OAI.Problem326.IntervalChain.right_endpoint_mem line 144

Source documentation

The last selected neighborhood contains the right endpoint.

theorem right_endpoint_mem {a b : ℝ} {ρ : ℝ → ℝ} {s : Finset ℝ}
    (hab : a ≤ b)
    (hcenters : ∀ t ∈ s, t ∈ Set.Icc a b)
    (hρ : ∀ t ∈ s, 0 < ρ t)
    (hcover : ∀ x ∈ Set.Icc a b, ∃ t ∈ s, x ∈ Set.Ioo (t - ρ t) (t + ρ t))
    (horder : ∀ u ∈ s, ∀ v ∈ s, u < v →
      u - ρ u < v - ρ v ∧ u + ρ u < v + ρ v)
    {v : ℝ} (hv : v ∈ s) (hmax : ∀ w ∈ s, w ≤ v) :
    b ∈ Set.Ioo (v - ρ v) (v + ρ v) := by
…

theorem OAI.Problem326.IntervalChain.exists_interval_chain line 165

Source documentation

Assemble ordered centers and transition cuts. The endpoint and overlap conditions imply each closed interval between neighboring cuts lies in its assigned neighborhood.

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