awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
apply :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (u - 1))
    fun (x : ℝ) ↦ ‖f c u x‖ ^ (1 / c)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ ‖f c u x‖ ^ (1 / c))
    (Measure.restrict volume (Ioi 0))

Tactic:
apply Integrable.congr (GammaIntegral_convergent hu)

Premises used: Real.GammaIntegral_convergent, MeasureTheory.Integrable.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (u - 1))
    fun (x : ℝ) ↦ ‖f c u x‖ ^ (1 / c)

Tactic:
eventuallyEq_of_mem (self_mem_ae_restrict measurableSet_Ioi) fun x hx => ?_

Premises used: Filter.eventuallyEq_of_mem, measurableSet_Ioi, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), rexp (-x) * x ^ (u - 1) = ‖f c u x‖ ^ (1 / c)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (u - 1))
    fun (x : ℝ) ↦ ‖f c u x‖ ^ (1 / c)

Tactic:
refine eventuallyEq_of_mem (self_mem_ae_restrict measurableSet_Ioi) fun x hx => ?_

Premises used: Filter.eventuallyEq_of_mem, measurableSet_Ioi, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : f c u x ^ (1 / c) = ‖f c u x‖ ^ (1 / c)
⊢ rexp (-x) * x ^ (u - 1) = ‖f c u x‖ ^ (1 / c)

Tactic:
rw [fpow hc u hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
e_a : f c u x = ‖f c u x‖
⊢ f c u x ^ (1 / c) = ‖f c u x‖ ^ (1 / c)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ f c u x = ‖f c u x‖

Tactic:
(norm_of_nonneg (posf _ _ x hx)).symm

Premises used: Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ f c u x = ‖f c u x‖

Tactic:
exact (norm_of_nonneg (posf _ _ x hx)).symm

Premises used: Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (f c u) (Measure.restrict volume (Ioi 0))

Tactic:
ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
refine : ContinuousOn (f c u) (Ioi 0)
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (f c u) (Measure.restrict volume (Ioi 0))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ rexp (-c * x)) (Ioi 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ (c * (u - 1))) x
⊢ ContinuousOn (f c u) (Ioi 0)

Tactic:
refine .mul (by fun_prop) (continuousOn_of_forall_continuousAt fun x hx ↦ ?_)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ (c * (u - 1))) x

Tactic:
continuousAt_rpow_const _ _ (Or.inl (mem_Ioi.mp hx).ne')

Premises used: Real.continuousAt_rpow_const, Set.mem_Ioi, LT.lt.ne', Iff.mp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ (c * (u - 1))) x

Tactic:
exact continuousAt_rpow_const _ _ (Or.inl (mem_Ioi.mp hx).ne')

Premises used: Real.continuousAt_rpow_const, Set.mem_Ioi, LT.lt.ne', Iff.mp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
⊢ ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))

Tactic:
have f_mem_Lp :
    ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
      MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0)) := by
    intro c u hc hu
    have A : ENNReal.ofReal (1 / c) ≠ 0 := by
      rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
    have B : ENNReal.ofReal (1 / c) ≠ ∞ := ENNReal.ofReal_ne_top
    rw [← memLp_norm_rpow_iff _ A B, ENNReal.toReal_ofReal (one_div_nonneg.mpr hc.le),
      ENNReal.div_self A B, memLp_one_iff_integrable]
    · apply Integrable.congr (GammaIntegral_convergent hu)
      refine eventuallyEq_of_mem (self_mem_ae_restrict measurableSet_Ioi) fun x hx => ?_
      dsimp only
      rw [fpow hc u hx]
      congr 1
      exact (norm_of_nonneg (posf _ _ x hx)).symm
    · refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
      refine .mul (by fun_prop) (continuousOn_of_forall_continuousAt fun x hx ↦ ?_)
      exact continuousAt_rpow_const _ _ (Or.inl (mem_Ioi.mp hx).ne')
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (a * s + b * t - 1)) ≤
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (t - 1))
        b
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b

Tactic:
rw [Gamma_eq_integral hs, Gamma_eq_integral ht, Gamma_eq_integral hst]

Premises used: Real.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      f a s a_1 * f b t a_1) ≤
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
          f a s a_1 ^ (1 / a))
        (1 / (1 / a)) *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          f b t a ^ (1 / b))
        (1 / (1 / b))

Tactic:
MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg e (posf' a s) (posf' b t) (f_mem_Lp ha hs)
      (f_mem_Lp hb ht)

Premises used: MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (a * s + b * t - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      f a s a_1 * f b t a_1)
h₁ :
  HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (t - 1))
        b =
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
          f a s a_1 ^ (1 / a))
        (1 / (1 / a)) *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          f b t a ^ (1 / b))
        (1 / (1 / b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (a * s + b * t - 1)) ≤
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (t - 1))
        b

Tactic:
convert!
    MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg e (posf' a s) (posf' b t) (f_mem_Lp ha hs)
      (f_mem_Lp hb ht) using 1

Premises used: MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (a * s + b * t - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      f a s a_1 * f b t a_1)

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), rexp (-x) * x ^ (a * s + b * t - 1) = f a s x * f b t x
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (a * s + b * t - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      f a s a_1 * f b t a_1)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : rexp (-x) = rexp (-a * x + -b * x)
rw₁ : rexp (-x) = rexp ((-a + -b) * x)
rw₂ : rexp (-x) = rexp (-(a + b) * x)
rw₃ : rexp (-x) = rexp (-1 * x)
rw₄ rw₅ : rexp (-x) = rexp (-x)
⊢ rexp (-x) = rexp (-a * x) * rexp (-b * x)

Tactic:
rw [← exp_add, ← add_mul, ← neg_add, hab, neg_one_mul]

Premises used: add_mul, neg_one_mul, neg_add, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ rexp (-x) = rexp (-a * x) * rexp (-b * x)

Tactic:
have A : exp (-x) = exp (-a * x) * exp (-b * x) := by
      rw [← exp_add, ← add_mul, ← neg_add, hab, neg_one_mul]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
rw : x ^ (a * s + (1 - a) * t - 1) = x ^ (a * (s - 1) + (1 - a) * (t - 1))
⊢ x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))

Tactic:
rw [← rpow_add hx, hab']

Premises used: Real.rpow_add