Update a function on a set of values

This file defines Function.updateFinset, the operation that updates a function on a (finite) set of values.

This is a very specific function used for MeasureTheory.marginal, and possibly not that useful for other purposes.

def Function.updateFinset {ι : Type u_1} {π : ι → Sort u_2} [DecidableEq ι] (x : (i : ι) → π i) (s : Finset ι) (y : (i : { x : ι // x ∈ s }) → π ↑i) (i : ι) : π i

updateFinset x s y is the vector x with the coordinates in s changed to the values of y.

Equations

• Function.updateFinset x s y i = if hi : i ∈ s then y ⟨i, hi⟩ else x i

theorem Function.updateFinset_def {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {s : Finset ι} {y : (i : { x : ι // x ∈ s }) → π ↑i} : updateFinset x s y = fun (i : ι) => if hi : i ∈ s then y ⟨i, hi⟩ else x i

@[simp]

theorem Function.updateFinset_empty {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {y : (i : { x : ι // x ∈ ∅ }) → π ↑i} : updateFinset x ∅ y = x

theorem Function.updateFinset_singleton {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {i : ι} {y : (i_1 : { x : ι // x ∈ {i} }) → π ↑i_1} : updateFinset x {i} y = update x i (y ⟨i, ⋯⟩)

theorem Function.update_eq_updateFinset {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {i : ι} {y : π i} : update x i y = updateFinset x {i} (uniqueElim y)

theorem DependsOn.updateFinset {ι : Type u_2} {π : ι → Type u_3} [DecidableEq ι] {α : Type u_1} {f : ((i : ι) → π i) → α} {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 those variables.

theorem DependsOn.update {ι : Type u_2} {π : ι → Type u_3} [DecidableEq ι] {α : Type u_1} {f : ((i : ι) → π i) → α} {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 Function.updateFinset_updateFinset {ι : Type u_1} {π : ι → Type u_2} {x : (i : ι) → π i} [DecidableEq ι] {s t : Finset ι} (hst : Disjoint s t) {y : (i : { x : ι // x ∈ s }) → π ↑i} {z : (i : { x : ι // x ∈ t }) → π ↑i} : updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((Equiv.piFinsetUnion π hst) (y, z))

theorem Function.updateFinset_updateFinset_of_subset {ι : Type u_1} {π : ι → Sort u_2} [DecidableEq ι] {s t : Finset ι} (hst : s ⊆ t) (x : (i : ι) → π i) (y : (i : { x : ι // x ∈ s }) → π ↑i) (z : (i : { x : ι // x ∈ t }) → π ↑i) : updateFinset (updateFinset x s y) t z = updateFinset x t z

theorem Function.restrict_updateFinset_of_subset {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {s t : Finset ι} (hst : s ⊆ t) (x : (i : ι) → π i) (y : (i : { x : ι // x ∈ t }) → π ↑i) : s.restrict (updateFinset x t y) = Finset.restrict₂ hst y

theorem Function.restrict_updateFinset {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {s : Finset ι} (x : (i : ι) → π i) (y : (i : { x : ι // x ∈ s }) → π ↑i) : s.restrict (updateFinset x s y) = y

@[simp]

theorem Function.updateFinset_restrict {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {s : Finset ι} (x : (i : ι) → π i) : updateFinset x s (s.restrict x) = x