English
The gammaPDFReal formula for f as piecewise function: if x ≥ 0 then f(x) = r^a/Γ(a) · x^{a-1} e^{-(r x)} else 0.
Русский
Гамма-плотность: для x ≥ 0 имеет вид f(x) = r^a/Γ(a) · x^{a-1} e^{-(r x)}, иначе f(x) = 0.
LaTeX
$$γ_{a,r}^{Real}(x) = \\begin{cases} \\frac{r^a}{\\Gamma(a)} x^{a-1} e^{-r x}, & x \\ge 0 \\\\ 0, & x<0 \\end{cases}$$
Lean4
/-- Auxiliary lemma for `exists_integrable_exp_sq_of_map_rotation_eq_self`.
The assumptions on `a` and `μ {x | ‖x‖ ≤ a}` are not needed and will be removed in that more
general theorem. -/
theorem exists_integrable_exp_sq_of_map_rotation_eq_self' [IsProbabilityMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) {a : ℝ} (ha_pos : 0 < a)
(ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}) (ha_lt : μ {x | ‖x‖ ≤ a} < 1) :
∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ :=
by
let c := μ {x | ‖x‖ ≤ a}
replace hc_lt : c < 1 := ha_lt
have hc_lt_top : c < ∞ := measure_lt_top _ _
have hc_one_sub_lt_top : 1 - c < ∞ := lt_top_of_lt (b := 2) (tsub_le_self.trans_lt (by simp))
have h_one_sub_lt_self : 1 - c < c :=
by
refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_
rw [← two_mul]
rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at ha_gt
have h_pos : 0 < logRatio c * a⁻¹ ^ 2 := mul_pos (logRatio_pos ha_gt hc_lt) (by positivity)
refine ⟨logRatio c * a⁻¹ ^ 2, h_pos, ⟨by fun_prop, ?_⟩⟩
simp only [HasFiniteIntegral, ← ofReal_norm_eq_enorm, Real.norm_eq_abs, Real.abs_exp]
-- `⊢ ∫⁻ x, ENNReal.ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ < ∞`
refine (lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self h_rot le_rfl ha_gt).trans_lt ?_
refine ENNReal.add_lt_top.mpr ⟨ENNReal.ofReal_lt_top, ?_⟩
refine
Summable.tsum_ofReal_lt_top <| Real.summable_exp_nat_mul_of_ge ?_ (fun i ↦ mod_cast (Nat.lt_pow_self (by simp)).le)
refine mul_neg_of_neg_of_pos (by simp) (Real.log_pos ?_)
change 1 < (c / (1 - c)).toReal
simp only [ENNReal.toReal_div, one_lt_div_iff, ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, hc_one_sub_lt_top,
and_self, true_and]
rw [ENNReal.toReal_lt_toReal hc_one_sub_lt_top.ne hc_lt_top.ne]
exact .inl h_one_sub_lt_self
