theorem indicator_one_wInner_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (s : Finset ι) (f : ι → 𝕜) : ⟪(↑s).indicator fun (x : ι) => 1, f⟫_[𝕜] = ∑ i ∈ s, f i

theorem wInner_one_indicator_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (f : ι → 𝕜) (s : Finset ι) : ⟪f, (↑s).indicator fun (x : ι) => 1⟫_[𝕜] = ∑ i ∈ s, (starRingEnd 𝕜) (f i)

theorem mu_wInner_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (s : Finset ι) (f : ι → 𝕜) : ⟪mu s, f⟫_[𝕜] = s.expect fun (i : ι) => f i

theorem wInner_one_mu {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (f : ι → 𝕜) (s : Finset ι) : ⟪f, mu s⟫_[𝕜] = s.expect fun (i : ι) => (starRingEnd 𝕜) (f i)