English
The gammaPDF(a,r,x) denotes the pdf value in ℝ≥0∞ as ENNReal.ofReal(gammaPDFReal(a,r,x)).
Русский
Функция gammaPDF(a,r,x) — это плотность Гамма, равная ENNReal.ofReal(gammaPDFReal(a,r,x)).
LaTeX
$$\\operatorname{gammaPDF}(a,r,x) = \\text{ENNReal}.ofReal\\big(\\operatorname{gammaPDFReal}(a,r,x)\\big)$$
Lean4
/-- **Fernique's theorem** for finite measures whose product is invariant by rotation: there exists
`C > 0` such that the function `x ↦ exp (C * ‖x‖ ^ 2)` is integrable. -/
theorem exists_integrable_exp_sq_of_map_rotation_eq_self [IsFiniteMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) :
∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ :=
by
by_cases hμ_zero : μ = 0
· exact ⟨1, by positivity, by simp [hμ_zero]⟩
let μ' := cond μ .univ
have hμ'_eq : μ' = (μ .univ)⁻¹ • μ := by simp [μ', cond]
have hμ' : IsProbabilityMeasure μ' := cond_isProbabilityMeasure <| by simp [hμ_zero]
have h_rot : (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4))) = μ'.prod μ' := by
calc
(μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4)))
_ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by
simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
_ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot]
_ = μ'.prod μ' := by simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
obtain ⟨C, hC_pos, hC⟩ := exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure (μ := μ') h_rot
refine ⟨C, hC_pos, ?_⟩
rwa [hμ'_eq, integrable_smul_measure] at hC
· simp
· simp [hμ_zero]
