4.1.1. Relations🔗

The analysis of input-output systems usually involves chaining multiple systems together in a feedback loop. While all practical application the feedback connection is again a well-defined input-output map, this is not necessarily the case in general. It would be possible to always assume that the feedback connection is well-defined, but this means that artificial looking assumptions have to be carried around for proofs that do not require them. To avoid talking about well-definedness, instead of using input-output maps, we use relations.

A relation is simply a subset of the cartesian product of two sets.

SetRel.{u_6, u_7} (α : Type u_6) (β : Type u_7) : Type (max u_7 u_6)
SetRel.{u_6, u_7} (α : Type u_6)
  (β : Type u_7) : Type (max u_7 u_6)

Every function defines a relation via its graph Function.graph.

4.1.2. Unbundled functions🔗

There are different ways of writing L^p functions in mathlib. The space of L^p functions is given by MeasureTheory.Lp and consists of all equivalence classes of functions together with the property that their L^p norm is finite. Proving theorems with equivalence classes can be rather tedious, because all equalities only hold almost everywhere and one has to use filter_upwards to prove equalities such as (f + g) x = f x + g x.

To circumvent these issues, we use functions directly and also we do not bundle in the property that we are dealing with (local) L^p functions, but rather assume these properties separately. So a nonlinear operator is just a map f : (α → E) → (α → F) and implicitly we use junk values for f u in the case that u : α → E is not a local L^p function.