exists_map_eq_of_sorted_nonempty_iff_wbtw

English

Let l be a nonempty list. There exists a list l' of reals which is sorted such that mapping l' by the line map from head to last yields l, if and only if l has the Wbtw relation with respect to R.

Русский

Пусть l не пуст; существует список l' действительных чисел, упорядоченный по возрастанию, такой что отображение l' линейной карте дает l, тогда и только тогда l удовлетворяет Wbtw по R.

LaTeX

$$$(\\exists l' \\in List(R))\\; l'.Sorted(\\cdot) \\land l'.map(lineMap(head(l), getLast(l))) = l \\iff Wbtw(R,l)$$$

Lean4

theorem exists_map_eq_of_sorted_nonempty_iff_wbtw {l : List P} (hl : l ≠ []) :
    (∃ l' : List R, l'.Sorted (· ≤ ·) ∧ l'.map (lineMap (l.head hl) (l.getLast hl)) = l) ↔ l.Wbtw R :=
  by
  refine ⟨fun ⟨l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
  · rw [← hl'l]
    exact Wbtw.map hl's.wbtw _
  · suffices ∃ l' : List R, (∀ a ∈ l', 0 ≤ a) ∧ l'.Sorted (· ≤ ·) ∧ l'.map (lineMap (l.head hl) (l.getLast hl)) = l
      by
      rcases this with ⟨l', -, hl'⟩
      exact ⟨l', hl'⟩
    induction l with
    | nil => simp at hl
    | cons head tail ih =>
      by_cases ht : tail = []
      · refine ⟨[0], ?_⟩
        simp [ht]
      · rw [wbtw_cons] at h
        replace ih := ih ht h.2
        rcases ih with ⟨l'', hl''0, hl''s, hl''⟩
        simp only [head_cons, getLast_cons ht]
        cases tail with
        | nil => simp at ht
        | cons head2 tail =>
          by_cases ht2 : tail = []
          · exact ⟨[0, 1], by simp [ht2]⟩
          · simp only [head_cons, getLast_cons ht2] at hl'' ⊢
            rw [pairwise_cons] at h
            have hw := h.1.1 _ (getLast_mem ht2)
            rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
            refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
            · simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index, and_imp,
                forall_apply_eq_imp_iff₂, true_and]
              intro a ha
              have := hl''0 a ha
              nlinarith
            · simp only [sorted_cons, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.map _ fun a b hab ↦ ?_
                gcongr
                linarith
            · simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq, map_inj_left, Function.comp_apply,
                lineMap_lineMap_left, lineMap_eq_lineMap_iff, true_and]
              ring_nf
              simp

Похожие утверждения