MaxLeafFormal.RSCStages

Source file MaxLeafFormal/RSCStages.lean of the Lean project (how it is built).

Statements of the paper formalised here: Proposition D.5.23.

import MaxLeafFormal.RSCCert

/-!
# Stages for (C5)

The definition of stages in the proof of `prop:rsc-cert` (with "nonnegative rational" from its statement),
and the fact that stages give (C5) at their start point, from `C5_of_stages`. No data is used.
-/

namespace MaxLeafFormal.RSCCert
open MaxLeafFormal.Antinorm8 (Kpos PZ)
open Pointwise

/-- Stages for (C5): `Ys = [Y₁, …, Y_{j-1}]` are finite sets of
nonnegative rational points such that, with `Y₀ = {P}` and `Y_j = Z`, every `x ∘ z` with
`x ∈ Y_{i-1}` and `z ∈ Z` lies in `conv(Y_i) + 𝒦_pos`, for `1 ≤ i ≤ j = Ys.length + 1`. -/
def IsStages (p₂ p₃ : ℝ) (Z : Finset (Fin 8 → ℝ)) (P : Fin 8 → ℝ)
    (Ys : List (Finset (Fin 8 → ℝ))) : Prop :=
  (∀ Y ∈ Ys, ∀ x ∈ Y, 0 ≤ x ∧ ∀ s, ∃ r : ℚ, x s = (r : ℝ)) ∧
  ∀ i, 1 ≤ i → i ≤ Ys.length + 1 →
    ∀ x ∈ (({P} : Finset (Fin 8 → ℝ)) :: Ys).getD (i - 1) ∅, ∀ z ∈ Z,
      merge p₂ p₃ x z ∈ convexHull ℝ (((Ys ++ [Z]).getD (i - 1) ∅ : Finset (Fin 8 → ℝ)) :
        Set (Fin 8 → ℝ)) + Kpos

/-- Stages give (C5) at their start point, with chains of length `Ys.length + 1`. -/
theorem isStages_C5 {p₂ p₃ : ℝ} (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1)
    {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) {P : Fin 8 → ℝ} (hP : 0 ≤ P)
    {Ys : List (Finset (Fin 8 → ℝ))} (h : IsStages p₂ p₃ Z P Ys) :
    ∀ Qs : List (Fin 8 → ℝ), Qs.length = Ys.length + 1 → (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
      Qs.foldl (merge p₂ p₃) P ∈ PZ Z := by
  intro Qs hQs hQ
  have key1 : ∀ i, i < Ys.length + 1 →
      ((({P} : Finset (Fin 8 → ℝ)) :: Ys) ++ [Z]).getD i ∅ =
        (({P} : Finset (Fin 8 → ℝ)) :: Ys).getD i ∅ := by
    intro i hi
    rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD,
      List.getElem?_append_left (by simpa using hi)]
  have key2 : ∀ i, ((({P} : Finset (Fin 8 → ℝ)) :: Ys) ++ [Z]).getD (i + 1) ∅ =
      (Ys ++ [Z]).getD i ∅ := by
    intro i
    rw [List.cons_append, List.getD_cons_succ]
  refine C5_of_stages hp hZ0 P hP (Ys.length + 1)
    (fun i => ((({P} : Finset (Fin 8 → ℝ)) :: Ys) ++ [Z]).getD i ∅) ?_ ?_ ?_ ?_ Qs hQs hQ
  · simp
  · show ((({P} : Finset (Fin 8 → ℝ)) :: Ys) ++ [Z]).getD (Ys.length + 1) ∅ = Z
    rw [key2, List.getD_eq_getElem?_getD, List.getElem?_append_right le_rfl]
    simp
  · intro i hi x hx
    have hx' : x ∈ (({P} : Finset (Fin 8 → ℝ)) :: Ys).getD i ∅ := by
      rw [← key1 i hi]; exact hx
    rcases i with _ | k
    · have : x = P := by simpa using hx'
      rw [this]; exact hP
    · have hk : k < Ys.length := by omega
      rw [List.getD_cons_succ, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hk,
        Option.getD_some] at hx'
      exact (h.1 _ (List.getElem_mem hk) x hx').1
  · intro i hi1 hij x hx z hz
    obtain ⟨k, rfl⟩ : ∃ k, i = k + 1 := ⟨i - 1, by omega⟩
    have hx' : x ∈ (({P} : Finset (Fin 8 → ℝ)) :: Ys).getD k ∅ := by
      have e := key1 k (by omega)
      simp only [Nat.add_sub_cancel] at hx
      rw [← e]; exact hx
    show merge p₂ p₃ x z ∈ convexHull ℝ
      (((({P} : Finset (Fin 8 → ℝ)) :: Ys) ++ [Z]).getD (k + 1) ∅ : Set (Fin 8 → ℝ)) + Kpos
    rw [key2]
    have h2 := h.2 (k + 1) (by omega) hij
    simp only [Nat.add_sub_cancel] at h2
    exact h2 x hx' z hz

end MaxLeafFormal.RSCCert
Back to top