Product laws for two-point random variables

noncomputable def Feige.boolHighMeasure (p : ℝ) : MeasureTheory.Measure Bool

The Bernoulli law assigning mass p to true.

Equations

• Feige.boolHighMeasure p = ENNReal.ofReal (1 - p) • MeasureTheory.Measure.dirac false + ENNReal.ofReal p • MeasureTheory.Measure.dirac true

theorem Feige.boolHighMeasure_isProbability {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : MeasureTheory.IsProbabilityMeasure (boolHighMeasure p)

def Feige.boolHighSet {m : ℕ} (ω : Fin m → Bool) : Finset (Fin m)

The coordinates at which a Boolean vector takes the high value.

Equations

• Feige.boolHighSet ω = {i : Fin m | ω i = true}

theorem Feige.measurable_boolHighSet {m : ℕ} : Measurable boolHighSet

theorem Feige.boolHighSet_injective {m : ℕ} : Function.Injective boolHighSet

theorem Feige.boolHighSet_surjective {m : ℕ} : Function.Surjective boolHighSet

theorem Feige.boolHighMeasure_singleton (p : ℝ) (b : Bool) : (boolHighMeasure p) {b} = ENNReal.ofReal (if b = true then p else 1 - p)

theorem Feige.map_boolHighSet_pi_eq_highSetMeasure {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) : MeasureTheory.Measure.map boolHighSet (MeasureTheory.Measure.pi fun (i : Fin m) => boolHighMeasure (p i)) = highSetMeasure p hp0 hp1

theorem Feige.map_boolHighMeasure_twoPoint {γ β : ℝ} (hγ : 0 ≤ γ) (hβ : 0 < β) : MeasureTheory.Measure.map (fun (b : Bool) => if b = true then highValue β else lowValue γ) (boolHighMeasure (highProbability γ β)) = twoPointMeasure (lowValue γ) (highValue β)

theorem Feige.map_canonicalTwoPointPiVector {m : ℕ} (γ β : Fin m → ℝ) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 < β i) : MeasureTheory.Measure.map (canonicalTwoPointPiVector γ β) (MeasureTheory.Measure.pi fun (i : Fin m) => boolHighMeasure (twoPointHighProbability γ β i)) = MeasureTheory.Measure.pi fun (i : Fin m) => twoPointMeasure (lowValue (γ i)) (highValue (β i))

theorem Feige.measurableSet_dirichletK_le {m : ℕ} (α : ℝ) : MeasurableSet {y : Fin m → ℝ | dirichletK y ≤ α}

theorem Feige.twoPointProductLaw_rejection {m : ℕ} (γ β : Fin m → ℝ) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 < β i) (α : ℝ) : (MeasureTheory.Measure.pi fun (i : Fin m) => twoPointMeasure (lowValue (γ i)) (highValue (β i))).real {y : Fin m → ℝ | dirichletK y ≤ α} = twoPointRejectionMass γ β α