Documentation

Mathlib.Data.Finset.Update

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.

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

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

Equations
Instances For
    source
    theorem Function.updateFinset_def {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {s : Finset ι} {y : (i : ↥s) → π ↑i} :
    updateFinset x s y = fun (i : ι) => if hi : i ∈ s then y ⟨i, hi⟩ else x i
    source
    @[simp]
    theorem Function.updateFinset_empty {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {y : (i : ↥∅) → π ↑i} :
    updateFinset x ∅ y = x
    source
    theorem Function.updateFinset_singleton {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {i : ι} {y : (i_1 : ↥{i}) → π ↑i_1} :
    updateFinset x {i} y = update x i (y ⟨i, ⋯⟩)
    source
    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)
    source
    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 : ↥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.

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

    source
    theorem Function.updateFinset_updateFinset {ι : Type u_1} {π : ι → Type u_2} {x : (i : ι) → π i} [DecidableEq ι] {s t : Finset ι} {y : (i : ↥s) → π ↑i} {z : (i : ↥t) → π ↑i} (hst : Disjoint s t) :
    updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((Equiv.piFinsetUnion π hst) (y, z))
    source
    theorem Function.updateFinset_updateFinset_of_subset {ι : Type u_1} {π : ι → Sort u_2} [DecidableEq ι] {s t : Finset ι} (hst : s ⊆ t) (x : (i : ι) → π i) (y : (i : ↥s) → π ↑i) (z : (i : ↥t) → π ↑i) :
    updateFinset (updateFinset x s y) t z = updateFinset x t z
    source
    theorem Function.restrict_updateFinset_of_subset {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {s t : Finset ι} (hst : s ⊆ t) (x : (i : ι) → π i) (y : (i : ↥t) → π ↑i) :
    s.restrict (updateFinset x t y) = Finset.restrict₂ hst y
    source
    theorem Function.restrict_updateFinset {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {s : Finset ι} (x : (i : ι) → π i) (y : (i : ↥s) → π ↑i) :
    s.restrict (updateFinset x s y) = y
    source
    @[simp]
    theorem Function.updateFinset_restrict {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {s : Finset ι} (x : (i : ι) → π i) :
    updateFinset x s (s.restrict x) = x
    source
    theorem Function.update_updateFinset {ι : Type u_1} {π : ι → Type u_2} {x : (i : ι) → π i} [DecidableEq ι] {s : Finset ι} {y : (i : ↥s) → π ↑i} {i : ι} {z : π i} (hi : i ∉ s) :
    update (updateFinset x s y) i z = updateFinset x (s ∪ {i}) ((Equiv.piFinsetUnion π ⋯) (y, uniqueElim z))
    source
    theorem Function.updateFinset_congr {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {s t : Finset ι} {y : (i : ↥s) → π ↑i} {z : (i : ↥t) → π ↑i} (h : s = t) :
    updateFinset x s y = updateFinset x t fun (i : ↥t) => y ⟨↑i, ⋯⟩
    source
    theorem Function.updateFinset_univ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] [Fintype ι] {y : (i : ↥Finset.univ) → π ↑i} :
    updateFinset x Finset.univ y = fun (i : ι) => y ⟨i, ⋯⟩
    source
    theorem Function.updateFinset_univ_apply {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] [Fintype ι] {y : (i : ↥Finset.univ) → π ↑i} {i : ι} :
    updateFinset x Finset.univ y i = y ⟨i, ⋯⟩