Indicator of intersection

Stream: Is there code for X?

[Vincent Beffara]

Do we have these?

lemma set.indicator_inter {α β : Type*} [has_zero β] {s t : set α} {f : α → β} :
  (s ∩ t).indicator f = s.indicator (t.indicator f) :=
begin
  classical,
  ext,
  simp only [set.indicator],
  convert ite_and (x ∈ s) (x ∈ t) (f x) 0
end

lemma set.indicator_inter_one {α : Type*} {s t : set α} :
  (s ∩ t).indicator (1 : α → ℝ) = s.indicator 1 * t.indicator 1 :=
begin
  ext,
  rw set.indicator_inter,
  simp only [set.indicator, pi.one_apply, pi.mul_apply, boole_mul]
end

[Vincent Beffara]

(The second one is not at the right level of generality, but the first one feels natural enough.)

[Eric Wieser]

Does the first exist as docs#set.indicator_indicator? (Edit: yes)

[Eric Wieser]

Is the second one generally s.indicator f * t.indicator g = (s ∩ t).indicator (f * g) in any monoid_with_zero?

[Vincent Beffara]

Eric Wieser said:

Does the first exist as docs#set.indicator_indicator? (Edit: yes)

Ah thanks! I was looking for indicator_inter or variations around that, but did not think about the other way.

[Vincent Beffara]

The more general version that you mention for the second one is certainly worth having, but the specialization with 1 is also useful in itself (typically for probability).