import Mathlib

open MeasureTheory intervalIntegral

namespace UniformCompleteness

/-
Completeness of the maximum for Uniform(0,θ): the analytic core, continuous case.

The crux of proving that X_(n) is a *complete* statistic is the implication

    (∀ θ, ∫₀^θ g(t) t^(n-1) dt = 0)  ⟹  g = 0,

i.e. the only mean-zero function is zero. The genuine mechanism is the
Fundamental Theorem of Calculus: F(θ) = ∫₀^θ h is differentiable with F' = h
at points where h is continuous, and if F ≡ 0 then F' ≡ 0, so h ≡ 0.

We formalize this for *continuous* integrands (the honest, FTC-based core).
The full statistical statement requires the a.e. version for merely integrable
g, which is a strictly stronger measure-theoretic result not formalized here.
-/

/-- **Core lemma (FTC form).** If `h` is continuous and all initial-segment
integrals `∫₀^θ h` vanish, then `h` is identically zero. -/
theorem eq_zero_of_forall_integral_eq_zero
    (h : ℝ → ℝ) (hc : Continuous h)
    (hvanish : ∀ θ : ℝ, (∫ x in (0:ℝ)..θ, h x) = 0) :
    ∀ θ : ℝ, h θ = 0 := by
  intro b
  -- F u := ∫₀^u h  has derivative h b at b by FTC.
  have hderiv : HasDerivAt (fun u => ∫ x in (0:ℝ)..u, h x) (h b) b :=
    (hc.integral_hasStrictDerivAt 0 b).hasDerivAt
  -- But F is the zero function, hence has derivative 0 at b.
  have hF0 : (fun u => ∫ x in (0:ℝ)..u, h x) = fun _ => (0:ℝ) := by
    funext u; exact hvanish u
  have hderiv0 : HasDerivAt (fun u => ∫ x in (0:ℝ)..u, h x) 0 b := by
    rw [hF0]; exact hasDerivAt_const b 0
  -- Uniqueness of the derivative forces h b = 0.
  exact (hderiv.unique hderiv0)

/-- **Completeness for continuous `g`.** If `g` is continuous and, for every
`θ > 0`, the (max-density) mean `∫₀^θ g(t) · (m+1) t^m / θ^(m+1) dt` vanishes,
then `g` vanishes on `(0,∞)`. This is the Lehmann–Scheffé completeness
condition for the family of Uniform(0,θ) maxima, restricted to continuous `g`. -/
theorem completeness_continuous
    (m : ℕ) (g : ℝ → ℝ) (hg : Continuous g)
    (hmean : ∀ θ : ℝ, 0 < θ → (∫ t in (0:ℝ)..θ, g t * ((m + 1) * t ^ m / θ ^ (m + 1))) = 0) :
    ∀ θ : ℝ, 0 < θ → g θ = 0 := by
  -- Strip the positive constant (m+1)/θ^(m+1): the integral of g(t) t^m over [0,θ] vanishes.
  have hstrip : ∀ θ : ℝ, 0 < θ → (∫ t in (0:ℝ)..θ, g t * t ^ m) = 0 := by
    intro θ hθ
    have hθn : θ ^ (m + 1) ≠ 0 := pow_ne_zero _ (ne_of_gt hθ)
    have hconst : (∫ t in (0:ℝ)..θ, ((m + 1) / θ ^ (m + 1)) * (g t * t ^ m))
        = ((m + 1) / θ ^ (m + 1)) * ∫ t in (0:ℝ)..θ, g t * t ^ m :=
      intervalIntegral.integral_const_mul _ _
    have hrw : (fun t => g t * ((m + 1) * t ^ m / θ ^ (m + 1)))
        = (fun t => ((m + 1) / θ ^ (m + 1)) * (g t * t ^ m)) := by
      funext t; ring
    have h0 := hmean θ hθ
    rw [hrw] at h0
    rw [hconst] at h0
    have hcne : ((m : ℝ) + 1) / θ ^ (m + 1) ≠ 0 := by
      apply div_ne_zero _ hθn
      positivity
    exact (mul_eq_zero.mp h0).resolve_left hcne
  -- Now h(t) = g(t) t^m is continuous and has vanishing initial integrals on (0,∞).
  have hcont : Continuous (fun t => g t * t ^ m) := hg.mul (continuous_pow m)
  intro θ hθ
  -- FTC: F u = ∫₀^u (g·x^m) has derivative g(θ)·θ^m at θ.
  have hderiv : HasDerivAt (fun u => ∫ x in (0:ℝ)..u, g x * x ^ m)
      ((g θ) * θ ^ m) θ :=
    (hcont.integral_hasStrictDerivAt 0 θ).hasDerivAt
  -- F is 0 on the open neighborhood (0,∞) of θ, so its derivative there is 0.
  have hloc : (fun u => ∫ x in (0:ℝ)..u, g x * x ^ m) =ᶠ[nhds θ] (fun _ => (0:ℝ)) := by
    have hopen : Set.Ioi (0:ℝ) ∈ nhds θ := Ioi_mem_nhds hθ
    filter_upwards [hopen] with u hu
    exact hstrip u hu
  have hderiv0 : HasDerivAt (fun u => ∫ x in (0:ℝ)..u, g x * x ^ m) 0 θ :=
    (hasDerivAt_const θ (0:ℝ)).congr_of_eventuallyEq hloc
  have hzero : g θ * θ ^ m = 0 := hderiv.unique hderiv0
  have hθm : θ ^ m ≠ 0 := pow_ne_zero _ (ne_of_gt hθ)
  exact (mul_eq_zero.mp hzero).resolve_right hθm

end UniformCompleteness