## Stream: new members

### Topic: union of unindexed sets

#### Iocta (Aug 27 2020 at 20:47):

There are a number of different unioning functions. Is there one that would work here?

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
import tactic.fin_cases
import data.set.basic
import data.real.basic
import data.complex.exponential
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal
import data.finset.basic
import data.finset.intervals
import algebra.big_operators
import algebra.big_operators.intervals

open_locale big_operators

noncomputable theory

universe u

variables (Ω : Type u) (γ : Type u)

example (p : pmf (set Ω)) (X : set Ω → ℝ) (h: p (set.Union {s : set Ω | X s > 0 }) > 0) :
∃ δ > (0:real), p (set.Union {s : set Ω | (X s) ≥ δ } ) > 0 := sorry


#### Iocta (Aug 27 2020 at 20:51):

In english, the statement is "Let X be a random variable with P(X>0)>0. Prove that there is a delta >0 such that P(X>=delta)>0."

#### Kenny Lau (Aug 27 2020 at 21:01):

are you sure pmf (set Ω) is the correct type?

#### Kenny Lau (Aug 27 2020 at 21:02):

a random variable is a measurable function from a probability space to R right

#### Kenny Lau (Aug 27 2020 at 21:03):

and "P(X>0)" means the measure of { s | X s > 0 }

#### Kenny Lau (Aug 27 2020 at 21:03):

there is no set.Union

#### Reid Barton (Aug 27 2020 at 21:03):

I feel like at least one of your other imports probably imports data.nat.basic for you

#### Iocta (Aug 27 2020 at 21:07):

I'm not sure if I have the correct type. If I say p: pmf \Omega X : \Omega -> real, then h : p { w : \Omega | X w > 0 }  is wrong because p should take omegas, not set Omegas

#### Iocta (Aug 27 2020 at 21:15):

So idk what h is if p: pmf \Omega.

#### Iocta (Aug 29 2020 at 07:31):

What's wrong with this tsum?

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
import tactic.fin_cases
import data.set.basic
import data.real.basic
import data.complex.exponential
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal
import data.finset.basic
import data.finset.intervals
import algebra.big_operators
import algebra.big_operators.intervals
import measure_theory.measure_space

open measure_theory

open_locale big_operators

noncomputable theory

universe u

example
{Ω : Type u}
[measurable_space Ω]
(p : measure Ω) [probability_measure p]
(X : Ω → ℝ)
(h : p {ω : Ω | X ω > 0} > 0):
∃ δ > 0, p {ω : Ω | X ω ≥ δ } > 0 :=
begin
let A := {ω : Ω | X ω > 0},
let A' := λ(n:{n : ℕ | n > 0}), {ω : Ω | X ω > 1/n},
have union_to_A: (⋃ n, A' n ) = A, sorry,
have subadditivity: p A ≤ (∑' (n:{n':ℕ|n'>0}), (λ m, p.measure_of (A' m)))
-- type mismatch at application
--   ∑' (n : ↥{n' : ℕ | n' > 0}), λ (m : ↥{n : ℕ | n > 0}), p.to_outer_measure.measure_of (A' m)
-- term
--   λ (n m : ↥{n' : ℕ | n' > 0}), p.to_outer_measure.measure_of (A' m)
-- has type
--   ↥{n' : ℕ | n' > 0} → ↥{n : ℕ | n > 0} → ennreal : Type
-- but is expected to have type
--   ?m_1 → ennreal : Type ?
-- state:
-- Ω : Type u,
-- _inst_1 : measurable_space Ω,
-- p : measure Ω,
-- _inst_2 : probability_measure p,
-- X : Ω → ℝ,
-- h : ⇑p {ω : Ω | X ω > 0} > 0,
-- A : set Ω := {ω : Ω | X ω > 0},
-- A' : ↥{n : ℕ | n > 0} → set Ω := λ (n : ↥{n : ℕ | n > 0}), {ω : Ω | X ω > 1 / ↑n},
-- union_to_A : (⋃ (n : ↥{n : ℕ | n > 0}), A' n) = A
-- ⊢ ∃ (δ : ℝ) (H : δ > 0), ⇑p {ω : Ω | X ω ≥ δ} > 0
end


#### Iocta (Aug 29 2020 at 08:29):

the lambda has two parameters n m, but I'm not sure where the n is coming from

#### Kevin Buzzard (Aug 29 2020 at 09:17):

I'm on mobile right now and can't really at this, but isn't it about time you started cutting down on your imports? They make your code about twice as long as it needs to be. You'll only need to import about two things to make this work. You know imports are transitive, right?

#### Iocta (Aug 29 2020 at 09:24):

is there tooling that will warn me about redundant or unused imports, or do I need to do it manually?

#### Kevin Buzzard (Aug 29 2020 at 09:51):

I think you need to do it manually. But to be honest I think doing it manually once will be a good exercise for you, your imports have been growing ever longer over the last few months

Last updated: May 12 2021 at 05:19 UTC