Moment bound for a chi-square variable

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.HMT2011ChisqMoment

/-- The source's `L_q` norm of a random variable `Z`:
`E^q(Z) = (E |Z|^q)^{1/q}`, for `q ≥ 1`. It is written with the lower Lebesgue integral
in `ℝ≥0∞`, so the value is the genuine (possibly infinite) `L_q` norm and not a junk
value of a Bochner integral for a non-integrable function. -/
noncomputable def LqNorm {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (Z : Ω → ℝ) (q : ℝ) : ℝ≥0∞ :=
  (∫⁻ ω, ENNReal.ofReal |Z ω| ^ q ∂P) ^ (1 / q)

/-- HMT 2011, Lemma (lem:chisq-moment): let `Ξ` be a `χ²` variate with `k` degrees of
freedom. For `q ≥ 1`, `E^q(Ξ) ≤ k + q`.

The `χ²` law with `k` degrees of freedom is realized as the Gamma law with shape `k/2`
and rate `1/2`. -/
theorem chisq_moment
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (k : ℕ) (Ξ : Ω → ℝ)
    (hΞ : ProbabilityTheory.HasLaw Ξ
      (ProbabilityTheory.gammaMeasure ((k : ℝ) / 2) (1 / 2)) P)
    (q : ℝ) (hq : 1 ≤ q) :
    LqNorm P Ξ q ≤ ENNReal.ofReal ((k : ℝ) + q) := by
  sorry

end RNLAPhaseB.HMT2011ChisqMoment