import algebra.support

open_locale big_operators

open function

variables {α β ι M N : Type*}

namespace set

section has_one

variables [has_one M] [has_one N] {s t : set α} {f g : α → M} {a : α}

noncomputable def indicator {M} [has_zero M] (s : set α) (f : α → M) : α → M

| x := by haveI := classical.dec_pred (∈ s); exact if x ∈ s then f x else 0

noncomputable def mul_indicator (s : set α) (f : α → M) : α → M

| x := by haveI := classical.dec_pred (∈ s); exact if x ∈ s then f x else 1

@[simp, to_additive] lemma piecewise_eq_mul_indicator [decidable_pred (∈ s)] :

s.piecewise f 1 = s.mul_indicator f :=

funext $ λ x, @if_congr _ _ _ _ (id _) _ _ _ _ iff.rfl rfl rfl

@[to_additive] lemma mul_indicator_apply (s : set α) (f : α → M) (a : α) [decidable (a ∈ s)] :

mul_indicator s f a = if a ∈ s then f a else 1 := by convert rfl

@[simp, to_additive] lemma mul_indicator_of_mem (h : a ∈ s) (f : α → M) :

mul_indicator s f a = f a :=

by { letI := classical.dec (a ∈ s), exact if_pos h }

@[simp, to_additive] lemma mul_indicator_of_not_mem (h : a ∉ s) (f : α → M) :

mul_indicator s f a = 1 :=

by { letI := classical.dec (a ∈ s), exact if_neg h }

@[to_additive] lemma mul_indicator_eq_one_or_self (s : set α) (f : α → M) (a : α) :

mul_indicator s f a = 1 ∨ mul_indicator s f a = f a :=

by_cases h : a ∈ s,

{ exact or.inr (mul_indicator_of_mem h f) },

{ exact or.inl (mul_indicator_of_not_mem h f) }

@[simp, to_additive] lemma mul_indicator_apply_eq_self :

s.mul_indicator f a = f a ↔ (a ∉ s → f a = 1) :=

by letI := classical.dec (a ∈ s); exact ite_eq_left_iff.trans (by rw [@eq_comm _ (f a)])

@[simp, to_additive] lemma mul_indicator_eq_self : s.mul_indicator f = f ↔ mul_support f ⊆ s :=

by simp only [funext_iff, subset_def, mem_mul_support, mul_indicator_apply_eq_self, not_imp_comm]

@[to_additive] lemma mul_indicator_eq_self_of_superset (h1 : s.mul_indicator f = f) (h2 : s ⊆ t) :

t.mul_indicator f = f :=

by { rw mul_indicator_eq_self at h1 ⊢, exact subset.trans h1 h2 }

@[simp, to_additive] lemma mul_indicator_apply_eq_one :

mul_indicator s f a = 1 ↔ (a ∈ s → f a = 1) :=

by letI := classical.dec (a ∈ s); exact ite_eq_right_iff

@[simp, to_additive] lemma mul_indicator_eq_one :

mul_indicator s f = (λ x, 1) ↔ disjoint (mul_support f) s :=

by simp only [funext_iff, mul_indicator_apply_eq_one, set.disjoint_left, mem_mul_support,

not_imp_not]

@[simp, to_additive] lemma mul_indicator_eq_one' :

mul_indicator s f = 1 ↔ disjoint (mul_support f) s :=

mul_indicator_eq_one

@[to_additive] lemma mul_indicator_apply_ne_one {a : α} :

s.mul_indicator f a ≠ 1 ↔ a ∈ s ∩ mul_support f :=

by simp only [ne.def, mul_indicator_apply_eq_one, not_imp, mem_inter_iff, mem_mul_support]

@[simp, to_additive] lemma mul_support_mul_indicator :

function.mul_support (s.mul_indicator f) = s ∩ function.mul_support f :=

ext $ λ x, by simp [function.mem_mul_support, mul_indicator_apply_eq_one]

lemma mem_of_mul_indicator_ne_one (h : mul_indicator s f a ≠ 1) : a ∈ s :=

not_imp_comm.1 (λ hn, mul_indicator_of_not_mem hn f) h

@[to_additive] lemma eq_on_mul_indicator : eq_on (mul_indicator s f) f s :=

λ x hx, mul_indicator_of_mem hx f

@[to_additive] lemma mul_support_mul_indicator_subset : mul_support (s.mul_indicator f) ⊆ s :=

λ x hx, hx.imp_symm (λ h, mul_indicator_of_not_mem h f)

@[simp, to_additive] lemma mul_indicator_mul_support : mul_indicator (mul_support f) f = f :=

mul_indicator_eq_self.2 subset.rfl

@[simp, to_additive] lemma mul_indicator_range_comp {ι : Sort*} (f : ι → α) (g : α → M) :

mul_indicator (range f) g ∘ f = g ∘ f :=

by letI := classical.dec_pred (∈ range f); exact piecewise_range_comp _ _ _

@[to_additive] lemma mul_indicator_congr (h : eq_on f g s) :

mul_indicator s f = mul_indicator s g :=

funext $ λx, by { simp only [mul_indicator], split_ifs, { exact h h_1 }, refl }

@[simp, to_additive] lemma mul_indicator_univ (f : α → M) : mul_indicator (univ : set α) f = f :=

mul_indicator_eq_self.2 $ subset_univ _

@[simp, to_additive] lemma mul_indicator_empty (f : α → M) : mul_indicator (∅ : set α) f = λa, 1 :=

mul_indicator_eq_one.2 $ disjoint_empty _

@[to_additive] lemma mul_indicator_empty' (f : α → M) : mul_indicator (∅ : set α) f = 1 :=

mul_indicator_empty f

variable (M)

@[simp, to_additive] lemma mul_indicator_one (s : set α) :

mul_indicator s (λx, (1:M)) = λx, (1:M) :=

mul_indicator_eq_one.2 $ by simp only [mul_support_one, empty_disjoint]

@[simp, to_additive] lemma mul_indicator_one' {s : set α} : s.mul_indicator (1 : α → M) = 1 :=

mul_indicator_one M s

variable {M}

@[to_additive] lemma mul_indicator_mul_indicator (s t : set α) (f : α → M) :

mul_indicator s (mul_indicator t f) = mul_indicator (s ∩ t) f :=

funext $ λx, by { simp only [mul_indicator], split_ifs, repeat {simp * at * {contextual := tt}} }

@[simp, to_additive] lemma mul_indicator_inter_mul_support (s : set α) (f : α → M) :

mul_indicator (s ∩ mul_support f) f = mul_indicator s f :=

by rw [← mul_indicator_mul_indicator, mul_indicator_mul_support]

@[to_additive] lemma comp_mul_indicator (h : M → β) (f : α → M) {s : set α} {x : α}

[decidable_pred (∈ s)] :

h (s.mul_indicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x :=

by letI := classical.dec_pred (∈ s); convert s.apply_piecewise f (const α 1) (λ _, h)

@[to_additive] lemma mul_indicator_comp_right {s : set α} (f : β → α) {g : α → M} {x : β} :

mul_indicator (f ⁻¹' s) (g ∘ f) x = mul_indicator s g (f x) :=

by { simp only [mul_indicator], split_ifs; refl }

@[to_additive] lemma mul_indicator_image {s : set α} {f : β → M} {g : α → β} (hg : injective g)

{x : α} : mul_indicator (g '' s) f (g x) = mul_indicator s (f ∘ g) x :=

by rw [← mul_indicator_comp_right, preimage_image_eq _ hg]

@[to_additive] lemma mul_indicator_comp_of_one {g : M → N} (hg : g 1 = 1) :

mul_indicator s (g ∘ f) = g ∘ (mul_indicator s f) :=

funext,

simp only [mul_indicator],

split_ifs; simp [*]

@[to_additive] lemma comp_mul_indicator_const (c : M) (f : M → N) (hf : f 1 = 1) :

(λ x, f (s.mul_indicator (λ x, c) x)) = s.mul_indicator (λ x, f c) :=

(mul_indicator_comp_of_one hf).symm

@[to_additive] lemma mul_indicator_preimage (s : set α) (f : α → M) (B : set M) :

(mul_indicator s f)⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B) :=

by letI := classical.dec_pred (∈ s); exact piecewise_preimage s f 1 B

@[to_additive] lemma mul_indicator_one_preimage (s : set M) :

t.mul_indicator 1 ⁻¹' s ∈ ({set.univ, ∅} : set (set α)) :=

classical,

rw [mul_indicator_one', preimage_one],

split_ifs; simp

@[to_additive] lemma mul_indicator_const_preimage_eq_union (U : set α) (s : set M) (a : M)

[decidable (a ∈ s)] [decidable ((1 : M) ∈ s)] :

U.mul_indicator (λ x, a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ (if (1 : M) ∈ s then Uᶜ else ∅) :=

rw [mul_indicator_preimage, preimage_one, preimage_const],

split_ifs; simp [← compl_eq_univ_diff]

@[to_additive] lemma mul_indicator_const_preimage (U : set α) (s : set M) (a : M) :

U.mul_indicator (λ x, a) ⁻¹' s ∈ ({set.univ, U, Uᶜ, ∅} : set (set α)) :=

classical,

rw [mul_indicator_const_preimage_eq_union],

split_ifs; simp

lemma indicator_one_preimage [has_zero M] (U : set α) (s : set M) :

U.indicator 1 ⁻¹' s ∈ ({set.univ, U, Uᶜ, ∅} : set (set α)) :=

indicator_const_preimage _ _ 1

@[to_additive] lemma mul_indicator_preimage_of_not_mem (s : set α) (f : α → M)

{t : set M} (ht : (1:M) ∉ t) :

(mul_indicator s f)⁻¹' t = f ⁻¹' t ∩ s :=

by simp [mul_indicator_preimage, pi.one_def, set.preimage_const_of_not_mem ht]

@[to_additive] lemma mem_range_mul_indicator {r : M} {s : set α} {f : α → M} :

r ∈ range (mul_indicator s f) ↔ (r = 1 ∧ s ≠ univ) ∨ (r ∈ f '' s) :=

by simp [mul_indicator, ite_eq_iff, exists_or_distrib, eq_univ_iff_forall, and_comm, or_comm,

@eq_comm _ r 1]

@[to_additive] lemma mul_indicator_rel_mul_indicator {r : M → M → Prop} (h1 : r 1 1)

(ha : a ∈ s → r (f a) (g a)) :

r (mul_indicator s f a) (mul_indicator s g a) :=

by { simp only [mul_indicator], split_ifs with has has, exacts [ha has, h1] }

end has_one

section monoid

variables [mul_one_class M] {s t : set α} {f g : α → M} {a : α}

@[to_additive] lemma mul_indicator_union_mul_inter_apply (f : α → M) (s t : set α) (a : α) :

mul_indicator (s ∪ t) f a * mul_indicator (s ∩ t) f a =

mul_indicator s f a * mul_indicator t f a :=

by by_cases hs : a ∈ s; by_cases ht : a ∈ t; simp *

@[to_additive] lemma mul_indicator_union_mul_inter (f : α → M) (s t : set α) :

mul_indicator (s ∪ t) f * mul_indicator (s ∩ t) f = mul_indicator s f * mul_indicator t f :=

funext $ mul_indicator_union_mul_inter_apply f s t

@[to_additive] lemma mul_indicator_union_of_not_mem_inter (h : a ∉ s ∩ t) (f : α → M) :

mul_indicator (s ∪ t) f a = mul_indicator s f a * mul_indicator t f a :=

by rw [← mul_indicator_union_mul_inter_apply f s t, mul_indicator_of_not_mem h, mul_one]

@[to_additive] lemma mul_indicator_union_of_disjoint (h : disjoint s t) (f : α → M) :

mul_indicator (s ∪ t) f = λa, mul_indicator s f a * mul_indicator t f a :=

funext $ λa, mul_indicator_union_of_not_mem_inter (λ ha, h.le_bot ha) _

@[to_additive] lemma mul_indicator_mul (s : set α) (f g : α → M) :

mul_indicator s (λa, f a * g a) = λa, mul_indicator s f a * mul_indicator s g a :=

by { funext, simp only [mul_indicator], split_ifs, { refl }, rw mul_one }

@[to_additive] lemma mul_indicator_mul' (s : set α) (f g : α → M) :

mul_indicator s (f * g) = mul_indicator s f * mul_indicator s g :=

mul_indicator_mul s f g

@[simp, to_additive] lemma mul_indicator_compl_mul_self_apply (s : set α) (f : α → M) (a : α) :

mul_indicator sᶜ f a * mul_indicator s f a = f a :=

classical.by_cases (λ ha : a ∈ s, by simp [ha]) (λ ha, by simp [ha])

@[simp, to_additive] lemma mul_indicator_compl_mul_self (s : set α) (f : α → M) :

mul_indicator sᶜ f * mul_indicator s f = f :=

funext $ mul_indicator_compl_mul_self_apply s f

@[simp, to_additive] lemma mul_indicator_self_mul_compl_apply (s : set α) (f : α → M) (a : α) :

mul_indicator s f a * mul_indicator sᶜ f a = f a :=

classical.by_cases (λ ha : a ∈ s, by simp [ha]) (λ ha, by simp [ha])

@[simp, to_additive] lemma mul_indicator_self_mul_compl (s : set α) (f : α → M) :

mul_indicator s f * mul_indicator sᶜ f = f :=

funext $ mul_indicator_self_mul_compl_apply s f

@[to_additive] lemma mul_indicator_mul_eq_left {f g : α → M}

(h : disjoint (mul_support f) (mul_support g)) :

(mul_support f).mul_indicator (f * g) = f :=

refine (mul_indicator_congr $ λ x hx, _).trans mul_indicator_mul_support,

have : g x = 1, from nmem_mul_support.1 (disjoint_left.1 h hx),

rw [pi.mul_apply, this, mul_one]

@[to_additive] lemma mul_indicator_mul_eq_right {f g : α → M}

(h : disjoint (mul_support f) (mul_support g)) :

(mul_support g).mul_indicator (f * g) = g :=

refine (mul_indicator_congr $ λ x hx, _).trans mul_indicator_mul_support,

have : f x = 1, from nmem_mul_support.1 (disjoint_right.1 h hx),

rw [pi.mul_apply, this, one_mul]

@[to_additive] lemma mul_indicator_mul_compl_eq_piecewise

[decidable_pred (∈ s)] (f g : α → M) :

s.mul_indicator f * sᶜ.mul_indicator g = s.piecewise f g :=

ext x,

by_cases h : x ∈ s,

{ rw [piecewise_eq_of_mem _ _ _ h, pi.mul_apply, set.mul_indicator_of_mem h,

set.mul_indicator_of_not_mem (set.not_mem_compl_iff.2 h), mul_one] },

{ rw [piecewise_eq_of_not_mem _ _ _ h, pi.mul_apply, set.mul_indicator_of_not_mem h,

set.mul_indicator_of_mem (set.mem_compl h), one_mul] },

noncomputable def mul_indicator_hom {α} (M) [mul_one_class M] (s : set α) : (α → M) →* (α → M) :=

{ to_fun := mul_indicator s,

map_one' := mul_indicator_one M s,

map_mul' := mul_indicator_mul s }

end monoid

section distrib_mul_action

variables {A : Type*} [add_monoid A] [monoid M] [distrib_mul_action M A]

lemma indicator_smul_apply (s : set α) (r : α → M) (f : α → A) (x : α) :

indicator s (λ x, r x • f x) x = r x • indicator s f x :=

by { dunfold indicator, split_ifs, exacts [rfl, (smul_zero (r x)).symm] }

lemma indicator_smul (s : set α) (r : α → M) (f : α → A) :

indicator s (λ (x : α), r x • f x) = λ (x : α), r x • indicator s f x :=

funext $ indicator_smul_apply s r f

lemma indicator_const_smul_apply (s : set α) (r : M) (f : α → A) (x : α) :

indicator s (λ x, r • f x) x = r • indicator s f x :=

indicator_smul_apply s (λ x, r) f x

lemma indicator_const_smul (s : set α) (r : M) (f : α → A) :

indicator s (λ (x : α), r • f x) = λ (x : α), r • indicator s f x :=

funext $ indicator_const_smul_apply s r f

end distrib_mul_action

section group

variables {G : Type*} [group G] {s t : set α} {f g : α → G} {a : α}

@[to_additive] lemma mul_indicator_inv' (s : set α) (f : α → G) :

mul_indicator s (f⁻¹) = (mul_indicator s f)⁻¹ :=

(mul_indicator_hom G s).map_inv f

@[to_additive] lemma mul_indicator_inv (s : set α) (f : α → G) :

mul_indicator s (λa, (f a)⁻¹) = λa, (mul_indicator s f a)⁻¹ :=

mul_indicator_inv' s f

@[to_additive] lemma mul_indicator_div (s : set α) (f g : α → G) :

mul_indicator s (λ a, f a / g a) =

λ a, mul_indicator s f a / mul_indicator s g a :=

(mul_indicator_hom G s).map_div f g

@[to_additive] lemma mul_indicator_div' (s : set α) (f g : α → G) :

mul_indicator s (f / g) = mul_indicator s f / mul_indicator s g :=

mul_indicator_div s f g

@[to_additive indicator_compl'] lemma mul_indicator_compl (s : set α) (f : α → G) :

mul_indicator sᶜ f = f * (mul_indicator s f)⁻¹ :=

eq_mul_inv_of_mul_eq $ s.mul_indicator_compl_mul_self f

lemma indicator_compl {G} [add_group G] (s : set α) (f : α → G) :

indicator sᶜ f = f - indicator s f :=

by rw [sub_eq_add_neg, indicator_compl']

@[to_additive indicator_diff'] lemma mul_indicator_diff (h : s ⊆ t) (f : α → G) :

mul_indicator (t \ s) f = mul_indicator t f * (mul_indicator s f)⁻¹ :=

eq_mul_inv_of_mul_eq $ by { rw [pi.mul_def, ←mul_indicator_union_of_disjoint, diff_union_self,

union_eq_self_of_subset_right h], exact disjoint_sdiff_self_left }

lemma indicator_diff {G : Type*} [add_group G] {s t : set α} (h : s ⊆ t) (f : α → G) :

indicator (t \ s) f = indicator t f - indicator s f :=

by rw [indicator_diff' h, sub_eq_add_neg]

end group

section comm_monoid

variables [comm_monoid M]

@[to_additive] lemma prod_mul_indicator_subset_of_eq_one [has_one N] (f : α → N)

(g : α → N → M) {s t : finset α} (h : s ⊆ t) (hg : ∀ a, g a 1 = 1) :

∏ i in s, g i (f i) = ∏ i in t, g i (mul_indicator ↑s f i) :=

rw ← finset.prod_subset h _,

{ apply finset.prod_congr rfl,

intros i hi,

congr,

symmetry,

exact mul_indicator_of_mem hi _ },

{ refine λ i hi hn, _,

convert hg i,

exact mul_indicator_of_not_mem hn _ }

add_decl_doc set.sum_indicator_subset_of_eq_zero

lemma prod_mul_indicator_subset (f : α → M) {s t : finset α} (h : s ⊆ t) :

∏ i in s, f i = ∏ i in t, mul_indicator ↑s f i :=

prod_mul_indicator_subset_of_eq_one _ (λ a b, b) h (λ _, rfl)

@[to_additive] lemma _root_.finset.prod_mul_indicator_eq_prod_filter

(s : finset ι) (f : ι → α → M) (t : ι → set α) (g : ι → α) [decidable_pred (λ i, g i ∈ t i)]:

∏ i in s, mul_indicator (t i) (f i) (g i) = ∏ i in s.filter (λ i, g i ∈ t i), f i (g i) :=

refine (finset.prod_filter_mul_prod_filter_not s (λ i, g i ∈ t i) _).symm.trans _,

refine eq.trans _ (mul_one _),

exact congr_arg2 (*)

(finset.prod_congr rfl $ λ x hx, mul_indicator_of_mem (finset.mem_filter.1 hx).2 _)

(finset.prod_eq_one $ λ x hx, mul_indicator_of_not_mem (finset.mem_filter.1 hx).2 _)

@[to_additive] lemma mul_indicator_finset_prod (I : finset ι) (s : set α) (f : ι → α → M) :

mul_indicator s (∏ i in I, f i) = ∏ i in I, mul_indicator s (f i) :=

(mul_indicator_hom M s).map_prod _ _

@[to_additive] lemma mul_indicator_finset_bUnion {ι} (I : finset ι)

(s : ι → set α) {f : α → M} : (∀ (i ∈ I) (j ∈ I), i ≠ j → disjoint (s i) (s j)) →

mul_indicator (⋃ i ∈ I, s i) f = λ a, ∏ i in I, mul_indicator (s i) f a :=

classical,

refine finset.induction_on I _ _,

{ intro h, funext, simp },

assume a I haI ih hI,

funext,

rw [finset.prod_insert haI, finset.set_bUnion_insert, mul_indicator_union_of_not_mem_inter, ih _],

{ assume i hi j hj hij,

exact hI i (finset.mem_insert_of_mem hi) j (finset.mem_insert_of_mem hj) hij },

simp only [not_exists, exists_prop, mem_Union, mem_inter_iff, not_and],

assume hx a' ha',

refine disjoint_left.1 (hI a (finset.mem_insert_self _ _) a' (finset.mem_insert_of_mem ha') _) hx,

exact (ne_of_mem_of_not_mem ha' haI).symm

@[to_additive] lemma mul_indicator_finset_bUnion_apply {ι} (I : finset ι)

(s : ι → set α) {f : α → M} (h : ∀ (i ∈ I) (j ∈ I), i ≠ j → disjoint (s i) (s j)) (x : α) :

mul_indicator (⋃ i ∈ I, s i) f x = ∏ i in I, mul_indicator (s i) f x :=

by rw set.mul_indicator_finset_bUnion I s h

end comm_monoid

section mul_zero_class

variables [mul_zero_class M] {s t : set α} {f g : α → M} {a : α}

lemma indicator_mul (s : set α) (f g : α → M) :

indicator s (λa, f a * g a) = λa, indicator s f a * indicator s g a :=

by { funext, simp only [indicator], split_ifs, { refl }, rw mul_zero }

lemma indicator_mul_left (s : set α) (f g : α → M) :

indicator s (λa, f a * g a) a = indicator s f a * g a :=

by { simp only [indicator], split_ifs, { refl }, rw [zero_mul] }

lemma indicator_mul_right (s : set α) (f g : α → M) :

indicator s (λa, f a * g a) a = f a * indicator s g a :=

by { simp only [indicator], split_ifs, { refl }, rw [mul_zero] }

lemma inter_indicator_mul {t1 t2 : set α} (f g : α → M) (x : α) :

(t1 ∩ t2).indicator (λ x, f x * g x) x = t1.indicator f x * t2.indicator g x :=

by { rw [← set.indicator_indicator], simp [indicator] }

end mul_zero_class

section mul_zero_one_class

variables [mul_zero_one_class M]

lemma inter_indicator_one {s t : set α} :

(s ∩ t).indicator (1 : _ → M) = s.indicator 1 * t.indicator 1 :=

funext (λ _, by simpa only [← inter_indicator_mul, pi.mul_apply, pi.one_apply, one_mul])

lemma indicator_prod_one {s : set α} {t : set β} {x : α} {y : β} :

(s ×ˢ t).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=

by { classical, simp [indicator_apply, ←ite_and] }

variables (M) [nontrivial M]

lemma indicator_eq_zero_iff_not_mem {U : set α} {x : α} :

indicator U 1 x = (0 : M) ↔ x ∉ U :=

by { classical, simp [indicator_apply, imp_false] }

lemma indicator_eq_one_iff_mem {U : set α} {x : α} :

indicator U 1 x = (1 : M) ↔ x ∈ U :=

by { classical, simp [indicator_apply, imp_false] }

lemma indicator_one_inj {U V : set α} (h : indicator U (1 : α → M) = indicator V 1) : U = V :=

by { ext, simp_rw [← indicator_eq_one_iff_mem M, h] }

end mul_zero_one_class

section order

variables [has_one M] {s t : set α} {f g : α → M} {a : α} {y : M}

variables [has_le M]

@[to_additive] lemma mul_indicator_apply_le' (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 1 ≤ y) :

mul_indicator s f a ≤ y :=

by_cases ha : a ∈ s,

{ simpa [ha] using hfg ha },

{ simpa [ha] using hg ha },

@[to_additive] lemma mul_indicator_le' (hfg : ∀ a ∈ s, f a ≤ g a) (hg : ∀ a ∉ s, 1 ≤ g a) :

mul_indicator s f ≤ g :=

λ a, mul_indicator_apply_le' (hfg _) (hg _)

@[to_additive] lemma le_mul_indicator_apply {y} (hfg : a ∈ s → y ≤ g a) (hf : a ∉ s → y ≤ 1) :

y ≤ mul_indicator s g a :=

@mul_indicator_apply_le' α Mᵒᵈ ‹_› _ _ _ _ _ hfg hf

@[to_additive] lemma le_mul_indicator (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a ≤ 1) :

f ≤ mul_indicator s g :=

λ a, le_mul_indicator_apply (hfg _) (hf _)

variables [preorder M]

lemma one_le_mul_indicator_apply (h : a ∈ s → 1 ≤ f a) : 1 ≤ mul_indicator s f a :=

le_mul_indicator_apply h (λ _, le_rfl)

lemma one_le_mul_indicator (h : ∀ a ∈ s, 1 ≤ f a) (a : α) : 1 ≤ mul_indicator s f a :=

one_le_mul_indicator_apply (h a)

@[to_additive] lemma mul_indicator_apply_le_one (h : a ∈ s → f a ≤ 1) : mul_indicator s f a ≤ 1 :=

mul_indicator_apply_le' h (λ _, le_rfl)

@[to_additive] lemma mul_indicator_le_one (h : ∀ a ∈ s, f a ≤ 1) (a : α) :

mul_indicator s f a ≤ 1 :=

mul_indicator_apply_le_one (h a)

@[to_additive] lemma mul_indicator_le_mul_indicator (h : f a ≤ g a) :

mul_indicator s f a ≤ mul_indicator s g a :=

mul_indicator_rel_mul_indicator le_rfl (λ _, h)

attribute [mono] mul_indicator_le_mul_indicator indicator_le_indicator

@[to_additive] lemma mul_indicator_le_mul_indicator_of_subset (h : s ⊆ t) (hf : ∀ a, 1 ≤ f a)

(a : α) :

mul_indicator s f a ≤ mul_indicator t f a :=

mul_indicator_apply_le' (λ ha, le_mul_indicator_apply (λ _, le_rfl) (λ hat, (hat $ h ha).elim))

(λ ha, one_le_mul_indicator_apply (λ _, hf _))

@[to_additive] lemma mul_indicator_le_self' (hf : ∀ x ∉ s, 1 ≤ f x) : mul_indicator s f ≤ f :=

mul_indicator_le' (λ _ _, le_rfl) hf

@[to_additive] lemma mul_indicator_Union_apply {ι M} [complete_lattice M] [has_one M]

(h1 : (⊥:M) = 1) (s : ι → set α) (f : α → M) (x : α) :

mul_indicator (⋃ i, s i) f x = ⨆ i, mul_indicator (s i) f x :=

by_cases hx : x ∈ ⋃ i, s i,

{ rw [mul_indicator_of_mem hx],

rw [mem_Union] at hx,

refine le_antisymm _ (supr_le $ λ i, mul_indicator_le_self' (λ x hx, h1 ▸ bot_le) x),

rcases hx with ⟨i, hi⟩,

exact le_supr_of_le i (ge_of_eq $ mul_indicator_of_mem hi _) },

{ rw [mul_indicator_of_not_mem hx],

simp only [mem_Union, not_exists] at hx,

simp [hx, ← h1] }

end order

section canonically_ordered_monoid

variables [canonically_ordered_monoid M]

@[to_additive] lemma mul_indicator_le_self (s : set α) (f : α → M) :

mul_indicator s f ≤ f :=

mul_indicator_le_self' $ λ _ _, one_le _

@[to_additive] lemma mul_indicator_apply_le {a : α} {s : set α} {f g : α → M}

(hfg : a ∈ s → f a ≤ g a) :

mul_indicator s f a ≤ g a :=

mul_indicator_apply_le' hfg $ λ _, one_le _

@[to_additive] lemma mul_indicator_le {s : set α} {f g : α → M} (hfg : ∀ a ∈ s, f a ≤ g a) :

mul_indicator s f ≤ g :=

mul_indicator_le' hfg $ λ _ _, one_le _

end canonically_ordered_monoid

lemma indicator_le_indicator_nonneg {β} [linear_order β] [has_zero β] (s : set α) (f : α → β) :

s.indicator f ≤ {x | 0 ≤ f x}.indicator f :=

intro x,

classical,

simp_rw indicator_apply,

split_ifs,

{ exact le_rfl, },

{ exact (not_le.mp h_1).le, },

{ exact h_1, },

{ exact le_rfl, },

lemma indicator_nonpos_le_indicator {β} [linear_order β] [has_zero β] (s : set α) (f : α → β) :

{x | f x ≤ 0}.indicator f ≤ s.indicator f :=

@indicator_le_indicator_nonneg α βᵒᵈ _ _ s f

end set

@[to_additive] lemma monoid_hom.map_mul_indicator

{M N : Type*} [mul_one_class M] [mul_one_class N] (f : M →* N)

(s : set α) (g : α → M) (x : α) :

f (s.mul_indicator g x) = s.mul_indicator (f ∘ g) x :=

congr_fun (set.mul_indicator_comp_of_one f.map_one).symm x