Normalised indicator

noncomputable def mu {K : Type u_1} {α : Type u_3} [DivisionSemiring K] (s : Finset α) : α → K

The normalised indicator_one of a set.

Equations

• mu s = (↑s.card)⁻¹ • (↑s).indicator fun (x : α) => 1

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

@[simp]

theorem mu_empty {K : Type u_1} {α : Type u_3} [DivisionSemiring K] : mu ∅ = 0

theorem map_mu {K : Type u_1} {L : Type u_2} {α : Type u_3} [DivisionSemiring K] [DivisionSemiring L] (f : K →+* L) (s : Finset α) (x : α) : f (mu s x) = mu s x

theorem mu_univ_eq_const {K : Type u_1} {α : Type u_3} [DivisionSemiring K] [Fintype α] : mu Finset.univ = Function.const α (↑(Fintype.card α))⁻¹

@[simp]

theorem mu_apply_eq_zero {K : Type u_1} {α : Type u_3} [DivisionSemiring K] {s : Finset α} [CharZero K] {a : α} : mu s a = 0 ↔ a ∉ s

theorem mu_apply_ne_zero {K : Type u_1} {α : Type u_3} [DivisionSemiring K] {s : Finset α} [CharZero K] {a : α} : mu s a ≠ 0 ↔ a ∈ s

@[simp]

theorem mu_eq_zero {K : Type u_1} {α : Type u_3} [DivisionSemiring K] {s : Finset α} [CharZero K] : mu s = 0 ↔ s = ∅

theorem mu_ne_zero {K : Type u_1} {α : Type u_3} [DivisionSemiring K] {s : Finset α} [CharZero K] : mu s ≠ 0 ↔ s.Nonempty

@[simp]

theorem support_mu (K : Type u_1) {α : Type u_3} [DivisionSemiring K] [CharZero K] (s : Finset α) : Function.support (mu s) = ↑s

theorem card_smul_mu (K : Type u_1) {α : Type u_3} [DivisionSemiring K] [CharZero K] (s : Finset α) : s.card • mu s = (↑s).indicator fun (x : α) => 1

theorem card_smul_mu_apply (K : Type u_1) {α : Type u_3} [DivisionSemiring K] [CharZero K] (s : Finset α) (x : α) : s.card • mu s x = (↑s).indicator (fun (x : α) => 1) x

@[simp]

theorem sum_mu (K : Type u_1) {α : Type u_3} [DivisionSemiring K] {s : Finset α} [CharZero K] [Fintype α] (hs : s.Nonempty) : ∑ x : α, mu s x = 1

@[simp]

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

@[simp]

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

@[simp]

theorem mu_inv (K : Type u_1) {α : Type u_3} [DivisionSemiring K] [Group α] [DecidableEq α] (s : Finset α) (a : α) : mu s⁻¹ a = mu s a⁻¹

@[simp]

theorem mu_neg (K : Type u_1) {α : Type u_3} [DivisionSemiring K] [AddGroup α] [DecidableEq α] (s : Finset α) (a : α) : mu (-s) a = mu s (-a)

theorem translate_mu (K : Type u_1) {G : Type u_4} [DivisionSemiring K] [AddCommGroup G] [DecidableEq G] (a : G) (s : Finset G) : translate a (mu s) = mu (a +ᵥ s)

theorem expect_mu (K : Type u_1) {G : Type u_4} [Semifield K] {s : Finset G} [CharZero K] [Fintype G] (hs : s.Nonempty) : (Finset.univ.expect fun (x : G) => mu s x) = (↑(Fintype.card G))⁻¹

@[simp]

theorem conjneg_mu (K : Type u_1) {G : Type u_4} [Semifield K] [StarRing K] [AddCommGroup G] [DecidableEq G] (s : Finset G) : conjneg (mu s) = mu (-s)

@[simp]

theorem conj_mu_apply (K : Type u_1) {α : Type u_3} [Semifield K] [StarRing K] (s : Finset α) (a : α) : (starRingEnd K) (mu s a) = mu s a

@[simp]

theorem conj_mu (K : Type u_1) {α : Type u_3} [Semifield K] [StarRing K] (s : Finset α) : (starRingEnd (α → K)) (mu s) = mu s

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of mu_pos.

@[simp]

theorem Complex.ofReal_mu {α : Type u_3} (s : Finset α) (a : α) : ↑(mu s a) = mu s a

@[simp]

theorem Complex.ofReal_comp_mu {α : Type u_3} (s : Finset α) : ofReal ∘ mu s = mu s

@[simp]

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

@[simp]

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

@[simp]

theorem NNReal.coe_mu {α : Type u_3} (s : Finset α) (x : α) : ↑(mu s x) = mu s x

@[simp]

theorem NNReal.coe_comp_mu {α : Type u_3} (s : Finset α) : toReal ∘ mu s = mu s