-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem doublingGamma_log_convex_Ioi : ConvexOn ℝ (Ioi (0 : ℝ)) (log ∘ doublingGamma)

Proof state:
case h.e'_10

⊢ (fun s => log (Gamma (s / 2 + 1 / 2))) =
    (log ∘ Gamma) ∘ ⇑((DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))

Tactic:
ext1 x

Result:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2 + 1 / 2)) =
    ((log ∘ Gamma) ∘ ⇑((DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))) x

Proof state:
case h.e'_9

⊢ Ioi (-1) = ((fun x => x + 1 / 2) ∘ fun x => 1 / 2 * x) ⁻¹' Ioi 0

Tactic:
rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
  preimage_const_mul_Ioi (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']

Result:
no goals

Proof state:
case h.e'_9

⊢ Ioi (-1) = ⇑((DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2)) ⁻¹' Ioi 0

Tactic:
change Ioi (-1 : ℝ) = ((fun x : ℝ => x + 1 / 2) ∘ fun x : ℝ => (1 / 2 : ℝ) * x) ⁻¹' Ioi 0

Result:
case h.e'_9

⊢ Ioi (-1) = ((fun x => x + 1 / 2) ∘ fun x => 1 / 2 * x) ⁻¹' Ioi 0

Proof state:
case refine_2

⊢ ConvexOn ℝ (Ioi (-1)) fun s => log (Gamma (s / 2 + 1 / 2))

Tactic:
convert
  convexOn_log_Gamma.comp_affineMap
    ((DistribMulAction.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
      AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using 1

Result:
case h.e'_9

⊢ Ioi (-1) = ⇑((DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2)) ⁻¹' Ioi 0

case h.e'_10

⊢ (fun s => log (Gamma (s / 2 + 1 / 2))) =
    (log ∘ Gamma) ∘ ⇑((DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))

Proof state:
⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)

Tactic:
refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm

Result:
case refine_1

⊢ ConvexOn ℝ (Ioi 0) fun s => log (Gamma (s / 2))

case refine_2

⊢ ConvexOn ℝ (Ioi 0) fun s => log (Gamma (s / 2 + 1 / 2))

case refine_3

⊢ ConvexOn ℝ (Ioi 0) fun s => s * log 2

Proof state:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2 + 1 / 2)) = log (Gamma ((1 / 2) • x + 1 / 2))

Tactic:
rw [smul_eq_mul, mul_comm, mul_one_div]

Result:
no goals

Proof state:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2)) = ((log ∘ Gamma) ∘ ⇑(DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap) x

Tactic:
simp only [LinearMap.coe_toAffineMap, Function.comp_apply, DistribMulAction.toLinearMap_apply]

Result:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2)) = log (Gamma ((1 / 2) • x))

Proof state:
case refine_3

⊢ ConvexOn ℝ (Ioi 0) fun s => s * log 2

Tactic:
simpa only [mul_comm _ (log _)] using
  (convexOn_id (convex_Ioi (0 : ℝ))).smul (log_pos one_lt_two).le

Result:
no goals

Proof state:
case h.e'_10

⊢ (fun s => log (Gamma (s / 2))) = (log ∘ Gamma) ∘ ⇑(DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap

Tactic:
ext1 x

Result:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2)) = ((log ∘ Gamma) ∘ ⇑(DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap) x

Proof state:
case refine_2

⊢ ConvexOn ℝ (Ioi 0) fun s => log (Gamma (s / 2 + 1 / 2))

Tactic:
refine ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)

Result:
case refine_2

⊢ ConvexOn ℝ (Ioi (-1)) fun s => log (Gamma (s / 2 + 1 / 2))

Proof state:
case h.e'_9

⊢ Ioi 0 = ⇑(DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap ⁻¹' Ioi 0

Tactic:
simpa only [zero_div] using (preimage_const_mul_Ioi (0 : ℝ) one_half_pos).symm

Result:
no goals

Proof state:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2)) = log (Gamma ((1 / 2) • x))

Tactic:
rw [smul_eq_mul, mul_comm, mul_one_div]

Result:
no goals

Proof state:
case refine_1

⊢ ConvexOn ℝ (Ioi 0) fun s => log (Gamma (s / 2))

Tactic:
convert
  convexOn_log_Gamma.comp_affineMap (DistribMulAction.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap
  using 1

Result:
case h.e'_9

⊢ Ioi 0 = ⇑(DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap ⁻¹' Ioi 0

case h.e'_10

⊢ (fun s => log (Gamma (s / 2))) = (log ∘ Gamma) ∘ ⇑(DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap

Proof state:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2 + 1 / 2)) =
    ((log ∘ Gamma) ∘ ⇑((DistribMulAction.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))) x

Tactic:
change log (Gamma (x / 2 + 1 / 2)) = log (Gamma ((1 / 2 : ℝ) • x + 1 / 2))

Result:
case h.e'_10.h
x : ℝ
⊢ log (Gamma (x / 2 + 1 / 2)) = log (Gamma ((1 / 2) • x + 1 / 2))