AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleQuantitativeNeighborhood

No declaration docstring.

theorem exists_pairwiseDisjoint_bounded_open_rectangles_of_cycleValue_pos
    {n : ℕ} {p : Fin (n + 1) → E × E}
    (hp : Function.Injective p)
    (hpos : 0 < cycleValue p)
    {r : ℝ} (hr : 0 < r) :
    ∃ ε : ℝ, 0 < ε ∧
      ∃ U : Fin (n + 1) → Set E, ∃ V : Fin (n + 1) → Set E,
        (∀ i, IsOpen (U i) ∧ (p i).1 ∈ U i ∧ U i ⊆ Metric.ball (p i).1 r) ∧
        (∀ i, IsOpen (V i) ∧ (p i).2 ∈ V i ∧ V i ⊆ Metric.ball (p i).2 r) ∧
        Set.Pairwise (Set.univ : Set (Fin (n + 1)))
          (Function.onFun Disjoint fun i => U i ×ˢ V i) ∧
        ∀ q : Fin (n + 1) → E × E,
          (∀ i, q i ∈ U i ×ˢ V i) → ε < cycleValue q := by
  let ε : ℝ := cycleValue p / 2
  have hεpos : 0 < ε := by
    dsimp [ε]
    linarith
  have hεp : ε < cycleValue p := by
    dsimp [ε]
    linarith

  let good : Set (Fin (n + 1) → E × E) := {q | ε < cycleValue q}
  have hgoodOpen : IsOpen good := isOpen_lt continuous_const continuous_cycleValue
  have hpGood : p ∈ good := hεp
  obtain ⟨C, hC, hCgood⟩ :=
    (isOpen_pi_iff' (s := good)).mp hgoodOpen p hpGood

  let R : Set (E × E) := Set.range p
  have hR : R.Finite := Set.finite_range p
  obtain ⟨W, hW, hWpair⟩ := hR.t2_separation

  have hcoordNhds : ∀ i, C i ∩ W (p i) ∈ 𝓝 (p i) := by
    intro i
    apply inter_mem
    · exact IsOpen.mem_nhds (hC i).1 (hC i).2
    · exact IsOpen.mem_nhds (hW (p i)).2 (hW (p i)).1

  choose U₀ V₀ hUopen hpU hVopen hpV hrect using
    fun i => mem_nhds_prod_iff'.mp (hcoordNhds i)

  let U : Fin (n + 1) → Set E := fun i => U₀ i ∩ Metric.ball (p i).1 r
  let V : Fin (n + 1) → Set E := fun i => V₀ i ∩ Metric.ball (p i).2 r

  refine ⟨ε, hεpos, U, V, ?_, ?_, ?_, ?_⟩
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCycleQuantitativeNeighborhood.lean:25published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.