Indicator

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

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} {β : Type u_3} [DecidableEq α] [Semiring β] {s : Finset α} (x : α) : 𝟭 s x = if x ∈ s then 1 else 0

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

theorem indicate_eq_zero {α : Type u_2} {β : Type u_3} [DecidableEq α] [Semiring β] {s : Finset α} [Nontrivial β] {a : α} : 𝟭 s a = 0 ↔ a ∉ s

theorem indicate_ne_zero {α : Type u_2} {β : Type u_3} [DecidableEq α] [Semiring β] {s : Finset α} [Nontrivial β] {a : α} : 𝟭 s a ≠ 0 ↔ a ∈ s

@[simp]

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

theorem sum_indicate {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semiring β] [Fintype α] (s : Finset α) : (Finset.univ.sum fun (x : α) => 𝟭 s x) = ↑s.card

theorem card_eq_sum_indicate {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) : s.card = Finset.univ.sum fun (x : α) => 𝟭 s x

theorem translate_indicate {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semiring β] [AddCommGroup α] (a : α) (s : Finset α) : τ a (𝟭 s) = 𝟭 (a +ᵥ s)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem indicate_isSelfAdjoint {α : Type u_2} {β : Type u_3} [DecidableEq α] [Semiring β] [StarRing β] (s : Finset α) : IsSelfAdjoint (𝟭 s)

theorem indicate_inf_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [CommSemiring β] [Fintype α] (s : Finset ι) (t : ι → Finset α) (x : α) : 𝟭 (s.inf t) x = s.prod fun (i : ι) => 𝟭 (t i) x

theorem indicate_inf {ι : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [CommSemiring β] [Fintype α] (s : Finset ι) (t : ι → Finset α) : 𝟭 (s.inf t) = s.prod fun (i : ι) => 𝟭 (t i)

@[simp]

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

@[simp]

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

@[simp]

theorem conjneg_indicate {α : Type u_2} {β : Type u_3} [DecidableEq α] [CommSemiring β] [StarRing β] [AddCommGroup α] (s : Finset α) : conjneg (𝟭 s) = 𝟭 (-s)

theorem expect_indicate {ι : Type u_1} {β : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring β] [Module ℚ≥0 β] (s : Finset ι) : (Finset.univ.expect fun (x : ι) => 𝟭 s x) = (↑(Fintype.card ι))⁻¹ • ↑s.card

@[simp]

theorem NNReal.coe_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) (x : α) : ↑(𝟭 s x) = 𝟭 s x

@[simp]

theorem NNReal.coe_comp_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) : NNReal.toReal ∘ 𝟭 s = 𝟭 s

@[simp]

theorem Complex.ofReal_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) (x : α) : ↑(𝟭 s x) = 𝟭 s x

@[simp]

theorem Complex.ofReal_comp_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) : Complex.ofReal' ∘ 𝟭 s = 𝟭 s

@[simp]

theorem indicate_nonneg {α : Type u_2} {β : Type u_3} [DecidableEq α] [OrderedSemiring β] {s : Finset α} : 0 ≤ 𝟭 s

@[simp]

theorem indicate_pos {α : Type u_2} {β : Type u_3} [DecidableEq α] [OrderedSemiring β] {s : Finset α} [Nontrivial β] : 0 < 𝟭 s ↔ s.Nonempty

theorem Finset.Nonempty.indicate_pos {α : Type u_2} {β : Type u_3} [DecidableEq α] [OrderedSemiring β] {s : Finset α} [Nontrivial β] : s.Nonempty → 0 < 𝟭 s

Alias of the reverse direction of indicate_pos.

Normalised indicator

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

The normalised indicate of a set.

Equations

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

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 mu_apply {α : Type u_2} {β : Type u_3} [DecidableEq α] [DivisionSemiring β] {s : Finset α} (x : α) : μ s x = (↑s.card)⁻¹ * if x ∈ s then 1 else 0

@[simp]

theorem mu_empty {α : Type u_2} {β : Type u_3} [DecidableEq α] [DivisionSemiring β] : μ ∅ = 0

theorem map_mu {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] [DivisionSemiring β] [DivisionSemiring γ] (f : β →+* γ) (s : Finset α) (x : α) : f (μ s x) = μ s x

@[simp]

theorem mu_apply_eq_zero {α : Type u_2} {β : Type u_3} [DecidableEq α] [DivisionSemiring β] {s : Finset α} [CharZero β] {a : α} : μ s a = 0 ↔ a ∉ s

theorem mu_apply_ne_zero {α : Type u_2} {β : Type u_3} [DecidableEq α] [DivisionSemiring β] {s : Finset α} [CharZero β] {a : α} : μ s a ≠ 0 ↔ a ∈ s

@[simp]

theorem mu_eq_zero {α : Type u_2} {β : Type u_3} [DecidableEq α] [DivisionSemiring β] {s : Finset α} [CharZero β] : μ s = 0 ↔ s = ∅

theorem mu_ne_zero {α : Type u_2} {β : Type u_3} [DecidableEq α] [DivisionSemiring β] {s : Finset α} [CharZero β] : μ s ≠ 0 ↔ s.Nonempty

@[simp]

theorem support_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [CharZero β] (s : Finset α) : Function.support (μ s) = ↑s

theorem card_smul_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [CharZero β] (s : Finset α) : s.card • μ s = 𝟭 s

theorem card_smul_mu_apply {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [CharZero β] (s : Finset α) (x : α) : s.card • μ s x = 𝟭 s x

theorem sum_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] {s : Finset α} [CharZero β] [Fintype α] (hs : s.Nonempty) : (Finset.univ.sum fun (x : α) => μ s x) = 1

theorem translate_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [AddCommGroup α] (a : α) (s : Finset α) : τ a (μ s) = μ (a +ᵥ s)

@[simp]

theorem mu_vadd {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] {G : Type u_5} [AddGroup G] [AddAction G α] (g : G) (s : Finset α) (a : α) : μ (g +ᵥ s) a = μ s (-g +ᵥ a)

@[simp]

theorem mu_smul {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] {G : Type u_5} [Group G] [MulAction G α] (g : G) (s : Finset α) (a : α) : μ (g • s) a = μ s (g⁻¹ • a)

@[simp]

theorem mu_neg {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [AddGroup α] (s : Finset α) (a : α) : μ (-s) a = μ s (-a)

@[simp]

theorem mu_inv {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [Group α] (s : Finset α) (a : α) : μ s⁻¹ a = μ s a⁻¹

theorem expect_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semifield β] {s : Finset α} [CharZero β] [Fintype α] (hs : s.Nonempty) : (Finset.univ.expect fun (x : α) => μ s x) = (↑(Fintype.card α))⁻¹

@[simp]

theorem conj_mu_apply {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semifield β] [StarRing β] [AddCommGroup α] (s : Finset α) (a : α) : (starRingEnd β) (μ s a) = μ s a

@[simp]

theorem conj_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semifield β] [StarRing β] [AddCommGroup α] (s : Finset α) : (starRingEnd (α → β)) (μ s) = μ s

@[simp]

theorem conjneg_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semifield β] [StarRing β] [AddCommGroup α] (s : Finset α) : conjneg (μ s) = μ (-s)

@[simp]

theorem RCLike.coe_mu {α : Type u_2} [DecidableEq α] {𝕜 : Type u_5} [RCLike 𝕜] (s : Finset α) (a : α) : ↑(μ s a) = μ s a

@[simp]

theorem RCLike.coe_comp_mu {α : Type u_2} [DecidableEq α] {𝕜 : Type u_5} [RCLike 𝕜] (s : Finset α) : RCLike.ofReal ∘ μ s = μ s

@[simp]

theorem NNReal.coe_mu {α : Type u_2} [DecidableEq α] (s : Finset α) (x : α) : ↑(μ s x) = μ s x

@[simp]

theorem NNReal.coe_comp_mu {α : Type u_2} [DecidableEq α] (s : Finset α) : NNReal.toReal ∘ μ s = μ s

@[simp]

theorem mu_nonneg {α : Type u_2} {β : Type u_3} [DecidableEq α] [LinearOrderedSemifield β] {s : Finset α} : 0 ≤ μ s

@[simp]

theorem mu_pos {α : Type u_2} {β : Type u_3} [DecidableEq α] [LinearOrderedSemifield β] {s : Finset α} : 0 < μ s ↔ s.Nonempty

theorem Finset.Nonempty.mu_pos {α : Type u_2} {β : Type u_3} [DecidableEq α] [LinearOrderedSemifield β] {s : Finset α} : s.Nonempty → 0 < μ s

Alias of the reverse direction of mu_pos.