fix(algebra/indicator_function): add missing decidable instances to lemma statements (#13834)

This keeps the definition of `set.indicator` as non-computable, but ensures that when lemmas are applied they generalize to any decidable instances.

Author: eric-wieser

src/algebra/indicator_function.lean

@@ -21,12 +21,14 @@ But since it is usually used to restrict a function to a certain set `s`,
 we let the indicator function take the value `f x` for some function `f`, instead of `1`.
 If the usual indicator function is needed, just set `f` to be the constant function `λx, 1`.
 
+The indicator function is implemented non-computably, to avoid having to pass around `decidable`
+arguments. This is in contrast with the design of `pi.single` or `set.piecewise`.
+
 ## Tags
 indicator, characteristic
 -/
 
-noncomputable theory
-open_locale classical big_operators
+open_locale big_operators
 open function
 
 variables {α β ι M N : Type*}
@@ -37,30 +39,40 @@ section has_one
 variables [has_one M] [has_one N] {s t : set α} {f g : α → M} {a : α}
 
 /-- `indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  -/
-def indicator {M} [has_zero M] (s : set α) (f : α → M) : α → M := λ x, if x ∈ s then f x else 0
+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
 
 /-- `mul_indicator s f a` is `f a` if `a ∈ s`, `1` otherwise.  -/
 @[to_additive]
-def mul_indicator (s : set α) (f : α → M) : α → M := λ x, if x ∈ s then f x else 1
+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 : s.piecewise f 1 = s.mul_indicator f := rfl
+@[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 : α) :
-  mul_indicator s f a = if a ∈ s then f a else 1 := 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 := if_pos h
+  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 := if_neg h
+  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 :=
-if h : a ∈ s then or.inr (mul_indicator_of_mem h f) else or.inl (mul_indicator_of_not_mem h f)
+begin
+  by_cases h : a ∈ s,
+  { exact or.inr (mul_indicator_of_mem h f) },
+  { exact or.inl (mul_indicator_of_not_mem h f) }
+end
 
 @[simp, to_additive] lemma mul_indicator_apply_eq_self :
   s.mul_indicator f a = f a ↔ (a ∉ s → f a = 1) :=
-ite_eq_left_iff.trans $ by rw [@eq_comm _ (f a)]
+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]
@@ -71,7 +83,7 @@ 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) :=
-ite_eq_right_iff
+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 :=
@@ -108,7 +120,7 @@ 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 :=
-piecewise_range_comp _ _ _
+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 :=
@@ -142,9 +154,10 @@ funext $ λx, by { simp only [mul_indicator], split_ifs, repeat {simp * at * {co
   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 : α} :
+@[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 :=
-s.apply_piecewise _ _ (λ _, h)
+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) :=
@@ -168,7 +181,7 @@ end
 
 @[to_additive] lemma mul_indicator_preimage (s : set α) (f : α → M) (B : set M) :
   (mul_indicator s f)⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B) :=
-piecewise_preimage s f 1 B
+by letI := classical.dec_pred (∈ s); exact piecewise_preimage s f 1 B
 
 @[to_additive] lemma mul_indicator_preimage_of_not_mem (s : set α) (f : α → M)
   {t : set M} (ht : (1:M) ∉ t) :
@@ -264,7 +277,7 @@ end
 
 /-- `set.mul_indicator` as a `monoid_hom`. -/
 @[to_additive "`set.indicator` as an `add_monoid_hom`."]
-def mul_indicator_hom {α} (M) [mul_one_class M] (s : set α) : (α → M) →* (α → M) :=
+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 }
@@ -374,7 +387,7 @@ lemma prod_mul_indicator_subset (f : α → M) {s t : finset α} (h : s ⊆ t) :
 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 : ι → α) :
+  (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) :=
 begin
   refine (finset.prod_filter_mul_prod_filter_not s (λ i, g i ∈ t i) _).symm.trans _,
@@ -392,6 +405,7 @@ end
   (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 :=
 begin
+  classical,
   refine finset.induction_on I _ _,
   { intro h, funext, simp },
   assume a I haI ih hI,
@@ -439,7 +453,11 @@ funext (λ _, by simpa only [← inter_indicator_mul, pi.mul_apply, pi.one_apply
 
 lemma indicator_prod_one {s : set α} {t : set β} {x : α} {y : β} :
   (s ×ˢ t : set _).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=
-by simp [indicator, ← ite_and]
+begin
+  letI := classical.dec_pred (∈ s),
+  letI := classical.dec_pred (∈ t),
+  simp [indicator_apply, ← ite_and],
+end
 
 end mul_zero_one_class
 
@@ -452,7 +470,11 @@ 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 :=
-if ha : a ∈ s then by simpa [ha] using hfg ha else by simpa [ha] using hg ha
+begin
+  by_cases ha : a ∈ s,
+  { simpa [ha] using hfg ha },
+  { simpa [ha] using hg ha },
+end
 
 @[to_additive] lemma mul_indicator_le' (hfg : ∀ a ∈ s, f a ≤ g a) (hg : ∀ a ∉ s, 1 ≤ g a) :
   mul_indicator s f ≤ g :=
@@ -540,6 +562,7 @@ lemma indicator_le_indicator_nonneg {β} [linear_order β] [has_zero β] (s : se
   s.indicator f ≤ {x | 0 ≤ f x}.indicator f :=
 begin
   intro x,
+  classical,
   simp_rw indicator_apply,
   split_ifs,
   { exact le_rfl, },

src/combinatorics/simple_graph/inc_matrix.lean

@@ -40,8 +40,6 @@ incidence matrix for each `simple_graph α` has the same type.
   arbitrary orientation of a simple graph.
 -/
 
-noncomputable theory
-
 open finset matrix simple_graph sym2
 open_locale big_operators matrix
 
@@ -50,7 +48,7 @@ variables (R : Type*) {α : Type*} (G : simple_graph α)
 
 /-- `G.inc_matrix R` is the `α × sym2 α` matrix whose `(a, e)`-entry is `1` if `e` is incident to
 `a` and `0` otherwise. -/
-def inc_matrix [has_zero R] [has_one R] : matrix α (sym2 α) R :=
+noncomputable def inc_matrix [has_zero R] [has_one R] : matrix α (sym2 α) R :=
 λ a, (G.incidence_set a).indicator 1
 
 variables {R}
@@ -70,6 +68,7 @@ variables [mul_zero_one_class R] {a b : α} {e : sym2 α}
 lemma inc_matrix_apply_mul_inc_matrix_apply :
   G.inc_matrix R a e * G.inc_matrix R b e = (G.incidence_set a ∩ G.incidence_set b).indicator 1 e :=
 begin
+  classical,
   simp only [inc_matrix, set.indicator_apply, ←ite_and_mul_zero,
     pi.one_apply, mul_one, set.mem_inter_eq],
   congr,
@@ -162,6 +161,7 @@ variables [fintype (sym2 α)] [semiring R] {a b : α} {e : sym2 α}
 lemma inc_matrix_mul_transpose_apply_of_adj (h : G.adj a b) :
   (G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ) a b = (1 : R) :=
 begin
+  classical,
   simp_rw [matrix.mul_apply, matrix.transpose_apply, inc_matrix_apply_mul_inc_matrix_apply,
     set.indicator_apply, pi.one_apply, sum_boole],
   convert nat.cast_one,

src/geometry/euclidean/circumcenter.lean

@@ -615,7 +615,7 @@ begin
              fs.subset_univ
              (λ i, zero_smul ℝ _),
            set.indicator_apply],
-  congr, funext, congr' 2
+  congr,
 end
 
 omit V

src/measure_theory/function/conditional_expectation.lean

@@ -853,6 +853,7 @@ begin
   { refine lintegral_congr_ae (ae_restrict_of_ae _),
     refine (@indicator_const_Lp_coe_fn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono (λ x hx, _),
     rw hx,
+    classical,
     simp_rw set.indicator_apply,
     split_ifs; simp, },
   rw [h_eq, lintegral_indicator _ hs, lintegral_const, measure.restrict_restrict hs],

src/measure_theory/function/uniform_integrable.lean

@@ -809,7 +809,7 @@ begin
       ((hf i).nnnorm.measurable_set_lt strongly_measurable_const)))
       (strongly_measurable.ae_strongly_measurable ((hf i).indicator
       (strongly_measurable_const.measurable_set_le (hf i).nnnorm))) hp),
-    { rw [indicator, pi.add_apply],
+    { rw [pi.add_apply, indicator_apply],
       split_ifs with hx,
       { rw [indicator_of_not_mem, add_zero],
         simpa using hx },

src/measure_theory/integral/bochner.lean

@@ -142,7 +142,7 @@ Bochner integral, simple function, function space, Lebesgue dominated convergenc
 -/
 
 noncomputable theory
-open_locale classical topological_space big_operators nnreal ennreal measure_theory
+open_locale topological_space big_operators nnreal ennreal measure_theory
 open set filter topological_space ennreal emetric
 
 namespace measure_theory
@@ -294,12 +294,13 @@ lemma integral_eq {m : measurable_space α} (μ : measure α) (f : α →ₛ F)
   f.integral μ = ∑ x in f.range, (μ (f ⁻¹' {x})).to_real • x :=
 by simp [integral, set_to_simple_func, weighted_smul_apply]
 
-lemma integral_eq_sum_filter {m : measurable_space α} (f : α →ₛ F) (μ : measure α) :
+lemma integral_eq_sum_filter [decidable_pred (λ x : F, x ≠ 0)] {m : measurable_space α} (f : α →ₛ F)
+  (μ : measure α) :
   f.integral μ = ∑ x in f.range.filter (λ x, x ≠ 0), (μ (f ⁻¹' {x})).to_real • x :=
-by { rw [integral_def, set_to_simple_func_eq_sum_filter], simp_rw weighted_smul_apply, }
+by { rw [integral_def, set_to_simple_func_eq_sum_filter], simp_rw weighted_smul_apply, congr }
 
 /-- The Bochner integral is equal to a sum over any set that includes `f.range` (except `0`). -/
-lemma integral_eq_sum_of_subset {f : α →ₛ F} {s : finset F}
+lemma integral_eq_sum_of_subset [decidable_pred (λ x : F, x ≠ 0)] {f : α →ₛ F} {s : finset F}
   (hs : f.range.filter (λ x, x ≠ 0) ⊆ s) : f.integral μ = ∑ x in s, (μ (f ⁻¹' {x})).to_real • x :=
 begin
   rw [simple_func.integral_eq_sum_filter, finset.sum_subset hs],
@@ -310,14 +311,15 @@ end
 
 @[simp] lemma integral_const {m : measurable_space α} (μ : measure α) (y : F) :
   (const α y).integral μ = (μ univ).to_real • y :=
-calc (const α y).integral μ = ∑ z in {y}, (μ ((const α y) ⁻¹' {z})).to_real • z :
+by classical; calc (const α y).integral μ = ∑ z in {y}, (μ ((const α y) ⁻¹' {z})).to_real • z :
   integral_eq_sum_of_subset $ (filter_subset _ _).trans (range_const_subset _ _)
 ... = (μ univ).to_real • y : by simp
 
 @[simp] lemma integral_piecewise_zero {m : measurable_space α} (f : α →ₛ F) (μ : measure α)
   {s : set α} (hs : measurable_set s) :
   (piecewise s hs f 0).integral μ = f.integral (μ.restrict s) :=
 begin
+  classical,
   refine (integral_eq_sum_of_subset _).trans
     ((sum_congr rfl $ λ y hy, _).trans (integral_eq_sum_filter _ _).symm),
   { intros y hy,
@@ -326,7 +328,8 @@ begin
     rcases hy with ⟨⟨rfl, -⟩|⟨x, hxs, rfl⟩, h₀⟩,
     exacts [(h₀ rfl).elim, ⟨set.mem_range_self _, h₀⟩] },
   { dsimp,
-    rw [indicator_preimage_of_not_mem, measure.restrict_apply (f.measurable_set_preimage _)],
+    rw [set.piecewise_eq_indicator, indicator_preimage_of_not_mem,
+      measure.restrict_apply (f.measurable_set_preimage _)],
     exact λ h₀, (mem_filter.1 hy).2 (eq.symm h₀) }
 end
 
@@ -687,10 +690,15 @@ variables [normed_group E] [normed_space ℝ E] [complete_space E]
           [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class ℝ 𝕜 E]
           [normed_group F] [normed_space ℝ F] [complete_space F]
 
+section
+open_locale classical
+
 /-- The Bochner integral -/
 def integral {m : measurable_space α} (μ : measure α) (f : α → E) : E :=
 if hf : integrable f μ then L1.integral (hf.to_L1 f) else 0
 
+end
+
 /-! In the notation for integrals, an expression like `∫ x, g ∥x∥ ∂μ` will not be parsed correctly,
   and needs parentheses. We do not set the binding power of `r` to `0`, because then
   `∫ x, f x = 0` will be parsed incorrectly. -/
@@ -707,7 +715,7 @@ variables {f g : α → E} {m : measurable_space α} {μ : measure α}
 
 lemma integral_eq (f : α → E) (hf : integrable f μ) :
   ∫ a, f a ∂μ = L1.integral (hf.to_L1 f) :=
-dif_pos hf
+@dif_pos _ (id _) hf _ _ _
 
 lemma integral_eq_set_to_fun (f : α → E) :
   ∫ a, f a ∂μ = set_to_fun μ (weighted_smul μ) (dominated_fin_meas_additive_weighted_smul μ) f :=
@@ -717,7 +725,7 @@ lemma L1.integral_eq_integral (f : α →₁[μ] E) : L1.integral f = ∫ a, f a
 (L1.set_to_fun_eq_set_to_L1 (dominated_fin_meas_additive_weighted_smul μ) f).symm
 
 lemma integral_undef (h : ¬ integrable f μ) : ∫ a, f a ∂μ = 0 :=
-dif_neg h
+@dif_neg _ (id _) h _ _ _
 
 lemma integral_non_ae_strongly_measurable (h : ¬ ae_strongly_measurable f μ) : ∫ a, f a ∂μ = 0 :=
 integral_undef $ not_and_of_not_left _ h

src/measure_theory/probability_mass_function/monad.lean

@@ -147,7 +147,7 @@ calc (p.bind f).to_outer_measure s
   ... = ∑' (a : α), ↑(p a) * ∑' (b : β), if b ∈ s then ↑(f a b) else (0 : ℝ≥0∞) :
     tsum_congr (λ a, congr_arg (λ x, ↑(p a) * x) $ tsum_congr (λ b, by split_ifs; refl))
   ... = ∑' (a : α), ↑(p a) * (f a).to_outer_measure s :
-    tsum_congr (λ a, by rw [to_outer_measure_apply, set.indicator])
+    tsum_congr (λ a, by simp only [to_outer_measure_apply, set.indicator_apply])
 
 /-- The measure of a set under `p.bind f` is the sum over `a : α`
   of the probability of `a` under `p` times the measure of the set under `f a` -/

src/topology/instances/ennreal.lean

@@ -841,12 +841,7 @@ lemma tsum_mono_subtype (f : α → ℝ≥0∞) {s t : set α} (h : s ⊆ t) :
 begin
   simp only [tsum_subtype],
   apply ennreal.tsum_le_tsum,
-  assume x,
-  split_ifs,
-  { exact le_rfl },
-  { exact (h_2 (h h_1)).elim },
-  { exact zero_le _ },
-  { exact le_rfl }
+  exact indicator_le_indicator_of_subset h (λ _, zero_le _),
 end
 
 lemma tsum_union_le (f : α → ℝ≥0∞) (s t : set α) :