AutoSamplingTheory.TechnicalLemmas.Analysis.PairingClosedChain

- Affine value of a finite chain at a terminal source point `z`. For `[p₀,...,pₖ]`, this is `Σ_{j<k} <p_j.2, p_{j+1}.1-p_j.1> + <p_k.2, z-p_k.1>`.

def chainValue : List (E × E) → E → ℝ
  | [], _ => 0
  | [p], z => inner ℝ p.2 (z - p.1)
  | p :: q :: rest, z =>
      inner ℝ p.2 (q.1 - p.1) + chainValue (q :: rest) z

/-- The rooted list condition consumed by the Rockafellar potential: closing a
nonempty chain back at the source coordinate of its head has nonpositive value. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:32published source at 0e31a3cda412

- The rooted list condition consumed by the Rockafellar potential: closing a nonempty chain back at the source coordinate of its head has nonpositive value.

def PairingClosedChainMonotone (Gamma : Set (E × E)) : Prop :=
  ∀ ⦃l : List (E × E)⦄ ⦃base : E × E⦄,
    l ≠ [] → l.head? = some base →
      List.Forall (fun p => p ∈ Gamma) l →
      chainValue l base.1 ≤ 0

@[simp]

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:40published source at 0e31a3cda412

No declaration docstring.

theorem chainValue_singleton (p : E × E) (z : E) :
    chainValue [p] z = inner ℝ p.2 (z - p.1) :=
  rfl

/-- Concatenating a nonempty second chain at `q` splits the value at the join. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:47published source at 0e31a3cda412

- Concatenating a nonempty second chain at `q` splits the value at the join.

theorem chainValue_append_cons :
    ∀ (l₁ : List (E × E)) (q : E × E) (l₂ : List (E × E)) (z : E),
      chainValue (l₁ ++ q :: l₂) z =
        chainValue l₁ q.1 + chainValue (q :: l₂) z
  | [], q, l₂, z => by simp [chainValue]
  | [p], q, l₂, z => by simp [chainValue]
  | p :: r :: l₁, q, l₂, z => by
      rw [show (p :: r :: l₁) ++ q :: l₂ = p :: ((r :: l₁) ++ q :: l₂) by rfl]
      simp only [chainValue]
      rw [chainValue_append_cons (r :: l₁) q l₂ z]
      rw [chainValue_append_cons [p] q [] q.1]
      simp [chainValue, add_assoc]

/-- Membership of an element in a list gives a prefix/suffix decomposition. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:52published source at 0e31a3cda412

- Membership of an element in a list gives a prefix/suffix decomposition.

theorem exists_split_of_mem {α : Type*} {a : α} :
    ∀ {l : List α}, a ∈ l → ∃ s t : List α, l = s ++ a :: t
  | [], h => by simp at h
  | b :: l, h => by
      rw [List.mem_cons] at h
      rcases h with h | h
      · subst b
        exact ⟨[], l, rfl⟩
      · rcases exists_split_of_mem h with ⟨s, t, rfl⟩
        exact ⟨b :: s, t, by simp⟩

/-- A duplicated element gives two explicit occurrences with an intermediate loop. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:66published source at 0e31a3cda412

- A duplicated element gives two explicit occurrences with an intermediate loop.

theorem exists_duplicate_split {α : Type*} {a : α} :
    ∀ {l : List α}, List.Duplicate a l →
      ∃ s t u : List α, l = s ++ a :: t ++ a :: u
  | _, List.Duplicate.cons_mem h => by
      rcases exists_split_of_mem h with ⟨t, u, rfl⟩
      exact ⟨[], t, u, by simp⟩
  | _, @List.Duplicate.cons_duplicate _ a b l h => by
      rcases exists_duplicate_split h with ⟨s, t, u, rfl⟩
      exact ⟨b :: s, t, u, by simp [List.append_assoc]⟩

/-- Removing the segment between two identical pair points decomposes the
original affine chain value into the shortened outer chain plus the closed
inner loop. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:78published source at 0e31a3cda412

- Removing the segment between two identical pair points decomposes the original affine chain value into the shortened outer chain plus the closed inner loop.

theorem chainValue_duplicate_split
    (s t u : List (E × E)) (a : E × E) (z : E) :
    chainValue (s ++ a :: t ++ a :: u) z =
      chainValue (s ++ a :: u) z + chainValue (a :: t) a.1 := by
  rw [show s ++ a :: t ++ a :: u = s ++ a :: (t ++ a :: u) by
    simp [List.append_assoc]]
  rw [chainValue_append_cons s a (t ++ a :: u) z]
  change chainValue s a.1 + chainValue ((a :: t) ++ a :: u) z =
    chainValue (s ++ a :: u) z + chainValue (a :: t) a.1
  rw [chainValue_append_cons (a :: t) a u z]
  rw [chainValue_append_cons s a u z]
  ring

end

end PairingClosedChain
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean:91published source at 0e31a3cda412