Reduction from means at most one to means exactly one

This is the final mean-normalization reduction in the proof of Theorem 2.1.

noncomputable def Feige.meanOneNormalize {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} (Y : Fin n → Ω → ℝ) (μ : MeasureTheory.Measure Ω) (i : Fin n) (ω : Ω) : ℝ

Normalize a positive-mean coordinate by its mean; replace a zero-mean coordinate by the constant one.

Equations

• Feige.meanOneNormalize Y μ i ω = if ∫ (ω' : Ω), Y i ω' ∂μ = 0 then 1 else Y i ω / ∫ (ω' : Ω), Y i ω' ∂μ

theorem Feige.meanOneNormalize_measurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) (hY : ∀ (i : Fin n), Measurable (Y i)) (i : Fin n) : Measurable (meanOneNormalize Y μ i)

theorem Feige.meanOneNormalize_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) [MeasureTheory.IsFiniteMeasure μ] (hY : ∀ (i : Fin n), MeasureTheory.Integrable (Y i) μ) (i : Fin n) : MeasureTheory.Integrable (meanOneNormalize Y μ i) μ

theorem Feige.meanOneNormalize_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) (hY : ∀ (i : Fin n) (ω : Ω), 0 ≤ Y i ω) (i : Fin n) (ω : Ω) : 0 ≤ meanOneNormalize Y μ i ω

theorem Feige.meanOneNormalize_mean {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) [MeasureTheory.IsProbabilityMeasure μ] (i : Fin n) : ∫ (ω : Ω), meanOneNormalize Y μ i ω ∂μ = 1

theorem Feige.meanOneNormalize_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) (hYindep : ProbabilityTheory.iIndepFun Y μ) : ProbabilityTheory.iIndepFun (meanOneNormalize Y μ) μ

theorem Feige.ae_le_meanOneNormalize {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) (hYint : ∀ (i : Fin n), MeasureTheory.Integrable (Y i) μ) (hYnonneg : ∀ (i : Fin n) (ω : Ω), 0 ≤ Y i ω) (hYmean : ∀ (i : Fin n), ∫ (ω : Ω), Y i ω ∂μ ≤ 1) : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : Fin n), Y i ω ≤ meanOneNormalize Y μ i ω

theorem Feige.ae_rejection_subset_normalized {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) (hYint : ∀ (i : Fin n), MeasureTheory.Integrable (Y i) μ) (hYnonneg : ∀ (i : Fin n) (ω : Ω), 0 ≤ Y i ω) (hYmean : ∀ (i : Fin n), ∫ (ω : Ω), Y i ω ∂μ ≤ 1) (α : ℝ) : {ω : Ω | (dirichletK fun (i : Fin n) => Y i ω) ≤ α} ≤ᵐ[μ] {ω : Ω | (dirichletK fun (i : Fin n) => meanOneNormalize Y μ i ω) ≤ α}

The rejection event for the original variables is almost-everywhere contained in that for their mean-one normalization.

theorem Feige.rejection_probability_le_normalized {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (Y : Fin n → Ω → ℝ) [MeasureTheory.IsFiniteMeasure μ] (hYint : ∀ (i : Fin n), MeasureTheory.Integrable (Y i) μ) (hYnonneg : ∀ (i : Fin n) (ω : Ω), 0 ≤ Y i ω) (hYmean : ∀ (i : Fin n), ∫ (ω : Ω), Y i ω ∂μ ≤ 1) (α : ℝ) : μ.real {ω : Ω | (dirichletK fun (i : Fin n) => Y i ω) ≤ α} ≤ μ.real {ω : Ω | (dirichletK fun (i : Fin n) => meanOneNormalize Y μ i ω) ≤ α}

Consequently, normalization can only increase the rejection probability.