# Zulip Chat Archive

## 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):

How about this:

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