Mathlib.Logic.Function.DependsOn

Module docstring

{"# 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 "}

DependsOn definition

(f : (Π i, α i) → β) (s : Set ι) : Prop

Full source

/-- 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`. -/
def DependsOn (f : (Π i, α i) → β) (s : Set ι) : Prop :=
  ∀ ⦃x y⦄, (∀ i ∈ s, x i = y i) → f x = f y

Dependence of a function on a set of variables

Informal description

A function $ f : (\Pi i, \alpha_i) \to \beta $ is said to *depend on* a set $ s \subseteq \iota $ if for any two inputs $ x $ and $ y $ that agree on $ s $ (i.e., $ x_i = y_i $ for all $ i \in s $), the outputs $ f(x) $ and $ f(y) $ are equal. This means $ f $'s value is determined only by the values of its arguments in $ s $, though it may not actually depend on all (or any) variables in $ s $ (e.g., if $ f $ is constant).

dependsOn_iff_factorsThrough theorem

{f : (Π i, α i) → β} {s : Set ι} : DependsOn f s ↔ FactorsThrough f s.restrict

Full source

lemma dependsOn_iff_factorsThrough {f : (Π i, α i) → β} {s : Set ι} :
    DependsOnDependsOn f s ↔ FactorsThrough f s.restrict := by
  rw [DependsOn, FactorsThrough]
  simp [funext_iff]

Equivalence of Dependence and Factorization Through Restriction

Informal description

For a function $ f : (\Pi i, \alpha_i) \to \beta $ and a set $ s \subseteq \iota $, the following are equivalent: 1. $ f $ depends on $ s $ (i.e., $ f(x) = f(y) $ whenever $ x $ and $ y $ agree on $ s $), 2. $ f $ factors through the restriction map $ s.\text{restrict} : (\Pi i, \alpha_i) \to (\Pi i \in s, \alpha_i) $.

dependsOn_iff_exists_comp theorem

 [Nonempty β] {f : (Π i, α i) → β} {s : Set ι} : DependsOn f s ↔ ∃ g : (Π i : s, α i) → β, f = g ∘ s.restrict

Full source

lemma dependsOn_iff_exists_comp [Nonempty β] {f : (Π i, α i) → β} {s : Set ι} :
    DependsOnDependsOn f s ↔ ∃ g : (Π i : s, α i) → β, f = g ∘ s.restrict := by
  rw [dependsOn_iff_factorsThrough, factorsThrough_iff]

Characterization of Dependence via Composition with Restriction

Informal description

For a nonempty type $\beta$ and a function $f : (\Pi i, \alpha_i) \to \beta$, the following are equivalent: 1. $f$ depends on a set $s \subseteq \iota$ (i.e., $f(x) = f(y)$ whenever $x_i = y_i$ for all $i \in s$), 2. There exists a function $g : (\Pi i \in s, \alpha_i) \to \beta$ such that $f = g \circ \text{restrict}_s$, where $\text{restrict}_s$ is the restriction map to $s$.

dependsOn_univ theorem

(f : (Π i, α i) → β) : DependsOn f univ

Full source

lemma dependsOn_univ (f : (Π i, α i) → β) : DependsOn f univ :=
  fun _ _ h ↦ congrArg _ <| funext fun i ↦ h i trivial

Any Function Depends on the Entire Domain

Informal description

For any function $ f : (\Pi i, \alpha_i) \to \beta $, $ f $ depends on the entire index set $ \iota $ (i.e., $ \text{DependsOn } f \text{ univ} $ holds). This means that if two inputs agree on all variables (since $ \text{univ} = \iota $), then their outputs under $ f $ must be equal.

dependsOn_const theorem

(b : β) : DependsOn (fun _ : Π i, α i ↦ b) ∅

Full source

/-- A constant function does not depend on any variable. -/
lemma dependsOn_const (b : β) : DependsOn (fun _ : Π i, α i ↦ b) ∅ := by simp [DependsOn]

Constant Function Depends on Empty Set of Variables

Informal description

For any constant function $f : (\Pi i, \alpha_i) \to \beta$ defined by $f(x) = b$ for some fixed $b \in \beta$ and all $x \in \Pi i, \alpha_i$, the function $f$ depends on the empty set of variables. That is, $\text{DependsOn}(f, \emptyset)$ holds.

DependsOn.mono theorem

{s t : Set ι} (hst : s ⊆ t) (hf : DependsOn f s) : DependsOn f t

Full source

lemma DependsOn.mono {s t : Set ι} (hst : s ⊆ t) (hf : DependsOn f s) : DependsOn f t :=
  fun _ _ h ↦ hf fun i hi ↦ h i (hst hi)

Monotonicity of Dependence: If $f$ Depends on $s$ and $s \subseteq t$, then $f$ Depends on $t$

Informal description

Let $f : (\Pi i, \alpha_i) \to \beta$ be a function and $s, t \subseteq \iota$ be sets of indices. If $f$ depends only on variables in $s$ (i.e., $\text{DependsOn}(f, s)$ holds) and $s \subseteq t$, then $f$ also depends only on variables in $t$ (i.e., $\text{DependsOn}(f, t)$ holds).

DependsOn.empty theorem

(hf : DependsOn f ∅) (x y : Π i, α i) : f x = f y

Full source

/-- A function which depends on the empty set is constant. -/
lemma DependsOn.empty (hf : DependsOn f ∅) (x y : Π i, α i) : f x = f y := hf (by simp)

Functions Depending on No Variables Are Constant

Informal description

If a function $f : (\Pi i, \alpha_i) \to \beta$ depends on the empty set of variables (i.e., $\text{DependsOn}(f, \emptyset)$ holds), then $f$ is constant. That is, for any two inputs $x$ and $y$ in $\Pi i, \alpha_i$, we have $f(x) = f(y)$.

Set.dependsOn_restrict theorem

(s : Set ι) : DependsOn (s.restrict (π := α)) s

Full source

lemma Set.dependsOn_restrict (s : Set ι) : DependsOn (s.restrict (π := α)) s :=
  fun _ _ h ↦ funext fun i ↦ h i.1 i.2

Restriction Function Depends Only on Its Domain

Informal description

For any set $s \subseteq \iota$, the restriction function $s.\text{restrict} : (\Pi i, \alpha_i) \to (\Pi i \in s, \alpha_i)$ depends only on the variables in $s$. That is, if two inputs $x$ and $y$ agree on $s$, then their restrictions $s.\text{restrict}(x)$ and $s.\text{restrict}(y)$ are equal.