Zulip Chat Archive

Stream: new members

Topic: union of unindexed sets


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

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

view this post on Zulip Kenny Lau (Aug 27 2020 at 21:01):

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

view this post on Zulip Kenny Lau (Aug 27 2020 at 21:02):

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

view this post on Zulip Kenny Lau (Aug 27 2020 at 21:03):

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

view this post on Zulip Kenny Lau (Aug 27 2020 at 21:03):

there is no set.Union

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

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

view this post on Zulip Iocta (Aug 27 2020 at 21:15):

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

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

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

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

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

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