Two-point parameters for augmented latent coordinates

The atom-at-one branch is represented by the harmless degenerate parametrization γ = 0, β = 1. A genuine support pair (x,y) is represented by γ = 1-x, β = y-1.

def Feige.augmentedGamma (p : AugmentedTwoPointParams) : ℝ

The lower displacement encoded by an augmented parameter.

Equations

• Feige.augmentedGamma (Sum.inl val) = 0
• Feige.augmentedGamma (Sum.inr q) = 1 - (↑q).1

def Feige.augmentedBeta (p : AugmentedTwoPointParams) : ℝ

The upper displacement encoded by an augmented parameter.

Equations

• Feige.augmentedBeta (Sum.inl val) = 1
• Feige.augmentedBeta (Sum.inr q) = (↑q).2 - 1

def Feige.AugmentedParamNonnegative (p : AugmentedTwoPointParams) : Prop

The nonnegativity condition on an augmented two-point parameter.

Equations

• Feige.AugmentedParamNonnegative (Sum.inl val) = True
• Feige.AugmentedParamNonnegative (Sum.inr q) = (0 ≤ (↑q).1 ∧ 1 < (↑q).2)

def Feige.AugmentedParamsNonnegative {n : ℕ} (p : Fin n → AugmentedTwoPointParams) : Prop

The condition enjoyed by latent parameters sampled from a nonnegative mean-one law: genuine lower support points are nonnegative and genuine upper support points are strictly above one.

Equations

• Feige.AugmentedParamsNonnegative p = ∀ (i : Fin n), Feige.AugmentedParamNonnegative (p i)

theorem Feige.augmentedGamma_nonneg {n : ℕ} {p : Fin n → AugmentedTwoPointParams} (i : Fin n) : 0 ≤ augmentedGamma (p i)

theorem Feige.augmentedGamma_le_one {n : ℕ} {p : Fin n → AugmentedTwoPointParams} (hp : AugmentedParamsNonnegative p) (i : Fin n) : augmentedGamma (p i) ≤ 1

theorem Feige.augmentedBeta_pos {n : ℕ} {p : Fin n → AugmentedTwoPointParams} (hp : AugmentedParamsNonnegative p) (i : Fin n) : 0 < augmentedBeta (p i)

theorem Feige.augmentedTwoPointKernel_eq_twoPointMeasure (p : AugmentedTwoPointParams) : augmentedTwoPointKernel p = twoPointMeasure (lowValue (augmentedGamma p)) (highValue (augmentedBeta p))

Both branches of the augmented kernel are exactly the canonical mean-one two-point measure for their γ,β parameters.

theorem Feige.augmentedConditionalProduct_eq_twoPointProduct {n : ℕ} (p : Fin n → AugmentedTwoPointParams) : augmentedConditionalProduct p = MeasureTheory.Measure.pi fun (i : Fin n) => twoPointMeasure (lowValue (augmentedGamma (p i))) (highValue (augmentedBeta (p i)))