English
ConvexOn Real (Ioi 0) (log ∘ doublingGamma).
Русский
Выпуклость log ∘ doublingGamma на (0, ∞).
LaTeX
$$$ \text{ConvexOn} \mathbb{R} (\mathrm{Ioi}(0)) (\log \circ \mathrm{doublingGamma}) $$$
Lean4
theorem doublingGamma_log_convex_Ioi : ConvexOn ℝ (Ioi (0 : ℝ)) (log ∘ doublingGamma) :=
by
refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm
· convert convexOn_log_Gamma.comp_affineMap (DistribMulAction.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap using 1
· simpa only [zero_div] using (preimage_const_mul_Ioi (0 : ℝ) one_half_pos).symm
· ext1 x
simp only [LinearMap.coe_toAffineMap, Function.comp_apply, DistribMulAction.toLinearMap_apply]
rw [smul_eq_mul, mul_comm, mul_one_div]
· refine ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)
convert
convexOn_log_Gamma.comp_affineMap
((DistribMulAction.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using
1
· change Ioi (-1 : ℝ) = ((fun x : ℝ => x + 1 / 2) ∘ fun x : ℝ => (1 / 2 : ℝ) * x) ⁻¹' Ioi 0
rw [preimage_comp, preimage_add_const_Ioi, zero_sub, preimage_const_mul_Ioi (_ : ℝ) one_half_pos, neg_div,
div_self (@one_half_pos ℝ _).ne']
· ext1 x
change log (Gamma (x / 2 + 1 / 2)) = log (Gamma ((1 / 2 : ℝ) • x + 1 / 2))
rw [smul_eq_mul, mul_comm, mul_one_div]
· simpa only [mul_comm _ (log _)] using (convexOn_id (convex_Ioi (0 : ℝ))).smul (log_pos one_lt_two).le
