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 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 then used to prove some properties about lmarginals.

Main definitions

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

Main statements

• dependsOn_lmarginal: If a function f depends on a set s and t is a finite set, then ∫⋯∫⁻_t, f ∂μ depends on s \ t.
• lmarginal_eq_of_disjoint: If a function f depends on a set s and t is a finite set disjoint from s and the measures μ i are probability measures, then ∫⋯∫⁻_t, f ∂μ is equal to f.

Tags

depends on, updateFinset, update, lmarginal

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.

Equations

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

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_empty {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} (hf : DependsOn f ∅) (x : (i : ι) → α i) (y : (i : ι) → α i) : f x = f y

A function which depends on the empty set is constant.

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

theorem Preorder.dependsOn_frestrictLe {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] (i : ι) : DependsOn (Preorder.frestrictLe i) (Set.Iic i)

theorem dependsOn_updateFinset {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} [DecidableEq ι] {s : Set ι} (hf : DependsOn f s) (t : Finset ι) (y : (i : { x : ι // x ∈ t }) → α ↑i) : DependsOn (fun (x : (i : ι) → α i) => f (Function.updateFinset x t y)) (s \ ↑t)

If one replaces the variables indexed by a finite set t, then f no longer depends on these variables.

theorem dependsOn_update {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} [DecidableEq ι] {s : Finset ι} (hf : DependsOn f ↑s) (i : ι) (y : α i) : DependsOn (fun (x : (i : ι) → α i) => f (Function.update x i y)) ↑(s.erase i)

If one replaces the variable indexed by i, then f no longer depends on this variable.

theorem dependsOn_lmarginal {ι : Type u_1} [DecidableEq ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.Measure (X i)} {f : ((i : ι) → X i) → ENNReal} {s : Set ι} (hf : DependsOn f s) (t : Finset ι) : DependsOn (∫⋯∫⁻_t, f ∂μ) (s \ ↑t)

If a function depends on s, then its lmarginal with respect to a finite set t only depends on s \ t.

theorem lmarginal_eq_of_disjoint {ι : Type u_1} [DecidableEq ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.Measure (X i)} {f : ((i : ι) → X i) → ENNReal} {s : Set ι} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (hf : DependsOn f s) {t : Finset ι} (hst : Disjoint s ↑t) : ∫⋯∫⁻_t, f ∂μ = f

If μ is a family of probability measures, and f depends on s, then integrating over some variables which are not in s does not change the value.

theorem lmarginal_const {ι : Type u_1} [DecidableEq ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.Measure (X i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} (c : ENNReal) (x : (i : ι) → X i) : (∫⋯∫⁻_s, fun (x : (i : ι) → X i) => c ∂μ) x = c

Integrating a constant over some variables with respect to probability measures does nothing.

theorem lmarginal_eq_of_disjoint_diff {ι : Type u_1} [DecidableEq ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.Measure (X i)} {f : ((i : ι) → X i) → ENNReal} {s : Set ι} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (mf : Measurable f) (hf : DependsOn f s) {t : Finset ι} {u : Finset ι} (htu : t ⊆ u) (hsut : Disjoint s (↑u \ ↑t)) : ∫⋯∫⁻_u, f ∂μ = ∫⋯∫⁻_t, f ∂μ

If μ is a family of probability measures, and f depends on s, then integrating over two different sets of variables such that their difference is not in s yields the same function.

theorem lmarginal_eq_of_disjoint_symmDiff {ι : Type u_1} [DecidableEq ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.Measure (X i)} {f : ((i : ι) → X i) → ENNReal} {s : Set ι} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (mf : Measurable f) (hf : DependsOn f s) {t : Finset ι} {u : Finset ι} (hstu : Disjoint s (symmDiff ↑t ↑u)) : ∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_u, f ∂μ

If μ is a family of probability measures, and f depends on s, then integrating over two different sets of variables such that their difference is not in s yields the same function.