Inverse image of the indicator function

Stream: maths

[Koundinya Vajjha]

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]

Also, how do I LaTeX?

[Johan Commelin]

LaTeX with double dollars: $$ blah $$

[Joey van Langen]

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

[Joey van Langen]

It is in mathlib/data/set/basic

[Koundinya Vajjha]

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

[Johan Commelin]

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

[Koundinya Vajjha]

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

[Johan Commelin]

I see. I think you want 4 lemmas

[Johan Commelin]

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

[Joey van Langen]

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]

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]

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]

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

[Koundinya Vajjha]

@Joey van Langen thanks I'll try that.