Moment bound for an inverse 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.HMT2011.InvChisqMoment

/-- HMT's notation `𝔼^q(X) = (𝔼 |X|^q)^{1/q}`, the `q`-th moment norm of a real
random variable `X` under the probability measure `P`. The exponent `q` is real,
because HMT apply this notation at non-integer `q` (e.g. `q = (k-1)/2` for even `k`).
The attached proof of lem:inv-chisq-moment writes
`𝔼^q(Ξ⁻¹) = [Γ(k/2-q) / (2^q Γ(k/2))]^{1/q}`. That is exactly
`(𝔼 Ξ^{-q})^{1/q}` for a `χ²_k` variate, which confirms this reading. -/
noncomputable def momentQ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (q : ℝ) (X : Ω → ℝ) : ℝ :=
  (∫ ω, |X ω| ^ q ∂P) ^ (1 / q)

/-- HMT (lem:inv-chisq-moment). Let `Ξ` be a `χ²` variate with `k` degrees of
freedom, where `k ≥ 5`. When `2 ≤ q ≤ (k-1)/2`, `𝔼^q(Ξ⁻¹) < 3/k`.

Realization notes:
* The `χ²_k` law is the Gamma law with shape `k/2` and rate `1/2`
  (`ProbabilityTheory.gammaMeasure (k/2) (1/2)`), with density
  `x^{k/2-1} e^{-x/2} / (2^{k/2} Γ(k/2))` on `x ≥ 0`. Under this law
  `𝔼 Ξ^{-q} = Γ(k/2-q) / (2^q Γ(k/2))`, matching the identity used in the source proof.
* `q` ranges over the reals in `[2, (k-1)/2]`. The source proof treats the endpoint
  `q = (k-1)/2`, a half-integer when `k` is even, and reaches smaller `q` by Hölder.
* `Ξ > 0` almost surely, so the Lean convention `0⁻¹ = 0` affects only a null set.
  Because `q < k/2`, the moment `𝔼 Ξ^{-q}` is finite. -/
theorem inv_chisq_moment
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (k : ℕ) (hk : 5 ≤ k)
    (Ξ : Ω → ℝ)
    (hΞ : ProbabilityTheory.HasLaw Ξ
      (ProbabilityTheory.gammaMeasure ((k : ℝ) / 2) (1 / 2)) P)
    (q : ℝ) (hq2 : 2 ≤ q) (hqk : q ≤ ((k : ℝ) - 1) / 2) :
    momentQ P q (fun ω => (Ξ ω)⁻¹) < 3 / (k : ℝ) := by
  sorry

end RNLAPhaseB.HMT2011.InvChisqMoment