← Mathematical handbook

Proposition 3(vi),(viii): reverse monotonicity and exchangeability

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_one_exchangeable (hb : 1 ∈ Set.Icc (-1) 1) : (leftBoundary 1 hb).IsExchangeable

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_neg_one_exchangeable (hb : -1 ∈ Set.Icc (-1) 1) : (leftBoundary (-1) hb).IsExchangeable

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_transpose_isSI_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).transpose.IsSI ↔ b = 0 ∨ b = 1

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_transpose_isSD_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).transpose.IsSD ↔ b = 0 ∨ b = -1

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_exchangeable_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).IsExchangeable ↔ b = -1 ∨ b = 0 ∨ b = 1