## Stream: maths

### Topic: Inverse image of the indicator function

#### Koundinya Vajjha (Jan 10 2019 at 09:04):

I'm struggling to get a hold of the inverse image of the indicator function:

s : Type u

def indicator (a : set s) [decidable_pred (λ (x:s), x ∈ a)]
:= (λ x : s, if (x ∈ a) then (1:ℝ) else 0)


I want to say that if $X = \mathbf{1}_A$ then $X^{-1}(B)$ is one of $A$ ,$A^c$, $\emptyset$ or $\emptyset^c$.
Any help would be appreciated.

#### Koundinya Vajjha (Jan 10 2019 at 09:05):

Also, how do I LaTeX?

#### Johan Commelin (Jan 10 2019 at 09:07):

LaTeX with double dollars: $blah$

#### Joey van Langen (Jan 10 2019 at 09:09):

You can get the inverse image with the symbol  ⁻¹' , which is \inv ' in lean

#### Joey van Langen (Jan 10 2019 at 09:09):

It is in mathlib/data/set/basic

#### Koundinya Vajjha (Jan 10 2019 at 09:11):

Yes I saw that, but I'm not able to state what I want to prove...

#### Johan Commelin (Jan 10 2019 at 09:12):

What have you tried? Can you give your attempt (+ error?)

#### Koundinya Vajjha (Jan 10 2019 at 09:16):

def indicator_inv (a: set s) (b : set ℝ) [decidable_pred (λ (x:s), x ∈ a)] :
indicator s a ⁻¹'  (b) = { -- what goes here ? }


#### Johan Commelin (Jan 10 2019 at 09:19):

I see. I think you want 4 lemmas

#### Johan Commelin (Jan 10 2019 at 09:19):

But maybe it depends on why you want this, and how you want to use this.

#### Joey van Langen (Jan 10 2019 at 09:21):

import data.set.basic
import data.real.basic

universe u

variable (s : Type u)

def indicator (a : set s) [decidable_pred (λ (x:s), x ∈ a)]
:= (λ x : s, if (x ∈ a) then (1:ℝ) else 0)

lemma preimage_indicator (a : set s) [decidable_pred (λ (x:s), x ∈ a)] (b : set ℝ):
(indicator s a) ⁻¹' b = a ∨ (indicator s a) ⁻¹' b = ∅ ∨
(indicator s a) ⁻¹' b = - a ∨ (indicator s a) ⁻¹' b = -∅ :=
sorry


#### Koundinya Vajjha (Jan 10 2019 at 09:22):

I'm trying to prove that the indicator function of an event is a random variable.

def is_random_variable {s : Type u} [measurable_space s] (X : s → ℝ) := measurable X

lemma is_random_variable_indicator (a : set s) [decidable_eq (set s)] [decidable_pred (λ (x:s), x ∈ a)]:
is_random_variable (indicator _ a) :=
begin
intros b h,
unfold measurable_space.map,
unfold set.preimage, dsimp,
sorry
end


#### Koundinya Vajjha (Jan 10 2019 at 09:24):

I'm stuck at

s : Type u,
_inst_1 : measurable_space s,
a : set s,
_inst_2 : decidable_eq (set s),
_inst_3 : decidable_pred (λ (x : s), x ∈ a),
b : set ℝ,
h : measurable_space.is_measurable (measure_theory.borel ℝ) b
⊢ measurable_space.is_measurable _inst_1 {x : s | indicator s a x ∈ b}


#### Koundinya Vajjha (Jan 10 2019 at 09:25):

I want to prove a lemma which would possibly rewrite the {x : s | indicator s a x ∈ b} maybe...

#### Koundinya Vajjha (Jan 10 2019 at 09:28):

@Joey van Langen thanks I'll try that.

Last updated: May 06 2021 at 18:20 UTC