Conditional calibration of augmented two-point products

The finite combinatorial theorem is isolated as a reusable proposition. Once it is available (including boundary values γᵢ = 0), the actual conditional product law selected by any admissible augmented latent vector inherits the same rejection bound.

def Feige.TwoPointRejectionBound : Prop

The finite two-point rejection estimate needed by the mixture argument, including the closed boundary 0 ≤ γᵢ ≤ 1.

Equations

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

theorem Feige.augmentedConditionalProduct_rejection_le (htwo : TwoPointRejectionBound) {n : ℕ} (p : Fin n → AugmentedTwoPointParams) (hp : AugmentedParamsNonnegative p) {α : ℝ} (hα : 0 ≤ α) : (augmentedConditionalProduct p).real {y : Fin n → ℝ | dirichletK y ≤ α} ≤ α

Pointwise calibration of the ordinary product law associated with an admissible augmented parameter vector.

theorem Feige.recursiveAugmentedKernel_rejection_le (htwo : TwoPointRejectionBound) {n : ℕ} (p : Fin n → AugmentedTwoPointParams) (hp : AugmentedParamsNonnegative p) {α : ℝ} (hα : 0 ≤ α) : ((recursiveAugmentedKernel n) p).real {y : Fin n → ℝ | dirichletK y ≤ α} ≤ α

The recursively measurable conditional kernel has the same pointwise rejection estimate.