Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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) :
as, ∃ 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 ↔ ∀ is, 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 elsers, ∀ is, 0 < E_star (u ↑r) x i
lemma U_def (s : finset β) (x : α) :
x ∈ U s = if s = ∅ then true elsers, ∀ is, 0 < E_star (u ↑r) x i :=
rfl
def h_ind_ii (s : set β) : Prop := ∀ rs, ∀ r'r, u r' ≤ u r
lemma exists_maximal' (S : set (set β)) : ∀ rS, ∃ 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment