feat: introduce a predicate DependsOn

Mathlib.lean

@@ -3829,6 +3829,7 @@ import Mathlib.Logic.Function.Coequalizer
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Logic.Function.Conjugate
 import Mathlib.Logic.Function.Defs
+import Mathlib.Logic.Function.DependsOn
 import Mathlib.Logic.Function.FiberPartition
 import Mathlib.Logic.Function.FromTypes
 import Mathlib.Logic.Function.Iterate

Mathlib/Data/Finset/Pi.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import Mathlib.Data.Finset.Card
 import Mathlib.Data.Finset.Union
 import Mathlib.Data.Multiset.Pi
+import Mathlib.Logic.Function.DependsOn
 
 /-!
 # The cartesian product of finsets
@@ -179,6 +180,9 @@ theorem restrict₂_comp_restrict {s t : Finset ι} (hst : s ⊆ t) :
 theorem restrict₂_comp_restrict₂ {s t u : Finset ι} (hst : s ⊆ t) (htu : t ⊆ u) :
     (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu) := rfl
 
+lemma dependsOn_restrict (s : Finset ι) : DependsOn (s.restrict (π := π)) s :=
+  (s : Set ι).dependsOn_restrict
+
 end Pi
 
 end Finset

Mathlib/Data/Finset/Update.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Mathlib.Data.Finset.Basic
+import Mathlib.Logic.Function.DependsOn
 
 /-!
 # Update a function on a set of values
@@ -49,6 +50,23 @@ theorem update_eq_updateFinset {i y} :
     exact uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y
   · simp [hj, updateFinset]
 
+/-- If one replaces the variables indexed by a finite set `t`, then `f` no longer depends on
+those variables. -/
+theorem _root_.DependsOn.updateFinset {α : Type*} {f : (Π i, π i) → α} {s : Set ι}
+    (hf : DependsOn f s) {t : Finset ι} (y : Π i : t, π i) :
+    DependsOn (fun x ↦ f (updateFinset x t y)) (s \ t) := by
+  refine fun x₁ x₂ h ↦ hf (fun i hi ↦ ?_)
+  simp only [Function.updateFinset]
+  split_ifs; · rfl
+  simp_all
+
+/-- If one replaces the variable indexed by `i`, then `f` no longer depends on
+this variable. -/
+theorem _root_.DependsOn.update {α : Type*} {f : (Π i, π i) → α} {s : Finset ι} (hf : DependsOn f s)
+    (i : ι) (y : π i) : DependsOn (fun x ↦ f (Function.update x i y)) (s.erase i) := by
+  simp_rw [Function.update_eq_updateFinset, erase_eq, coe_sdiff]
+  exact hf.updateFinset _
+
 theorem updateFinset_updateFinset {s t : Finset ι} (hst : Disjoint s t)
     {y : ∀ i : ↥s, π i} {z : ∀ i : ↥t, π i} :
     updateFinset (updateFinset x s y) t z =

Mathlib/Logic/Function/DependsOn.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2024 Etienne Marion. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Etienne Marion
+-/
+import Mathlib.Data.Set.Function
+
+/-!
+# 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 call some function constant with respect to
+some variables and be able to infer this when applying transformations mentioned above.
+This is why 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`.
+
+## Tags
+
+depends on
+-/
+
+open Set
+
+variable {ι : Type*} {α : ι → Type*} {β : Type*}
+
+/-- A function `f` depends on `s` if, whenever `x` and `y` coincide over `s`, `f x = f y`. -/
+def DependsOn (f : (Π i, α i) → β) (s : Set ι) : Prop :=
+  ∀ ⦃x y⦄, (∀ i ∈ s, x i = y i) → f x = f y
+
+lemma dependsOn_iff_factorsThrough {f : (Π i, α i) → β} {s : Set ι} :
+    DependsOn f s ↔ Function.FactorsThrough f s.restrict := by
+  rw [DependsOn, Function.FactorsThrough]
+  simp [funext_iff]
+
+lemma dependsOn_univ (f : (Π i, α i) → β) : DependsOn f univ :=
+  fun _ _ h ↦ congrArg _ <| funext fun i ↦ h i trivial
+
+variable {f : (Π i, α i) → β}
+
+/-- A constant function does not depend on any variable. -/
+lemma dependsOn_const (b : β) : DependsOn (fun _ : Π i, α i ↦ b) ∅ := by simp [DependsOn]
+
+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)
+
+/-- 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)
+
+lemma Set.dependsOn_restrict (s : Set ι) : DependsOn (s.restrict (π := α)) s :=
+  fun _ _ h ↦ funext fun i ↦ h i.1 i.2

Mathlib/Order/Restriction.lean

@@ -52,6 +52,9 @@ theorem restrictLe₂_comp_restrictLe {a b : α} (hab : a ≤ b) :
 theorem restrictLe₂_comp_restrictLe₂ {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
     (restrictLe₂ (π := π) hab) ∘ (restrictLe₂ hbc) = restrictLe₂ (hab.trans hbc) := rfl
 
+lemma dependsOn_restrictLe (a : α) : DependsOn (restrictLe (π := π) a) (Iic a) :=
+  (Iic a).dependsOn_restrict
+
 end Set
 
 section Finset
@@ -68,7 +71,7 @@ lemma frestrictLe_apply (a : α) (f : (a : α) → π a) (i : Iic a) : frestrict
 
 /-- If a function `f` indexed by `α` is restricted to elements `≤ b`, and `a ≤ b`,
 this is the restriction to elements `≤ b`. Intervals are seen as finite sets. -/
-def frestrictLe₂ {a b : α} (hab : a ≤ b) := Finset.restrict₂ (π := π) (Iic_subset_Iic.2 hab)
+def frestrictLe₂ {a b : α} (hab : a ≤ b) := restrict₂ (π := π) (Iic_subset_Iic.2 hab)
 
 @[simp]
 lemma frestrictLe₂_apply {a b : α} (hab : a ≤ b) (f : (i : Iic b) → π i) (i : Iic a) :
@@ -80,6 +83,9 @@ theorem frestrictLe₂_comp_frestrictLe {a b : α} (hab : a ≤ b) :
 theorem frestrictLe₂_comp_frestrictLe₂ {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
     (frestrictLe₂ (π := π) hab) ∘ (frestrictLe₂ hbc) = frestrictLe₂ (hab.trans hbc) := rfl
 
+lemma dependsOn_frestrictLe (a : α) : DependsOn (frestrictLe (π := π) a) (Set.Iic a) :=
+  coe_Iic a ▸ (Finset.Iic a).dependsOn_restrict
+
 end Finset
 
 end Preorder