Calibration after latent mixing

This is the measure-theoretic averaging step in the proof of Theorem 2.1. It is kept separate from the construction of the latent law: any probability measure on augmented parameters that is almost surely admissible can be used.

theorem Feige.augmentedMixture_rejection_le (htwo : TwoPointRejectionBound) {n : ℕ} (ν : MeasureTheory.Measure (Fin n → AugmentedTwoPointParams)) [MeasureTheory.IsProbabilityMeasure ν] (hν : ∀ᵐ (p : Fin n → AugmentedTwoPointParams) ∂ν, AugmentedParamsNonnegative p) {α : ℝ} (hα : 0 ≤ α) : (ν.bind ⇑(recursiveAugmentedKernel n)).real {y : Fin n → ℝ | dirichletK y ≤ α} ≤ α

Mixing conditionally calibrated augmented two-point products preserves the rejection bound.