Proposal: general Orlicz ψ_p norms and a unified sub-Gaussian interface

[tukamilano]

I'd like to replace the two Orlicz families in
Moments/Orlicz.lean
with a single ψ_p family, and use it to tidy up the sub-Gaussian side. Mathlib
has no Orlicz norm at the current pin.

Why:

• Lines 57–342 (ψ₂) and 343–588 (ψ₁) are a near line-by-line transcription of
  each other: 3 definitions and 13 lemmas duplicated. SubGaussianOrlicz.lean
  repeats three more pairs.
• Nothing relates the two norms, so "sub-Gaussian implies sub-exponential"
  cannot be stated today.
• ‖c‖_{ψ₂} = |c| / √(log 2) and ‖c‖_{ψ₁} = |c| / log 2 are both
  |c| / (log 2) ^ (1 / p), which only becomes visible with p a parameter.

Proposed definition:

/-- `K` is an admissible `ψ p` scale for `X`: `E[exp ((|X| / K) ^ p)] ≤ 2`. -/
def HasOrliczPsiBound (p : ℝ) (X : Ω → ℝ) (μ : Measure Ω) (K : ℝ) : Prop :=
  0 < K ∧ ∫⁻ ω, ENNReal.ofReal (exp ((|X ω| / K) ^ p)) ∂μ ≤ 2

plus orliczPsiNorm p and HasFiniteOrliczPsiNorm p.