-- Mathlib/Probability/Distributions/Gamma.lean
/-- The pdf of the gamma distribution integrates to 1 -/
@[simp]
lemma lintegral_gammaPDF_eq_one {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫⁻ x, gammaPDF a r x = 1

Proof state:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
⊢ gammaPDFReal a r x = (fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x

Tactic:
simp_rw [gammaPDFReal, eq_true_intro hx, ite_true]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0

Tactic:
rw [setLIntegral_congr_fun measurableSet_Iio
  (ae_of_all _ (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx)), lintegral_zero]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫ (a_1 : ℝ) in Ioi 0, r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))) = 1

Tactic:
rw [integral_mul_left, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
  ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
  div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1

Tactic:
have leftSide : ∫⁻ x in Iio 0, gammaPDF a r x = 0 := by
  rw [setLIntegral_congr_fun measurableSet_Iio
    (ae_of_all _ (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx)), lintegral_zero]

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
⊢ 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity

Result:
no goals

Proof state:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ gammaPDFReal a r =ᶠ[ae (ℙ.restrict (Ici 0))] fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : 0 ≤ x) ↦ ?_

Result:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
⊢ gammaPDFReal a r x = (fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1

Tactic:
have rightSide : ∫⁻ x in Ici 0, gammaPDF a r x =
    ∫⁻ x in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * exp (-(r * x))) :=
  setLIntegral_congr_fun measurableSet_Ici (ae_of_all _ (fun _ ↦ gammaPDF_of_nonneg))

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1

Proof state:
case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∀ᵐ (x : ℝ), x ∈ Ici 0 → 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
exact ae_of_all _ (fun x (hx : 0 ≤ x) ↦ by positivity)

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫ (a_1 : ℝ) in Ici 0, r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)) = 1

Tactic:
simp_rw [integral_Ici_eq_integral_Ioi, mul_assoc]

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫ (a_1 : ℝ) in Ioi 0, r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))) = 1

Proof state:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (ℙ.restrict (Ici 0))

Tactic:
apply (measurable_gammaPDFReal a r).aestronglyMeasurable.congr

Result:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ gammaPDFReal a r =ᶠ[ae (ℙ.restrict (Ici 0))] fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1

Tactic:
rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
  leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫ (a_1 : ℝ) in Ici 0, r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)) = 1

case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Ici 0))] fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (ℙ.restrict (Ici 0))

Proof state:
case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Ici 0))] fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]

Result:
case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∀ᵐ (x : ℝ), x ∈ Ici 0 → 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))