appendix-c.lean

import data.set.finite
import topology.instances.real

open set

def is_maximal {α : Type*} [partial_order α] (s : set α) (b : α) : Prop :=
∃ (h : b ∈ s), ∀ b' ∈ s, b ≤ b' → b = b'

lemma exists_maximal {α : Type*} [partial_order α] (s : set α) (hs : finite s) :
  ∀ a ∈ s, ∃ b (h : a ≤ b), is_maximal s b :=
begin
  intros a has,
  let t : set α := {a' ∈ s | a ≤ a'},
  suffices h' : ∃ (b : α) (hbt : b ∈ t), ∀ (b' : α), b' ∈ t → b ≤ b' → b = b',
  { rcases h' with ⟨b, hbt, hb⟩,
    refine ⟨b, hbt.2, hbt.1, _⟩,
    intros b' hb' hbb',
    exact hb b' ⟨hb', le_trans hbt.2 hbb'⟩ hbb', },
  apply finite.exists_maximal_wrt id t,
  { exact finite_subset hs (inter_subset_left s {a' | a ≤ a'}), },
  { exact ne_empty_of_mem ⟨has, le_refl a⟩, },
end

section

def bb : finset string := {"BARC", "HSBC", "LLOY", "NATW", "RBSG", "SANT", "STDCH"}
def β : Type := {b : string // b ∈ bb}
instance : fintype β := finset.subtype.fintype bb

parameter T : ℝ   -- final time.
def α : Type := (β → Ioi (0 : ℝ)) × (Ico 0 T)

parameter E_star (v : α → β → ℝ) : α → β → ℝ
parameter is_mono_E_star {v v' : α → β → ℝ} {x : α} : v x ≤ v' x → E_star v x ≤ E_star v' x

parameter {V (s : set β) : set α}
parameter {u (s : set β) : α → β → ℝ}

parameter cond_V_s_iff (s : set β) (x : α) : x ∈ V s ↔ ∀ i ∈ s, 0 < E_star (u s) x i

parameter cond_fallback (s s' : set β) (x : α) : is_maximal {s' ∈ 𝒫 s | x ∈ V s'} s' → u s x = u s' x

def U (s : finset β) : set α :=
λ x : α, if s = ∅ then true else ∃ r ⊂ s, ∀ i ∈ s, 0 < E_star (u ↑r) x i

lemma U_def (s : finset β) (x : α) :
  x ∈ U s = if s = ∅ then true else ∃ r ⊂ s, ∀ i ∈ s, 0 < E_star (u ↑r) x i :=
rfl

def h_ind_ii (s : set β) : Prop := ∀ r ⊂ s, ∀ r' ⊆ r, u r' ≤ u r

lemma exists_maximal' (S : set (set β)) : ∀ r ∈ S, ∃ s' (h : r ≤ s'), is_maximal S s' :=
exists_maximal S (finite.of_fintype S)

include is_mono_E_star cond_V_s_iff cond_fallback

lemma L2 [fintype β] (s : finset β) (hs : h_ind_ii ↑s) : U s ⊆ V ↑s :=
begin
  rw ←compl_subset_compl,
  intros x hx,
  have hx' := mt (iff.mpr (cond_V_s_iff ↑s x)) hx,
  push_neg at hx',
  rcases hx' with ⟨i, hi, hE⟩,
  have hne : s ≠ ∅,
  { intro he,
    rw [he, finset.coe_empty] at hi,
    exact hi, },
  rw [mem_compl_eq, U_def, if_neg hne],
  push_neg,
  intros r hr,
  refine ⟨i, hi, _⟩,
  suffices h : u ↑r x ≤ u ↑s x,
  { exact le_trans (is_mono_E_star h i) hE, },
  have h : ∃ (r' : set β) (h : ∅ ⊆ r'), is_maximal {r' ∈ 𝒫 ↑r | x ∈ V r'} r',
  { apply exists_maximal',
    exact ⟨empty_subset ↑r, iff.mpr (cond_V_s_iff ∅ x) (λ i h, false.elim h)⟩, },
  rcases h with ⟨r', he, hmr'⟩,
  rw cond_fallback ↑r r' x hmr',
  have h : ∃ (s' : set β) (h : r' ⊆ s'), is_maximal {s' ∈ 𝒫 ↑s | x ∈ V s'} s',
  { apply exists_maximal',
    cases hmr' with h₁ h₂,
    apply and.intro,
    { exact subset.trans (and.left h₁) (and.left hr), },
    { exact and.right h₁, }, },
  rcases h with ⟨s', hr', hms'⟩,
  rw cond_fallback ↑s s' x hms',
  suffices hs' : s' ⊂ ↑s,
  { exact hs s' hs' r' hr' x, },
  cases hms' with h₁ h₂,
  apply and.intro (and.left h₁),
  exact λ hss', hx (hss' ▸ and.right h₁),
end

end