Zulip Chat Archive

Stream: maths

Topic: Inverse image of the indicator function


view this post on Zulip 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=1AX = \mathbf{1}_A then X1(B)X^{-1}(B) is one of AA ,Ac A^c, \emptyset or c\emptyset^c.
Any help would be appreciated.

view this post on Zulip Koundinya Vajjha (Jan 10 2019 at 09:05):

Also, how do I LaTeX?

view this post on Zulip Johan Commelin (Jan 10 2019 at 09:07):

LaTeX with double dollars: $$ blah $$

view this post on Zulip Joey van Langen (Jan 10 2019 at 09:09):

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

view this post on Zulip Joey van Langen (Jan 10 2019 at 09:09):

It is in mathlib/data/set/basic

view this post on Zulip Koundinya Vajjha (Jan 10 2019 at 09:11):

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

view this post on Zulip Johan Commelin (Jan 10 2019 at 09:12):

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

view this post on Zulip 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 ? }

view this post on Zulip Johan Commelin (Jan 10 2019 at 09:19):

I see. I think you want 4 lemmas

view this post on Zulip Johan Commelin (Jan 10 2019 at 09:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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}

view this post on Zulip 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...

view this post on Zulip 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