simple function from finite restriction

Stream: Is there code for X?

[Alex Kontorovich]

Can someone please help me create a simple function? Say I have a function f and a finite set s; I want to say that the restriction of f to s is a simple function, something like this...?

import measure_theory.integral.lebesgue

example (f : ℝ → ℝ) (s : finset ℝ) : ∃ g : measure_theory.simple_func ℝ ℝ, (g : ℝ → ℝ) = (s : set ℝ).indicator f :=
begin
  sorry,
end

[Eric Wieser]

I would probably start as

import measure_theory.integral.lebesgue

noncomputable example (f : ℝ → ℝ) (s : finset ℝ) : measure_theory.simple_func ℝ ℝ :=
{ to_fun := (s : set ℝ).indicator f,
  measurable_set_fiber' := λ x, sorry,
  finite_range' := sorry  }

but maybe that's obvious

[Adam Topaz]

This might be one of the ugliest proofs I've written in a while... plenty of golfing room...

import tactic
import measure_theory.integral.lebesgue

open_locale classical

lemma measurable_of_cofinite (S T : set ℝ)
  (hT : T.finite) (h : Tᶜ ⊆ S) : measurable_set S :=
begin
  suffices : Sᶜ.finite,
  { rw (show S = Sᶜᶜ, by simp),
    apply measurable_set.compl,
    apply set.finite.measurable_set this },
  suffices : Sᶜ ⊆ T,
  { exact hT.subset this },
  exact set.compl_subset_comm.mp h
end

noncomputable
def foobar (f : ℝ → ℝ) (S : finset ℝ) : measure_theory.simple_func ℝ ℝ :=
{ to_fun := (S : set ℝ).indicator f,
  measurable_set_fiber' := begin
    intros x,
    by_cases hx : x = 0,
    rw hx,
    { suffices : (S : set ℝ)ᶜ ⊆ (S : set ℝ).indicator f ⁻¹' {0},
      { apply measurable_of_cofinite _ S _ this,
        exact finset.finite_to_set S },
      intros t ht,
      simp only [set.indicator_apply, set.mem_preimage,
        finset.mem_coe, set.mem_singleton_iff, ite_eq_right_iff],
      intros ht',
      exact false.elim (ht ht') },
    have : (S : set ℝ).indicator f ⁻¹' {x} = S.filter (λ y, f y = x),
    { ext t,
      simp only [set.mem_preimage, set.mem_singleton_iff,
        finset.coe_filter, set.mem_sep_eq, finset.mem_coe,
        set.indicator_apply],
      split_ifs,
      { refine ⟨λ hh, ⟨h, hh⟩, λ hh, hh.2⟩ },
      { refine ⟨λ hh, false.elim (hx hh.symm), λ hh,
          false.elim (h hh.1)⟩, } },
    rw this,
    apply set.finite.measurable_set,
    exact (finset.filter (λ (y : ℝ), f y = x) S).finite_to_set
  end,
  finite_range' := begin
    suffices : set.range ((S : set ℝ).indicator f) ⊆ (f '' (S : set ℝ) ∪ {0}),
    { apply set.finite.subset _ this,
      apply set.finite.union, swap, { apply set.finite_singleton },
      apply set.finite.image,
      exact finset.finite_to_set S },
    intros x hx,
    simp at hx,
    obtain ⟨y,hy⟩ := hx,
    simp [set.indicator_apply] at hy,
    by_cases y ∈ S,
    left, { rw if_pos h at hy, rw ← hy, use [y, h, rfl] },
    right, { rw if_neg h at hy, rw ← hy, simp }
  end }

[Floris van Doorn]

Golfed a bit :-)

import measure_theory.integral.lebesgue

noncomputable theory
open set measure_theory
open_locale big_operators

def foo (f : ℝ → ℝ) (s : finset ℝ) : simple_func ℝ ℝ :=
∑ i in s, (simple_func.const ℝ (f i)).piecewise
  {i} (measurable_set_singleton i) (simple_func.const ℝ 0)

lemma coe_sum {s : finset ℝ} (f : ℝ → simple_func ℝ ℝ) (x : ℝ) :
  (∑ i in s, f i) x = ∑ i in s, f i x :=
by { induction s using finset.induction with i s hi ih, simp, simp [hi, ih] }

lemma coe_foo (f : ℝ → ℝ) (s : finset ℝ) : (foo f s : ℝ → ℝ) = (s : set ℝ).indicator f :=
begin
  ext x,
  simp_rw [foo, coe_sum, simple_func.piecewise_apply, simple_func.const_apply, mem_singleton_iff,
    finset.sum_ite_eq, indicator_apply, finset.mem_coe]
end