How best to express my applied maths problem in mathlib?

Stream: Is there code for X?

[Alistair Tucker]

Hi everyone. I am hoping to prove something about a problem I have concerning financial contagion (more prosaically interbank debt valuation). In particular I would like to prove that given my set-up a solution exists and is unique. I have managed to convince myself that it's true but the argument is pretty messy. What I'd like to ask is whether there is some mathlib theory currently unknown to me in which it could all be expressed (and resolved) more nicely. Or if not, what such a theory might look like.

For example, in my initial attempts I have expressed continuity of a function using definitions from topology.basic. But it looks as if there are other ways to posit a continuous function in mathlib (or even a function which, like this one, solves a PDE). Perhaps one of them might be more appropriate? I'll post some code now.

[Alistair Tucker]

The set of banks I call β. Goings-on in the real economy are communicated as a path in 'asset space' X. Various chunks of debt may have various maturities τ up to some final time T. Given ψ specifying the set of surviving banks as a function of asset space, we construct the full solution using induction and the PDE-solving operator ℋ.

import topology.instances.real

@[derive decidable_eq] inductive β |BARC |HSBC |LLOY |NATW |RBSG |SANT |STDCH

def X : Type := β → ℝ
instance : has_add X := by { dunfold X, apply_instance, }
instance : has_coe ℝ X := ⟨λ r i, r⟩
noncomputable instance : topological_space X := by { dunfold X, apply_instance, }

def Tt (T : with_top ℝ) : set ℝ := {t : ℝ | 0 ≤ t ∧ (t : with_top ℝ) < T}
def Tτ {T : with_top ℝ} (t : Tt T) : set ℝ := {τ : ℝ | t.1 < τ ∧ (τ : with_top ℝ) ≤ T}

def debt_fn (T : with_top ℝ) : Type* := Π (t : Tt T), X → β → Tτ t → ℝ

open pfun

variable {T : with_top ℝ}
variable ℋ : (Π t : Tt T, X →. Tτ t → ℝ) → (Π t : Tt T, X → Tτ t → ℝ)

def v_mk (b : finset β) (ψb : Tt T → X → finset β) (v : Π c < b, debt_fn T) : debt_fn T :=
λ t y i, ite (i ∈ b) (ℋ (λ s x, ⟨ψb s x < b, (λ h, v (ψb s x) h s x i)⟩) t y) 0

def v (ψ : finset β → Tt T → X → finset β) : finset β → debt_fn T :=
λ a, finset.strong_induction_on a (λ b v, v_mk ℋ b (ψ b) v)

[Alistair Tucker]

These are the properties of ℋ that I believe to be relevant. The first argument v' to ℋ communicates boundary conditions. In fact I have defined it not only at the boundary but over the whole of the complement of the PDE's domain. I also make use of an 'equity valuation function' E^* taking the set of debt valuations as an argument. The idea is that where one of its components falls below zero a bank will have failed.

class well_behaved_soln : Prop :=
(matches_on_complement (v' : Π t, X →. Tτ t → ℝ) : ∀ t y h, ℋ v' t y = fn (v' t) y h)
(positivity_preserving (v' : Π t, X →. Tτ t → ℝ) : (∀ t y h, 0 ≤ fn (v' t) y h) → 0 ≤ ℋ v')
(continuity_preserving (v' : Π t, X →. Tτ t → ℝ) : ∀ t, pcontinuous (v' t) → continuous (ℋ v' t))
(translation_invariant (v' : Π t, X →. Tτ t → ℝ) (o : β → ℝ) :
  ∀ t y, ℋ v' t (y + o) = ℋ (λ s x, ⟨x + o ∈ dom (v' s), (λ h, fn (v' s) (x + o) h)⟩) t y)
(compatible_on_subsets (v' : Π t, X →. Tτ t → ℝ) (V : Tt T → set X) (hs : ∀ t, V t ⊆ -dom (v' t)) :
  ∀ t y, ℋ v' t y = ℋ (λ s x, ⟨x ∉ V s, (λ h, ℋ v' s x)⟩) t y)
(mono_wrt_val_on_compl (v₁ v₂ : Π t, X →. Tτ t → ℝ) (hd : ∀ t y, y ∈ dom (v₁ t) ↔ y ∈ dom (v₂ t)) :
  (∀ t y (h : y ∈ dom (v₁ t)), fn (v₁ t) y h ≤ fn (v₂ t) y ((hd t y).1 h)) → ℋ v₁ ≤ ℋ v₂)

variable [well_behaved_soln ℋ]

variable ℰ (t : Tt T) (y : X) (υ : β → Tτ t → ℝ) : β → ℝ
def E_star (v : debt_fn T) (t : Tt T) (y : X) : β → ℝ := ℰ t y (v t y)

def mono_wrt_assets (u : debt_fn T) : Prop :=
∀ (r : ℝ) (hr : 0 ≤ r) (t : Tt T) (y : X), u t y ≤ u t (y + r)

def strict_mono_wrt_assets (E : Tt T → X → β → ℝ) : Prop :=
∀ (r : ℝ) (hr : 0 < r) (t : Tt T) (y : X), E t y < E t (y + r)

class equity_function : Prop :=
(mono_wrt_debt_valuation {t : Tt T} {y : X} {υ₁ υ₂ : β → Tτ t → ℝ} : υ₁ ≤ υ₂ → ℰ t y υ₁ ≤ ℰ t y υ₂)
(preserves_mono_wrt_assets {u : debt_fn T} : mono_wrt_assets u → strict_mono_wrt_assets (E_star ℰ u))

variable [equity_function ℰ]

[Alistair Tucker]

Now this is what I want to prove: the existence and uniqueness of a 'survivors' function φ having the following properties.

def V (ψ : finset β → Tt T → X → finset β) (a : finset β) : Tt T → set X :=
λ t y, ψ a t y = a

class surviving_set (ψ : finset β → Tt T → X → finset β) : Prop :=
(only_fail : ∀ a t y, ψ a t y ≤ a)
(idempotent : ∀ a t y, y ∈ V ψ (ψ a t y) t)
(maximal : ∀ a t y, ∀ b ≤ a, ψ a t y < b → y ∉ V ψ b t)
(consistent : ∀ a t y, y ∈ V ψ a t ↔ ∀ i ∈ a, 0 < E_star ℰ (v ℋ ψ a) t y i)
(supported : ∀ a t y, (∃ b < a, ∀ i ∈ a, 0 < E_star ℰ (v ℋ ψ b) t y i) → y ∈ V ψ a t)
  -- I'm not fond of this last condition. Perhaps I can lose it or replace it.

theorem exists_unique_soln : ∃! ψ, surviving_set ℋ ℰ ψ :=
sorry

[Alistair Tucker]

oops I also need

class equity_function : Prop :=
...
(continuity_preserving (υ : debt_fn T) : ∀ t, continuous (υ t) → continuous (E_star ℰ υ t))