Indicator

def indicate {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] (s : Finset α) (a : α) : R

Equations

• 𝟭 s a = if a ∈ s then 1 else 0

def «term𝟭» : Lean.ParserDescr

Equations

• «term𝟭» = Lean.ParserDescr.node `«term𝟭» 1024 (Lean.ParserDescr.symbol "𝟭 ")

def «term𝟭_[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem indicate_apply {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] {s : Finset α} (x : α) : 𝟭 s x = if x ∈ s then 1 else 0

@[simp]

theorem indicate_empty {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] : 𝟭 ∅ = 0

@[simp]

theorem indicate_univ {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] [Fintype α] : 𝟭 Finset.univ = 1

theorem indicate_inter_apply {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] (s t : Finset α) (x : α) : 𝟭 (s ∩ t) x = 𝟭 s x * 𝟭 t x

theorem indicate_inter {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] (s t : Finset α) : 𝟭 (s ∩ t) = 𝟭 s * 𝟭 t

theorem map_indicate {α : Type u_2} {R : Type u_4} {S : Type u_5} [DecidableEq α] [Semiring R] [Semiring S] (f : R →+* S) (s : Finset α) (x : α) : f (𝟭 s x) = 𝟭 s x

@[simp]

theorem indicate_image {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] {α' : Type u_6} [DecidableEq α'] (e : α ≃ α') (s : Finset α) (a : α') : 𝟭 (Finset.image (⇑e) s) a = 𝟭 s (e.symm a)

@[simp]

theorem indicate_apply_eq_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] {s : Finset α} [Nontrivial R] {a : α} : 𝟭 s a = 0 ↔ a ∉ s

theorem indicate_apply_ne_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] {s : Finset α} [Nontrivial R] {a : α} : 𝟭 s a ≠ 0 ↔ a ∈ s

@[simp]

theorem indicate_eq_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] {s : Finset α} [Nontrivial R] : 𝟭 s = 0 ↔ s = ∅

theorem indicate_ne_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] {s : Finset α} [Nontrivial R] : 𝟭 s ≠ 0 ↔ s.Nonempty

@[simp]

theorem support_indicate {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] {s : Finset α} [Nontrivial R] : Function.support (𝟭 s) = ↑s

theorem sum_indicate {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] [Fintype α] (s : Finset α) : ∑ x : α, 𝟭 s x = ↑s.card

theorem card_eq_sum_indicate {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) : s.card = ∑ x : α, 𝟭 s x

@[simp]

theorem indicate_vadd {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] {G : Type u_6} [AddGroup G] [AddAction G α] (g : G) (s : Finset α) (a : α) : 𝟭 (g +ᵥ s) a = 𝟭 s (-g +ᵥ a)

@[simp]

theorem indicate_smul {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] {G : Type u_6} [Group G] [MulAction G α] (g : G) (s : Finset α) (a : α) : 𝟭 (g • s) a = 𝟭 s (g⁻¹ • a)

@[simp]

theorem indicate_neg {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] [AddGroup α] (s : Finset α) (a : α) : 𝟭 (-s) a = 𝟭 s (-a)

@[simp]

theorem indicate_inv {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semiring R] [Group α] (s : Finset α) (a : α) : 𝟭 s⁻¹ a = 𝟭 s a⁻¹

theorem indicate_inf_apply {ι : Type u_1} {α : Type u_2} {R : Type u_4} [DecidableEq α] [CommSemiring R] [Fintype α] (s : Finset ι) (t : ι → Finset α) (x : α) : 𝟭 (s.inf t) x = ∏ i ∈ s, 𝟭 (t i) x

theorem indicate_inf {ι : Type u_1} {α : Type u_2} {R : Type u_4} [DecidableEq α] [CommSemiring R] [Fintype α] (s : Finset ι) (t : ι → Finset α) : 𝟭 (s.inf t) = ∏ i ∈ s, 𝟭 (t i)

@[simp]

theorem conj_indicate_apply {α : Type u_2} {R : Type u_4} [DecidableEq α] [CommSemiring R] [StarRing R] (s : Finset α) (a : α) : (starRingEnd R) (𝟭 s a) = 𝟭 s a

@[simp]

theorem conj_indicate {α : Type u_2} {R : Type u_4} [DecidableEq α] [CommSemiring R] [StarRing R] (s : Finset α) : (starRingEnd (α → R)) (𝟭 s) = 𝟭 s

@[simp]

theorem indicate_nonneg {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset α} : 0 ≤ 𝟭 s

@[simp]

theorem indicate_apply_nonneg {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset α} {a : α} : 0 ≤ 𝟭 s a

@[simp]

theorem indicate_pos {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset α} [Nontrivial R] : 0 < 𝟭 s ↔ s.Nonempty

theorem Finset.Nonempty.indicate_pos {α : Type u_2} {R : Type u_4} [DecidableEq α] [Semiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset α} [Nontrivial R] : s.Nonempty → 0 < 𝟭 s

Alias of the reverse direction of indicate_pos.

Normalised indicator

def mu {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] (s : Finset α) : α → R

The normalised indicate of a set.

Equations

• mu s = (↑s.card)⁻¹ • 𝟭 s

def mu.termμ : Lean.ParserDescr

Equations

• mu.termμ = Lean.ParserDescr.node `mu.termμ 1024 (Lean.ParserDescr.symbol "μ ")

def mu.«termμ_[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem mu_apply {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] {s : Finset α} (x : α) : mu s x = (↑s.card)⁻¹ * if x ∈ s then 1 else 0

@[simp]

theorem mu_empty {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] : mu ∅ = 0

theorem map_mu {α : Type u_2} {R : Type u_4} {S : Type u_5} [DecidableEq α] [DivisionSemiring R] [DivisionSemiring S] (f : R →+* S) (s : Finset α) (x : α) : f (mu s x) = mu s x

theorem mu_univ_eq_const {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] [Fintype α] : mu Finset.univ = Function.const α (↑(Fintype.card α))⁻¹

@[simp]

theorem mu_apply_eq_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] {s : Finset α} [CharZero R] {a : α} : mu s a = 0 ↔ a ∉ s

theorem mu_apply_ne_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] {s : Finset α} [CharZero R] {a : α} : mu s a ≠ 0 ↔ a ∈ s

@[simp]

theorem mu_eq_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] {s : Finset α} [CharZero R] : mu s = 0 ↔ s = ∅

theorem mu_ne_zero {α : Type u_2} {R : Type u_4} [DecidableEq α] [DivisionSemiring R] {s : Finset α} [CharZero R] : mu s ≠ 0 ↔ s.Nonempty

@[simp]

theorem support_mu {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] [CharZero R] (s : Finset α) : Function.support (mu s) = ↑s

theorem card_smul_mu {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] [CharZero R] (s : Finset α) : s.card • mu s = 𝟭 s

theorem card_smul_mu_apply {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] [CharZero R] (s : Finset α) (x : α) : s.card • mu s x = 𝟭 s x

@[simp]

theorem sum_mu {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] {s : Finset α} [CharZero R] [Fintype α] (hs : s.Nonempty) : ∑ x : α, mu s x = 1

@[simp]

theorem mu_vadd {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] {G : Type u_6} [AddGroup G] [AddAction G α] (g : G) (s : Finset α) (a : α) : mu (g +ᵥ s) a = mu s (-g +ᵥ a)

@[simp]

theorem mu_smul {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] {G : Type u_6} [Group G] [MulAction G α] (g : G) (s : Finset α) (a : α) : mu (g • s) a = mu s (g⁻¹ • a)

@[simp]

theorem mu_neg {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] [AddGroup α] (s : Finset α) (a : α) : mu (-s) a = mu s (-a)

@[simp]

theorem mu_inv {α : Type u_2} (R : Type u_4) [DecidableEq α] [DivisionSemiring R] [Group α] (s : Finset α) (a : α) : mu s⁻¹ a = mu s a⁻¹

@[simp]

theorem conj_mu_apply {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semifield R] [StarRing R] (s : Finset α) (a : α) : (starRingEnd R) (mu s a) = mu s a

@[simp]

theorem conj_mu {α : Type u_2} (R : Type u_4) [DecidableEq α] [Semifield R] [StarRing R] (s : Finset α) : (starRingEnd (α → R)) (mu s) = mu s

@[simp]

theorem mu_nonneg {α : Type u_2} {K : Type u_3} [DecidableEq α] [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {s : Finset α} : 0 ≤ mu s

@[simp]

theorem mu_pos {α : Type u_2} {K : Type u_3} [DecidableEq α] [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {s : Finset α} : 0 < mu s ↔ s.Nonempty

theorem Finset.Nonempty.mu_pos {α : Type u_2} {K : Type u_3} [DecidableEq α] [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {s : Finset α} : s.Nonempty → 0 < mu s

Alias of the reverse direction of mu_pos.