Support of the augmented latent parameterization

theorem Feige.measurableSet_augmentedParamNonnegative : MeasurableSet {p : AugmentedTwoPointParams | AugmentedParamNonnegative p}

theorem Feige.measurableSet_augmentedParamsNonnegative (n : ℕ) : MeasurableSet {p : Fin n → AugmentedTwoPointParams | AugmentedParamsNonnegative p}

theorem Feige.ae_latentPair_first_nonnegative {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ] (hsupport : μ (Set.Iio 0) = 0) (M : ℝ) : ∀ᵐ (p : ℝ × ℝ) ∂latentPairMeasure μ M, 0 ≤ p.1

theorem Feige.ae_latentParams_nonnegative {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ] (hsupport : μ (Set.Iio 0) = 0) (M : ℝ) : ∀ᵐ (q : TwoPointParams) ∂latentParamsMeasure μ M, 0 ≤ (↑q).1 ∧ 1 < (↑q).2

theorem Feige.ae_augmentedLatent_nonnegative {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ] (hsupport : μ (Set.Iio 0) = 0) : ∀ᵐ (p : AugmentedTwoPointParams) ∂meanOneAugmentedLatent μ, AugmentedParamNonnegative p

theorem Feige.ae_recursiveAugmentedLatent_nonnegative (n : ℕ) (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (hμ : ∀ (i : Fin n), MeasureTheory.Integrable (fun (x : ℝ) => x) (μ i)) (hmean : ∀ (i : Fin n), ∫ (x : ℝ), x ∂μ i = 1) (hsupport : ∀ (i : Fin n), (μ i) (Set.Iio 0) = 0) : ∀ᵐ (p : Fin n → AugmentedTwoPointParams) ∂recursiveAugmentedLatent n fun (i : Fin n) => meanOneAugmentedLatent (μ i), AugmentedParamsNonnegative p