CommunicationComplexity.FiniteProbabilitySpace

source

noncomputable def PMF.toProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] (p : PMF Ω) :

MeasureTheory.ProbabilityMeasure Ω

Bundle the measure associated to a PMF as a probability measure.

Equations

p.toProbabilityMeasure = ⟨p.toMeasure, ⋯⟩

Instances For

source

@[simp]

theorem PMF.coe_toProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] (p : PMF Ω) :

↑p.toProbabilityMeasure = p.toMeasure

source

class CommunicationComplexity.FiniteMeasureSpace (Ω : Type u_1) [MeasurableSpace Ω] :

Type u_1

A finite measurable space: the type is finite and the measurable structure is discrete. This deliberately does not include a measure.

fintype : Fintype Ω
discrete : DiscreteMeasurableSpace Ω

Instances

source

def CommunicationComplexity.FiniteMeasureSpace.of (Ω : Type u_1) [MeasurableSpace Ω] [Fintype Ω] [DiscreteMeasurableSpace Ω] :

FiniteMeasureSpace Ω

Helper for bundling already-existing finite measurable-space instances locally.

Equations

CommunicationComplexity.FiniteMeasureSpace.of Ω = { fintype := inferInstance, discrete := ⋯ }

Instances For

source

class CommunicationComplexity.FiniteProbabilitySpace (Ω : Type u_1) :

Type u_1

toMeasureSpace : MeasureTheory.MeasureSpace Ω
finite : FiniteMeasureSpace Ω
prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

Instances

source

def CommunicationComplexity.FiniteProbabilitySpace.of (Ω : Type u_1) [m : MeasureTheory.MeasureSpace Ω] [Fintype Ω] [DiscreteMeasurableSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] :

FiniteProbabilitySpace Ω

Helper for bundling already-existing instances locally.

Equations

CommunicationComplexity.FiniteProbabilitySpace.of Ω = { toMeasureSpace := m, finite := CommunicationComplexity.FiniteMeasureSpace.of Ω, prob := ⋯ }

Instances For

source

noncomputable def CommunicationComplexity.FiniteProbabilitySpace.ofProbabilityMeasure (Ω : Type u_1) [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) :

FiniteProbabilitySpace Ω

Build a finite probability space from a finite measurable space and a probability measure.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CommunicationComplexity.FiniteMeasureSpace.measureReal_eq_sum_singletons {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (S : Set Ω) :

μ.real S = ∑ ω : Ω, if ω ∈ S then μ.real {ω} else 0

A finite measure on a finite measurable space is determined by its singleton masses.

source

theorem CommunicationComplexity.FiniteMeasureSpace.probabilityMeasure_measureReal_eq_sum_singletons {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (S : Set Ω) :

(↑μ).real S = ∑ ω : Ω, if ω ∈ S then (↑μ).real {ω} else 0

A probability measure on a finite measurable space is determined by its singleton masses.

source

theorem CommunicationComplexity.FiniteMeasureSpace.measureReal_preimage_eq_sum_fibers {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] [Fintype α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Z : Ω → α) (P : α → Prop) :

μ.real {ω : Ω | P (Z ω)} = ∑ z : α, if P z then μ.real (Z ⁻¹' {z}) else 0

On a finite measurable space, the real measure of a preimage event is the sum of the real masses of the fibers that imply the event.

source

theorem CommunicationComplexity.FiniteMeasureSpace.probabilityMeasure_measureReal_preimage_eq_sum_fibers {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] [Fintype α] (μ : MeasureTheory.ProbabilityMeasure Ω) (Z : Ω → α) (P : α → Prop) :

(↑μ).real {ω : Ω | P (Z ω)} = ∑ z : α, if P z then (↑μ).real (Z ⁻¹' {z}) else 0

On a finite measurable space, the real measure of a preimage event is the sum of the real masses of the fibers that imply the event.

source

theorem CommunicationComplexity.FiniteMeasureSpace.absolutelyContinuous_iff_forall_singletons {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] {μ ν : MeasureTheory.Measure Ω} :

μ.AbsolutelyContinuous ν ↔ ∀ (ω : Ω), ν {ω} = 0 → μ {ω} = 0

On a finite measurable space, absolute continuity is equivalent to absolute continuity on singleton masses.

source

theorem CommunicationComplexity.FiniteMeasureSpace.probabilityMeasure_sq_integral_le_integral_sq {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (f : Ω → ℝ) :

(∫ (ω : Ω), f ω ∂↑μ) ^ 2 ≤ ∫ (ω : Ω), f ω ^ 2 ∂↑μ

For any probability measure on a finite measurable space, the square of an expectation is bounded by the expectation of the square.

source

theorem CommunicationComplexity.FiniteMeasureSpace.integral_comp_eq_sum_measureReal_fibers {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] [MeasurableSpace α] [DiscreteMeasurableSpace α] [Fintype α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Z : Ω → α) (f : α → ℝ) :

∫ (ω : Ω), f (Z ω) ∂μ = ∑ z : α, μ.real (Z ⁻¹' {z}) * f z

On a finite measurable space, the integral of a function of a finite-valued random variable is the sum over its fibers.

source

theorem CommunicationComplexity.FiniteMeasureSpace.measureReal_eq_sum_cond_fiber_real {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] [MeasurableSpace α] [DiscreteMeasurableSpace α] [Fintype α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Z : Ω → α) (S : Set Ω) :

μ.real S = ∑ z : α, μ.real (Z ⁻¹' {z}) * μ[|Z ⁻¹' {z}].real S

Law of total probability over the fibers of a finite-valued random variable, in real-valued measure form.

source

instance CommunicationComplexity.finiteMeasureSpaceBool :

FiniteMeasureSpace Bool

Equations

CommunicationComplexity.finiteMeasureSpaceBool = CommunicationComplexity.FiniteMeasureSpace.of Bool

source

noncomputable instance CommunicationComplexity.finiteMeasureSpaceProd (Ω₁ : Type u_1) (Ω₂ : Type u_2) [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [FiniteMeasureSpace Ω₁] [FiniteMeasureSpace Ω₂] :

FiniteMeasureSpace (Ω₁ × Ω₂)

Equations

CommunicationComplexity.finiteMeasureSpaceProd Ω₁ Ω₂ = CommunicationComplexity.FiniteMeasureSpace.of (Ω₁ × Ω₂)

source

noncomputable instance CommunicationComplexity.finiteMeasureSpacePi {ι : Type u_1} [Fintype ι] (Ω : ι → Type u_2) [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → FiniteMeasureSpace (Ω i)] :

FiniteMeasureSpace ((i : ι) → Ω i)

Equations

CommunicationComplexity.finiteMeasureSpacePi Ω = CommunicationComplexity.FiniteMeasureSpace.of ((i : ι) → Ω i)

source

noncomputable instance CommunicationComplexity.instProd (Ω₁ : Type u_1) (Ω₂ : Type u_2) [FiniteProbabilitySpace Ω₁] [FiniteProbabilitySpace Ω₂] :

FiniteProbabilitySpace (Ω₁ × Ω₂)

Equations

CommunicationComplexity.instProd Ω₁ Ω₂ = CommunicationComplexity.FiniteProbabilitySpace.of (Ω₁ × Ω₂)

source

noncomputable instance CommunicationComplexity.instPi {ι : Type u_1} [Fintype ι] (Ω : ι → Type u_2) [(i : ι) → FiniteProbabilitySpace (Ω i)] :

FiniteProbabilitySpace ((i : ι) → Ω i)

Equations

CommunicationComplexity.instPi Ω = CommunicationComplexity.FiniteProbabilitySpace.of ((i : ι) → Ω i)

source

theorem CommunicationComplexity.uniformOn_univ_measureReal_eq_card_filter {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (S : Set Ω) :

((ProbabilityTheory.uniformOn Set.univ) S).toReal = ↑{ω : Ω | ω ∈ S}.card / ↑(Fintype.card Ω)

On a finite discrete type with the uniform measure on Set.univ, the real-valued measure of a set is its cardinality divided by the size of the ambient type.

source

theorem CommunicationComplexity.uniformOn_univ_measureReal_eq_card_subtype {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (S : Set Ω) [Fintype { ω : Ω // ω ∈ S }] :

((ProbabilityTheory.uniformOn Set.univ) S).toReal = ↑(Fintype.card { ω : Ω // ω ∈ S }) / ↑(Fintype.card Ω)

On a finite discrete type with the uniform measure on Set.univ, the real-valued measure of a set is the cardinality of the corresponding subtype divided by the size of the ambient type.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.nonempty {Ω : Type u_1} [FiniteProbabilitySpace Ω] :

Nonempty Ω

You usually won't need this theorem explicitly, because of the instance below.

source

@[instance 100]

instance CommunicationComplexity.FiniteProbabilitySpace.instNonempty (Ω : Type u_1) [FiniteProbabilitySpace Ω] :

Nonempty Ω

source

def CommunicationComplexity.FiniteProbabilitySpace.toPMF (Ω : Type u_1) [FiniteProbabilitySpace Ω] :

PMF Ω

Equations

CommunicationComplexity.FiniteProbabilitySpace.toPMF Ω = MeasureTheory.volume.toPMF

Instances For

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measure_eq {Ω : Type u_1} [FiniteProbabilitySpace Ω] (S : Set Ω) :

MeasureTheory.volume S = ∑ ω : ↑S, (toPMF Ω) ↑ω

source

theorem CommunicationComplexity.FiniteProbabilitySpace.hasSum_measure_singletons {Ω : Type u_1} {α : Type u_2} [FiniteProbabilitySpace Ω] [Finite α] (e : Ω ≃ α) :

HasSum (fun (a : α) => MeasureTheory.volume {e.symm a}) 1

The singleton masses of a finite probability space sum to 1 along any finite enumeration.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.pmf_prod {Ω₁ : Type u_1} {Ω₂ : Type u_2} [FiniteProbabilitySpace Ω₁] [FiniteProbabilitySpace Ω₂] (x : Ω₁) (y : Ω₂) :

(toPMF (Ω₁ × Ω₂)) (x, y) = (toPMF Ω₁) x * (toPMF Ω₂) y

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_prod {Ω₁ : Type u_1} {Ω₂ : Type u_2} [FiniteProbabilitySpace Ω₁] [FiniteProbabilitySpace Ω₂] (A : Set Ω₁) (B : Set Ω₂) :

MeasureTheory.volume.real (A ×ˢ B) = MeasureTheory.volume.real A * MeasureTheory.volume.real B

The real-valued measure of a measurable rectangle in a product finite probability space factors as the product of the two measures.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_iUnion_fintype {Ω : Type u_1} {ι : Type u_2} [FiniteProbabilitySpace Ω] [Fintype ι] (A : ι → Set Ω) (hdisj : Pairwise fun (i j : ι) => Disjoint (A i) (A j)) :

MeasureTheory.volume.real (⋃ (i : ι), A i) = ∑ i : ι, MeasureTheory.volume.real (A i)

The real-valued measure of a finite disjoint union is the sum of the real-valued measures of its parts.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_preimage_finset {Ξ : Type u_1} {Ω : Type u_2} [FiniteProbabilitySpace Ξ] [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (φ : Ξ → Ω) (T : Finset Ω) :

MeasureTheory.volume.real (φ ⁻¹' ↑T) = ∑ a ∈ T, MeasureTheory.volume.real (φ ⁻¹' {a})

The real-valued measure of the preimage of a finite set splits as a sum over singleton fibers.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_finset {Ω : Type u_1} [FiniteProbabilitySpace Ω] (T : Finset Ω) :

MeasureTheory.volume.real ↑T = ∑ a ∈ T, MeasureTheory.volume.real {a}

The real-valued measure of a finite set splits as a sum over its singleton parts.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.integral_eq_pmf_sum {Ω : Type u_1} [FiniteProbabilitySpace Ω] (f : Ω → ℝ) :

∫ (ω : Ω), f ω = ∑ ω : Ω, ((toPMF Ω) ω).toReal * f ω

On a finite probability space, integrating a real-valued function is a finite weighted sum.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.sq_integral_le_integral_sq {Ω : Type u_1} [FiniteProbabilitySpace Ω] (f : Ω → ℝ) :

(∫ (ω : Ω), f ω) ^ 2 ≤ ∫ (ω : Ω), f ω ^ 2

On a finite probability space, the square of an expectation is bounded by the expectation of the square.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.integral_comp_eval {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [FiniteProbabilitySpace Ω] (i : ι) (f : Ω → ℝ) :

∫ (ωs : ι → Ω), f (ωs i) = ∫ (ω : Ω), f ω

Integrating a function over a coordinate of a finite product space is the same as integrating it over the original finite probability space.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_pi_univ {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} [(i : ι) → FiniteProbabilitySpace (Ω i)] (s : (i : ι) → Set (Ω i)) :

MeasureTheory.volume.real (Set.univ.pi s) = ∏ i : ι, MeasureTheory.volume.real (s i)

The real-valued measure of a cylinder set in a finite product probability space is the product of the real-valued measures of its coordinate slices.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_eq_integral_indicator_one {Ω : Type u_1} [FiniteProbabilitySpace Ω] (S : Set Ω) :

MeasureTheory.volume.real S = ∫ (ω : Ω), S.indicator 1 ω

The real-valued measure of a set is the integral of its indicator.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_eq_integral_indicator {Ω : Type u_1} [FiniteProbabilitySpace Ω] (S : Set Ω) :

MeasureTheory.volume.real S = ∫ (ω : Ω), if ω ∈ S then 1 else 0

The real-valued measure of a set is the integral of the corresponding 0/1 function.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.pmf_toReal_sum_eq_one {Ω : Type u_1} [FiniteProbabilitySpace Ω] :

∑ ω : Ω, ((toPMF Ω) ω).toReal = 1

The weights of a finite probability space sum to 1.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.pmf_toReal_nonneg {Ω : Type u_1} [FiniteProbabilitySpace Ω] (ω : Ω) :

0 ≤ ((toPMF Ω) ω).toReal

Each weight in a finite probability space is nonnegative.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.exists_pmf_toReal_pos {Ω : Type u_1} [FiniteProbabilitySpace Ω] :

∃ (ω : Ω), 0 < ((toPMF Ω) ω).toReal

Some point in a finite probability space has positive probability mass.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.integral_le_of_le {Ω : Type u_1} [FiniteProbabilitySpace Ω] {f : Ω → ℝ} {c : ℝ} (hf : ∀ (ω : Ω), f ω ≤ c) :

∫ (ω : Ω), f ω ≤ c

If f(x) ≤ c everywhere under a probability measure, then ∫ f ≤ c.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.measureReal_ge_le_integral_div {Ω : Type u_1} [FiniteProbabilitySpace Ω] {f : Ω → ℝ} {ε : ℝ} (hf_nonneg : ∀ (ω : Ω), 0 ≤ f ω) (hε : 0 < ε) :

MeasureTheory.volume.real {ω : Ω | ε ≤ f ω} ≤ (∫ (ω : Ω), f ω) / ε

Markov's inequality for nonnegative functions on a finite probability space.

source

theorem CommunicationComplexity.FiniteProbabilitySpace.lt_integral_of_lt {Ω : Type u_1} [FiniteProbabilitySpace Ω] {f : Ω → ℝ} {c : ℝ} (hf : ∀ (ω : Ω), c < f ω) :

c < ∫ (ω : Ω), f ω

If f(x) > c everywhere under a probability measure on a nonempty type, then ∫ f > c.