Functions depending only on some variables

When dealing with a function f : Π i, α i depending on many variables, some operations may get rid of the dependency on some variables (see Function.updateFinset or MeasureTheory.lmarginal for example). However considering this new function as having a different domain with fewer points is not comfortable in Lean, as it requires the use of subtypes and can lead to tedious writing.

On the other hand one wants to be able for example to describe some function as constant with respect to some variables, and be able to deduce this when applying transformations mentioned above. This is why we introduce the predicate DependsOn f s, which states that if x and y coincide over the set s, then f x = f y. This is equivalent to Function.FactorsThrough f s.restrict.

Main definition

• DependsOn f s: If x and y coincide over the set s, then f x equals f y.

Main statement

• dependsOn_iff_factorsThrough: A function f depends on s if and only if it factors through s.restrict.

Implementation notes

When we write DependsOn f s, i.e. f only depends on s, it should be interpreted as "f potentially depends only on variables in s". However it might be the case that f does not depend at all on variables in s, for example if f is constant. As a consequence, DependsOn f univ is always true, see dependsOn_univ.

The predicate DependsOn f s can also be interpreted as saying that f is independent of all the variables which are not in s. Although this phrasing might seem more natural, we choose to go with DependsOn because writing mathematically "independent of variables in s" would boil down to ∀ x y, (∀ i ∉ s, x i = y i) → f x = f y, which is the same as DependsOn f sᶜ.

Tags

depends on

def DependsOn {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (f : ((i : ι) → α i) → β) (s : Set ι) : Prop

A function f depends on s if, whenever x and y coincide over s, f x = f y.

It should be interpreted as "f potentially depends only on variables in s". However it might be the case that f does not depend at all on variables in s, for example if f is constant. As a consequence, DependsOn f univ is always true, see dependsOn_univ.

Equations

• DependsOn f s = ∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y

theorem dependsOn_iff_factorsThrough {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {s : Set ι} : DependsOn f s ↔ Function.FactorsThrough f s.restrict

theorem dependsOn_iff_exists_comp {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [Nonempty β] {f : ((i : ι) → α i) → β} {s : Set ι} : DependsOn f s ↔ ∃ (g : ((i : ↑s) → α ↑i) → β), f = g ∘ s.restrict

theorem dependsOn_univ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (f : ((i : ι) → α i) → β) : DependsOn f Set.univ

theorem dependsOn_const {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (b : β) : DependsOn (fun (x : (i : ι) → α i) => b) ∅

A constant function does not depend on any variable.

theorem DependsOn.mono {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {s t : Set ι} (hst : s ⊆ t) (hf : DependsOn f s) : DependsOn f t

theorem DependsOn.empty {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} (hf : DependsOn f ∅) (x y : (i : ι) → α i) : f x = f y

A function which depends on the empty set is constant.

theorem Set.dependsOn_restrict {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) : DependsOn s.restrict s