union of unindexed sets

Stream: new members

[Iocta]

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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

there is no set.Union

[Reid Barton]

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

[Iocta]

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]

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

[Iocta]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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