# 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

source
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

Instances For

source
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
source
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
source
theorem dependsOn_univ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (f : ((i : ι) → α i) → β) :
DependsOn f Set.univ
source
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.

source
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
source
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.

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