Holder's Theorem for Semigroups

This file containes the proof of Holder's theorem for semigroups and some variants of it.

theorem holder_not_anom {α : Type u} [Semigroup α] [LinearOrder α] [IsOrderedCancelSemigroup α] [Pow α ℕ+] [PNatPowAssoc α] (not_anom : ¬has_anomalous_pair α) : ∃ (G : Subsemigroup (Multiplicative ℝ)), Nonempty (α ≃*o ↥G)

If α is a linear ordered cancel semigroup that does not have anomalous pairs, then α is monoid order isomorphic to a subsemigroup of ℝ.

theorem holder_large_differences {α : Type u} [Semigroup α] [LinearOrder α] [IsOrderedCancelSemigroup α] [Pow α ℕ+] [PNatPowAssoc α] (has_large_diff : has_large_differences) : ∃ (G : Subsemigroup (Multiplicative ℝ)), Nonempty (α ≃*o ↥G)

If α is a linear ordered cancel semigroup that has large differences, then α is monoid order isomorphic to a subsemigroup of ℝ.

theorem holder_sign_arch_differences {α : Type u} [Semigroup α] [LinearOrder α] [IsOrderedCancelSemigroup α] [Pow α ℕ+] [PNatPowAssoc α] (sign : ∀ (x y : α), is_one x ∨ is_one y ∨ same_sign x y) (arch : is_archimedean) (differences : ∀ (x y : α), x < y → ∃ (z : α), x * z = y) : ∃ (G : Subsemigroup (Multiplicative ℝ)), Nonempty (α ≃*o ↥G)

If α is a linear ordered cancel semigroup where all elements are nonnegative or all are nonpositive, α is archimedean, and it has differences (i.e. if x < y then there exists z such that x*z = y), then α is monoid order isomoprhic to a subsemigroup of ℝ.