English
Definition of gammaPDFReal(a,r,x) as the nonnegative real-valued density piece: if x ≥ 0 then r^a/(Γ(a)) x^{a−1} e^{−r x} else 0.
Русский
Определение gammaPDFReal(a,r,x): если x ≥ 0, то (r^a/Γ(a)) x^{a−1} e^{−r x}, иначе 0.
LaTeX
$$\\operatorname{gammaPDFReal}(a,r,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`, in which we will replace
the assumption `IsProbabilityMeasure μ` by the weaker `IsFiniteMeasure μ`. -/
theorem exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure [IsProbabilityMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) :
∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ := by
-- If there exists `a > 0` such that `2⁻¹ < μ {x | ‖x‖ ≤ a} < 1`, we can call the previous lemma.
by_cases h_meas_Ioo : ∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
· obtain ⟨a, ha_pos, ha_gt, ha_lt⟩ : ∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1 := h_meas_Ioo
exact exists_integrable_exp_sq_of_map_rotation_eq_self' h_rot ha_pos ha_gt ha_lt
obtain ⟨b, hb⟩ : ∃ b, μ {x | ‖x‖ ≤ b} = 1 := by
by_contra h_ne
push_neg at h_meas_Ioo h_ne
suffices μ .univ ≤ 2⁻¹ by simp at this
have h_le a : μ {x | ‖x‖ ≤ a} ≤ 2⁻¹ :=
by
have h_of_pos a' (ha : 0 < a') : μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹ :=
by
by_contra h_lt
refine h_ne a' ?_
exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))
rcases le_or_gt a 0 with ha | ha
·
calc
μ {x | ‖x‖ ≤ a}
_ ≤ μ {x | ‖x‖ ≤ 1} := (measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity)))
_ ≤ 2⁻¹ := h_of_pos _ (by positivity)
· exact h_of_pos a ha
have h_univ : (Set.univ : Set E) = ⋃ a : ℕ, {x | ‖x‖ ≤ a} :=
by
ext x
simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_setOf_eq, true_iff]
exact exists_nat_ge _
rw [h_univ, Monotone.measure_iUnion]
· simp [h_le]
· intro a b hab x hx
simp only [Set.mem_setOf_eq] at hx ⊢
exact
hx.trans
(mod_cast hab)
-- So we can take `C = 1` and show that `x ↦ exp (‖x‖ ^ 2)` is integrable, since it is bounded.
have hb' : ∀ᵐ x ∂μ, ‖x‖ ≤ b := by
rwa [ae_iff_prob_eq_one]
refine measurable_to_prop ?_
rw [show (fun x : E ↦ ‖x‖ ≤ b) ⁻¹' { True } = {x : E | ‖x‖ ≤ b} by ext; simp]
exact measurableSet_le (by fun_prop) (by fun_prop)
refine ⟨1, by positivity, ?_⟩
refine
integrable_of_le_of_le (g₁ := 0) (g₂ := fun _ ↦ rexp (b ^ 2)) (by fun_prop) ?_ ?_ (integrable_const _)
(integrable_const _)
· exact ae_of_all _ fun _ ↦ by positivity
· filter_upwards [hb'] with x hx
simp only [one_mul]
gcongr
