How to show that a Finset E is measurable?

Stream: general

[Icaro Costa]

I am new to Lean, and I am trying to prove a theorem that involves using subsets of finite and discrete measurable sets. Lean seems to require me to show first that Finset E is measurable first. This is my current code:

live shell

import Mathlib
open ProbabilityTheory MeasureTheory
open scoped ENNReal

variable {E : Type*} [MeasurableSpace E][DiscreteMeasurableSpace E][Fintype E]
variable {w : E → NNReal}

theorem weight_is_measurable: Measurable w := by {
  apply Measurable.of_discrete
}

def S (A : Finset E): NNReal := ∑ x ∈ A, w x

instance : MeasurableSpace (Finset E) := by
{

}


-- theorem sum_is_measurable: Measurable S

How can I prove it?

[Aaron Liu]

Sorry, your code does not work for me in the web editor. Please create a #mwe.

[Edward van de Meent]

why do you want to prove Measurable S?

[Icaro Costa]

Aaron Liu said:

Sorry, your code does not work for me in the web editor. Please create a #mwe.

Really? I don't see any error besides a warning

[Aaron Liu]

I mean when I uncomment the theorem sum_is_measurable

[Icaro Costa]

Edward van de Meent said:

why do you want to prove Measurable S?

At the end, I want to prove that it doesn't matter what subset I choose from E, the expected value of that sum is proportional to the expected value over the whole set. But first, I wanted to try simpler things, so I learn how to use the MeasureTheory library better

[Icaro Costa]

Aaron Liu said:

I mean when I uncomment the theorem sum_is_measurable

Oh yeah, so, the reason I am trying to prove that Finset E is a MeasurableSpace instance is because of that error

[Icaro Costa]

To be honest, I don't know how to begin the proof. I tried to do 'intro x or ext x' to say 'let x be an element of this finite set', but it didn't work. I wanted to show that Finset is Set, so I can use higher theorems

[Edward van de Meent]

there's an easy way to do that:

instance : MeasurableSpace (Finset E) := MeasurableSpace.comap (Finset.toSet) inferInstance

[Edward van de Meent]

here the measuable sets (of finite sets) are precisely those which are measurable as set of sets