ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<GOAL>DifferentiableWithinAt ℝ (fun x => Real.exp (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ (fun x => Real.exp (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hc : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun x => Real.exp (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hc : Differentiable ℝ f<GOAL>Differentiable ℝ fun x => Real.exp (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.exp (f x)) s x = Real.exp (f x) • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>fderiv ℝ (fun x => Real.exp (f x)) x = Real.exp (f x) • fderiv ℝ f x
<VAR>n : ℕ<VAR>c : ℝ<GOAL>(iteratedDeriv n fun s => Real.exp (c * s)) = fun s => c ^ n * Real.exp (c * s)
<VAR>z w : ↥circle<GOAL>(↑z).arg = (↑w).arg ↔ z = w
<VAR>z : ↥circle<GOAL>expMapCircle (↑z).arg = z
<GOAL>circle.argPartialEquiv.target = Set.Ioc (-π) π
<GOAL>↑circle.argPartialEquiv.symm = ⇑expMapCircle
<GOAL>↑circle.argPartialEquiv = Complex.arg ∘ Subtype.val
<VAR>z : ↥circle<GOAL>↑(circle.argEquiv z) = (↑z).arg
<GOAL>⇑circle.argEquiv.symm = ⇑expMapCircle ∘ Subtype.val
<GOAL>Function.LeftInverse (⇑expMapCircle) (Complex.arg ∘ Subtype.val)
<GOAL>Set.InvOn (Complex.arg ∘ Subtype.val) (⇑expMapCircle) (Set.Ioc (-π) π) Set.univ
<GOAL>Set.SurjOn (⇑expMapCircle) (Set.Ioc (-π) π) Set.univ
<GOAL>Function.Periodic (⇑expMapCircle) (2 * π)
<VAR>x : ℝ<GOAL>expMapCircle (x - 2 * π) = expMapCircle x
<VAR>x : ℝ<GOAL>expMapCircle (x + 2 * π) = expMapCircle x
<VAR>x : ℝ<GOAL>(↑x).expMapCircle = expMapCircle x
<VAR>θ : Real.Angle<GOAL>↑θ.expMapCircle = ↑θ.cos + ↑θ.sin * Complex.I
<VAR>θ : Real.Angle<GOAL>(-θ).expMapCircle = θ.expMapCircle⁻¹
<VAR>θ₁ θ₂ : Real.Angle<GOAL>(θ₁ + θ₂).expMapCircle = θ₁.expMapCircle * θ₂.expMapCircle
<VAR>θ : Real.Angle<GOAL>↑(↑θ.expMapCircle).arg = θ
<VAR>T : ℝ<GOAL>Function.Periodic (fun x => expMapCircle (2 * π / T * x)) T
<VAR>T : ℝ<VAR>x : ℝ<GOAL>AddCircle.toCircle ↑x = expMapCircle (2 * π / T * x)
<VAR>T : ℝ<GOAL>Continuous AddCircle.toCircle
<VAR>T : ℝ<VAR>hT : T ≠ 0<GOAL>Function.Injective AddCircle.toCircle
<VAR>θ : Real.Angle<GOAL>AddCircle.homeomorphCircle' θ = θ.expMapCircle
<VAR>x : ↥circle<GOAL>AddCircle.homeomorphCircle'.symm x = ↑(↑x).arg
<VAR>x : ℝ<GOAL>AddCircle.homeomorphCircle' ↑x = expMapCircle x
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>x : AddCircle T<GOAL>(AddCircle.homeomorphCircle hT) x = x.toCircle
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ℤ<GOAL>↑(ZMod.toCircle ↑j) = cexp (2 * ↑π * Complex.I * ↑j / ↑N)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ℕ<GOAL>↑(ZMod.toCircle ↑j) = cexp (2 * ↑π * Complex.I * ↑j / ↑N)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ZMod N<GOAL>↑(ZMod.toCircle j) = cexp (2 * ↑π * Complex.I * ↑j.val / ↑N)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ℤ<GOAL>ZMod.stdAddChar ↑j = cexp (2 * ↑π * Complex.I * ↑j / ↑N)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ZMod N<GOAL>ZMod.stdAddChar j = ↑(ZMod.toCircle j)
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>hbdd : BddBelow (Set.range fun n => u n / ↑n)<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>h.lim ≤ u n / ↑n
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<GOAL>∀ᶠ (p : ℕ) in Filter.atTop, u p / ↑p < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>hbdd : BddBelow (Set.range fun n => u n / ↑n)<GOAL>Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (𝓝 h.lim)
<VAR>x : ℂ<VAR>h : x ∈ Complex.slitPlane<GOAL>HasStrictDerivAt Complex.log x⁻¹ x
<VAR>z : ℂ<VAR>hz : z ∈ Complex.slitPlane<GOAL>HasDerivAt Complex.log z⁻¹ z
<VAR>z : ℂ<VAR>hz : z ∈ Complex.slitPlane<GOAL>DifferentiableAt ℂ Complex.log z
<VAR>x : ℂ<VAR>h : x ∈ Complex.slitPlane<GOAL>HasStrictFDerivAt Complex.log (x⁻¹ • 1) x
<VAR>x : ℂ<VAR>h : x ∈ Complex.slitPlane<VAR>n : ℕ∞<GOAL>ContDiffAt ℂ n Complex.log x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>h₁ : HasStrictFDerivAt f f' x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasStrictFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h₁ : HasStrictDerivAt f f' x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasStrictDerivAt (fun t => Complex.log (f t)) (f' / f x) x
<VAR>f : ℝ → ℂ<VAR>x : ℝ<VAR>f' : ℂ<VAR>h₁ : HasStrictDerivAt f f' x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasStrictDerivAt (fun t => Complex.log (f t)) (f' / f x) x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>h₁ : HasFDerivAt f f' x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h₁ : HasDerivAt f f' x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasDerivAt (fun t => Complex.log (f t)) (f' / f x) x
<VAR>f : ℝ → ℂ<VAR>x : ℝ<VAR>f' : ℂ<VAR>h₁ : HasDerivAt f f' x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasDerivAt (fun t => Complex.log (f t)) (f' / f x) x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>h₁ : DifferentiableAt ℂ f x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>DifferentiableAt ℂ (fun t => Complex.log (f t)) x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>s : Set E<VAR>x : E<VAR>h₁ : HasFDerivWithinAt f f' s x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasFDerivWithinAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') s x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>h₁ : HasDerivWithinAt f f' s x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasDerivWithinAt (fun t => Complex.log (f t)) (f' / f x) s x
<VAR>f : ℝ → ℂ<VAR>s : Set ℝ<VAR>x : ℝ<VAR>f' : ℂ<VAR>h₁ : HasDerivWithinAt f f' s x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>HasDerivWithinAt (fun t => Complex.log (f t)) (f' / f x) s x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>x : E<VAR>h₁ : DifferentiableWithinAt ℂ f s x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>DifferentiableWithinAt ℂ (fun t => Complex.log (f t)) s x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>h₁ : DifferentiableOn ℂ f s<VAR>h₂ : ∀ x ∈ s, f x ∈ Complex.slitPlane<GOAL>DifferentiableOn ℂ (fun t => Complex.log (f t)) s
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>h₁ : Differentiable ℂ f<VAR>h₂ : ∀ (x : E), f x ∈ Complex.slitPlane<GOAL>Differentiable ℂ fun t => Complex.log (f t)
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>h₁ : DifferentiableAt ℂ f x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>deriv (Complex.log ∘ f) x = logDeriv f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>s : Set α<VAR>f : α → E<VAR>a : α<GOAL>‖s.indicator f a‖ = s.indicator (fun a => ‖f a‖) a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>s : Set α<VAR>f : α → E<VAR>a : α<GOAL>‖s.indicator f a‖₊ = s.indicator (fun a => ‖f a‖₊) a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>f : α → E<VAR>a : α<GOAL>‖s.indicator f a‖ ≤ ‖t.indicator f a‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>s : Set α<VAR>f : α → E<VAR>a : α<GOAL>s.indicator (fun a => ‖f a‖) a ≤ ‖f a‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>s : Set α<VAR>f : α → E<VAR>a : α<GOAL>‖s.indicator f a‖ ≤ ‖f a‖
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>(∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / ∑ i ∈ s, w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∏ i ∈ s, z i ^ w i = x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∑ i ∈ s, w i * z i = x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0<VAR>hw' : ∑ i ∈ s, w i = 1<GOAL>∏ i ∈ s, z i ^ ↑(w i) ≤ ∑ i ∈ s, w i * z i
<VAR>w₁ w₂ p₁ p₂ : ℝ≥0<GOAL>w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂
<VAR>w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0<GOAL>w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
<VAR>w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0<GOAL>w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
<VAR>w₁ w₂ p₁ p₂ : ℝ<VAR>hw₁ : 0 ≤ w₁<VAR>hw₂ : 0 ≤ w₂<VAR>hp₁ : 0 ≤ p₁<VAR>hp₂ : 0 ≤ p₂<VAR>hw : w₁ + w₂ = 1<GOAL>p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂
<VAR>w₁ w₂ w₃ p₁ p₂ p₃ : ℝ<VAR>hw₁ : 0 ≤ w₁<VAR>hw₂ : 0 ≤ w₂<VAR>hw₃ : 0 ≤ w₃<VAR>hp₁ : 0 ≤ p₁<VAR>hp₂ : 0 ≤ p₂<VAR>hp₃ : 0 ≤ p₃<VAR>hw : w₁ + w₂ + w₃ = 1<GOAL>p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
<VAR>w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ<VAR>hw₁ : 0 ≤ w₁<VAR>hw₂ : 0 ≤ w₂<VAR>hw₃ : 0 ≤ w₃<VAR>hw₄ : 0 ≤ w₄<VAR>hp₁ : 0 ≤ p₁<VAR>hp₂ : 0 ≤ p₂<VAR>hp₃ : 0 ≤ p₃<VAR>hp₄ : 0 ≤ p₄<VAR>hw : w₁ + w₂ + w₃ + w₄ = 1<GOAL>p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ * p₄ ^ w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 < z i<GOAL>(∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹
<VAR>a b p q : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hpq : p.IsConjExponent q<GOAL>a * b ≤ a ^ p / p + b ^ q / q
<VAR>a b : ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>a * b ≤ |a| ^ p / p + |b| ^ q / q
<VAR>a b : ℝ≥0<VAR>p q : ℝ≥0<VAR>hpq : p.IsConjExponent q<GOAL>a * b ≤ a ^ ↑p / p + b ^ ↑q / q
<VAR>a b : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal
<VAR>a b : ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>w f : ι → ℝ≥0<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ q<GOAL>(Summable fun i => f i * g i) ∧ ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ q<GOAL>Summable fun i => f i * g i
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ q<GOAL>∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ q) (B ^ q)<GOAL>∃ C ≤ A * B, HasSum (fun i => f i * g i) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>IsGreatest ((fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}) ((∑ i ∈ s, f i ^ p) ^ (1 / p))
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<GOAL>Summable fun i => (f i + g i) ^ p
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<GOAL>(∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ p) (B ^ p)<GOAL>∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, |f i|) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, |f i| ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>w f : ι → ℝ<VAR>hw : ∀ (i : ι), 0 ≤ w i<VAR>hf : ∀ (i : ι), 0 ≤ f i<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : Summable fun i => f i ^ p<VAR>hg_sum : Summable fun i => g i ^ q<GOAL>(Summable fun i => f i * g i) ∧ ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : Summable fun i => f i ^ p<VAR>hg_sum : Summable fun i => g i ^ q<GOAL>Summable fun i => f i * g i
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : Summable fun i => f i ^ p<VAR>hg_sum : Summable fun i => g i ^ q<GOAL>∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>A B : ℝ<VAR>hA : 0 ≤ A<VAR>hB : 0 ≤ B<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg_sum : HasSum (fun i => g i ^ q) (B ^ q)<GOAL>∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>hg : ∀ i ∈ s, 0 ≤ g i<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : Summable fun i => f i ^ p<VAR>hg_sum : Summable fun i => g i ^ p<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : Summable fun i => f i ^ p<VAR>hg_sum : Summable fun i => g i ^ p<GOAL>Summable fun i => (f i + g i) ^ p
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>hf_sum : Summable fun i => f i ^ p<VAR>hg_sum : Summable fun i => g i ^ p<GOAL>(∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>f g : ι → ℝ<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>A B : ℝ<VAR>hA : 0 ≤ A<VAR>hB : 0 ≤ B<VAR>hfA : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hgB : HasSum (fun i => g i ^ p) (B ^ p)<GOAL>∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0∞<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>b : ℂ<VAR>hb : b ≠ 0<GOAL>(fun x => 0 ^ x) =ᶠ[𝓝 b] 0
<VAR>a b : ℂ<VAR>ha : a ≠ 0<GOAL>(fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)
<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ≠ 0<GOAL>(fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.1 * x.2)
<VAR>a b : ℂ<VAR>ha : a ≠ 0<GOAL>ContinuousAt (fun x => a ^ x) b
<VAR>a b : ℂ<VAR>h : b ≠ 0<GOAL>ContinuousAt (fun x => a ^ x) b
<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ∈ Complex.slitPlane<GOAL>ContinuousAt (fun x => x.1 ^ x.2) p
<VAR>a b : ℂ<VAR>ha : a ∈ Complex.slitPlane<GOAL>ContinuousAt (fun x => x ^ b) a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>a b : ℂ<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>hg : Filter.Tendsto g l (𝓝 b)<VAR>ha : a ∈ Complex.slitPlane<GOAL>Filter.Tendsto (fun x => f x ^ g x) l (𝓝 (a ^ b))
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<VAR>a b : ℂ<VAR>hf : Filter.Tendsto f l (𝓝 b)<VAR>h : a ≠ 0 ∨ b ≠ 0<GOAL>Filter.Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℂ<VAR>s : Set α<VAR>a : α<VAR>hf : ContinuousWithinAt f s a<VAR>hg : ContinuousWithinAt g s a<VAR>h0 : f a ∈ Complex.slitPlane<GOAL>ContinuousWithinAt (fun x => f x ^ g x) s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>a : α<VAR>b : ℂ<VAR>hf : ContinuousWithinAt f s a<VAR>h : b ≠ 0 ∨ f a ≠ 0<GOAL>ContinuousWithinAt (fun x => b ^ f x) s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℂ<VAR>a : α<VAR>hf : ContinuousAt f a<VAR>hg : ContinuousAt g a<VAR>h0 : f a ∈ Complex.slitPlane<GOAL>ContinuousAt (fun x => f x ^ g x) a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>a : α<VAR>b : ℂ<VAR>hf : ContinuousAt f a<VAR>h : b ≠ 0 ∨ f a ≠ 0<GOAL>ContinuousAt (fun x => b ^ f x) a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℂ<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>h0 : ∀ a ∈ s, f a ∈ Complex.slitPlane<GOAL>ContinuousOn (fun x => f x ^ g x) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>b : ℂ<VAR>hf : ContinuousOn f s<VAR>h : b ≠ 0 ∨ ∀ a ∈ s, f a ≠ 0<GOAL>ContinuousOn (fun x => b ^ f x) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℂ<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h0 : ∀ (a : α), f a ∈ Complex.slitPlane<GOAL>Continuous fun x => f x ^ g x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>b : ℂ<VAR>hf : Continuous f<VAR>h : b ≠ 0 ∨ ∀ (a : α), f a ≠ 0<GOAL>Continuous fun x => b ^ f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>b : ℂ<VAR>hf : ContinuousOn f s<VAR>h : ∀ a ∈ s, f a ∈ Complex.slitPlane<GOAL>ContinuousOn (fun x => f x ^ b) s
<VAR>p : ℝ × ℝ<VAR>hp_fst : p.1 < 0<GOAL>(fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (Real.log x.1 * x.2) * Real.cos (x.2 * π)
<VAR>p : ℝ × ℝ<VAR>hp_fst : 0 < p.1<GOAL>(fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (Real.log x.1 * x.2)
<VAR>p : ℝ × ℝ<VAR>hp : p.1 ≠ 0<GOAL>ContinuousAt (fun p => p.1 ^ p.2) p
<VAR>p : ℝ × ℝ<VAR>hp : 0 < p.2<GOAL>ContinuousAt (fun p => p.1 ^ p.2) p
<VAR>p : ℝ × ℝ<VAR>h : p.1 ≠ 0 ∨ 0 < p.2<GOAL>ContinuousAt (fun p => p.1 ^ p.2) p
<VAR>x q : ℝ<VAR>h : x ≠ 0 ∨ 0 ≤ q<GOAL>ContinuousAt (fun x => x ^ q) x
<VAR>q : ℝ<VAR>h : 0 ≤ q<GOAL>Continuous fun x => x ^ q
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>x y : ℝ<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<VAR>h : x ≠ 0 ∨ 0 < y<GOAL>Filter.Tendsto (fun t => f t ^ g t) l (𝓝 (x ^ y))
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<VAR>x p : ℝ<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>h : x ≠ 0 ∨ 0 ≤ p<GOAL>Filter.Tendsto (fun a => f a ^ p) l (𝓝 (x ^ p))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℝ<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<VAR>h : f x ≠ 0 ∨ 0 < g x<GOAL>ContinuousAt (fun t => f t ^ g t) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<VAR>h : f x ≠ 0 ∨ 0 < g x<GOAL>ContinuousWithinAt (fun t => f t ^ g t) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>h : ∀ x ∈ s, f x ≠ 0 ∨ 0 < g x<GOAL>ContinuousOn (fun t => f t ^ g t) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℝ<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : ∀ (x : α), f x ≠ 0 ∨ 0 < g x<GOAL>Continuous fun x => f x ^ g x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>x : α<VAR>p : ℝ<VAR>hf : ContinuousWithinAt f s x<VAR>h : f x ≠ 0 ∨ 0 ≤ p<GOAL>ContinuousWithinAt (fun x => f x ^ p) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>x : α<VAR>p : ℝ<VAR>hf : ContinuousAt f x<VAR>h : f x ≠ 0 ∨ 0 ≤ p<GOAL>ContinuousAt (fun x => f x ^ p) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>p : ℝ<VAR>hf : ContinuousOn f s<VAR>h : ∀ x ∈ s, f x ≠ 0 ∨ 0 ≤ p<GOAL>ContinuousOn (fun x => f x ^ p) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>p : ℝ<VAR>hf : Continuous f<VAR>h : ∀ (x : α), f x ≠ 0 ∨ 0 ≤ p<GOAL>Continuous fun x => f x ^ p
<VAR>p : ℂ × ℂ<VAR>h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0<VAR>h₂ : 0 < p.2.re<GOAL>ContinuousAt (fun x => x.1 ^ x.2) p
<VAR>z w : ℂ<VAR>hz : 0 ≤ z.re ∨ z.im ≠ 0<VAR>hw : 0 < w.re<GOAL>ContinuousAt (fun x => x ^ w) z
<VAR>x : ℝ<VAR>y : ℂ<VAR>h : 0 < y.re ∨ x ≠ 0<GOAL>ContinuousAt (fun a => ↑a ^ y) x
<VAR>y : ℂ<VAR>hs : 0 < y.re<GOAL>Continuous fun x => ↑x ^ y
<VAR>x : ℝ≥0<VAR>y : ℝ≥0<VAR>hy : 1 < y<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, x ^ (1 / ↑n) ≤ y
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0<VAR>v : α → ℝ<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>hx : Filter.Tendsto u f (𝓝 x)<VAR>hy : Filter.Tendsto v f (𝓝 y)<VAR>h : x ≠ 0 ∨ 0 < y<GOAL>Filter.Tendsto (fun a => u a ^ v a) f (𝓝 (x ^ y))
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : x ≠ 0 ∨ 0 ≤ y<GOAL>ContinuousAt (fun z => z ^ y) x
<VAR>y : ℝ<VAR>h : 0 ≤ y<GOAL>Continuous fun x => x ^ y
<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>y : ℝ≥0∞<VAR>hy : 1 < y<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, x ^ (1 / ↑n) ≤ y
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>h : 0 < y<GOAL>ContinuousAt (fun a => a ^ y) x
<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Filter.Tendsto (fun x => c * x ^ y) (𝓝 0) (𝓝 0)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>r : ℝ<VAR>hm : Filter.Tendsto m f (𝓝 a)<GOAL>Filter.Tendsto (fun x => m x ^ r) f (𝓝 (a ^ r))
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>Real.Gamma (a * s + b * t) ≤ Real.Gamma s ^ a * Real.Gamma t ^ b
<GOAL>ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ Real.Gamma)
<GOAL>ConvexOn ℝ (Set.Ioi 0) Real.Gamma
<VAR>f : ℝ → ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hn : n ≠ 0<GOAL>f ↑n = f 1 + Real.log ↑(n - 1)!
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hx : 0 < x<VAR>n : ℕ<GOAL>f (x + ↑n) = f x + ∑ m ∈ Finset.range n, Real.log (x + ↑m)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hn : n ≠ 0<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>f (↑n + x) ≤ f ↑n + x * Real.log ↑n