ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>NormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>DenselyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖) '' Metric.closedBall 0 1) = ‖f‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₁₂<VAR>e : E ≃SL[σ₁₂] F<GOAL>LipschitzWith ‖↑e‖₊ ⇑e
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>f : E' → F<VAR>s : Set (E' →SL[σ₁₂] F)<VAR>hs : Bornology.IsBounded s<VAR>hf : f ∈ closure (DFunLike.coe '' s)<GOAL>⇑(ContinuousLinearMap.ofMemClosureImageCoeBounded f hs hf) = f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>α : Type u_12<VAR>l : Filter α<VAR>l.NeBot<VAR>f : E' → F<VAR>g : α → E' →SL[σ₁₂] F<VAR>hf : Filter.Tendsto (fun a x => (g a) x) l (𝓝 f)<VAR>hg : Bornology.IsBounded (Set.range g)<GOAL>⇑(ContinuousLinearMap.ofTendstoOfBoundedRange f g hf hg) = f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Filter.Tendsto (fun n x => (f n) x) Filter.atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 g)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>ProperSpace F<VAR>s : Set (E' →SL[σ₁₂] F)<VAR>hb : Bornology.IsBounded s<GOAL>IsCompact (closure (DFunLike.coe '' s))
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>ProperSpace F<VAR>s : Set (E' →SL[σ₁₂] F)<VAR>hb : Bornology.IsBounded s<VAR>hc : IsClosed (DFunLike.coe '' s)<GOAL>IsCompact (DFunLike.coe '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>s : Set (E' →SL[σ₁₂] F)<VAR>hb : Bornology.IsBounded s<VAR>hc : ∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s<GOAL>IsClosed (DFunLike.coe '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>ProperSpace F<VAR>s : Set (E' →SL[σ₁₂] F)<VAR>hb : Bornology.IsBounded s<VAR>hc : ∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s<GOAL>IsCompact (DFunLike.coe '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>E' : Type u_11<VAR>SeminormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>RingHomIsometric σ₁₂<VAR>f₀ : E' →SL[σ₁₂] F<VAR>r : ℝ<VAR>f : E' →SL[σ₁₂] F<VAR>hf : ⇑f ∈ closure (DFunLike.coe '' Metric.closedBall f₀ r)<GOAL>f ∈ Metric.closedBall f₀ r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f₀ : E →SL[σ₁₂] F<VAR>r : ℝ<GOAL>IsClosed (DFunLike.coe '' Metric.closedBall f₀ r)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>ProperSpace F<VAR>f₀ : E →SL[σ₁₂] F<VAR>r : ℝ<GOAL>IsCompact (DFunLike.coe '' Metric.closedBall f₀ r)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜 Fₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ₁₂] F<VAR>CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>h_e : UniformInducing ⇑e<VAR>x : E<GOAL>(f.extend e h_dense h_e) (e x) = f x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜 Fₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ₁₂] F<VAR>CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>h_e : UniformInducing ⇑e<VAR>g : Fₗ →SL[σ₁₂] F<VAR>H : g.comp e = f<GOAL>f.extend e h_dense h_e = g
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜 Fₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>h_e : UniformInducing ⇑e<GOAL>ContinuousLinearMap.extend 0 e h_dense h_e = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜 Fₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ₁₂] F<VAR>CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>N : ℝ≥0<VAR>h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖<VAR>RingHomIsometric σ₁₂<GOAL>‖f.extend e h_dense ⋯‖ ≤ ↑N * ‖f‖
<VAR>x y : ℝ<GOAL>x.rpow y = x ^ y
<VAR>x y : ℝ<GOAL>x ^ y = (↑x ^ ↑y).re
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>x ^ y = rexp (Real.log x * y)
<VAR>x y : ℝ<GOAL>rexp (x * y) = rexp x ^ y
<VAR>x : ℝ<VAR>n : ℤ<GOAL>x ^ ↑n = x ^ n
<VAR>x : ℝ<VAR>n : ℕ<GOAL>x ^ ↑n = x ^ n
<VAR>x : ℝ<GOAL>rexp 1 ^ x = rexp x
<VAR>n : ℕ<GOAL>rexp 1 ^ n = rexp ↑n
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>x ^ y = 0 ↔ x = 0
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>x ^ y ≠ 0 ↔ x ≠ 0
<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<GOAL>x ^ y = rexp (Real.log x * y) * Real.cos (y * π)
<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>y : ℝ<GOAL>x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y) * Real.cos (y * π)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>0 < x ^ y
<VAR>x : ℝ<GOAL>x ^ 0 = 1
<VAR>x : ℝ<GOAL>0 < x ^ 0
<VAR>x a : ℝ<GOAL>0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
<VAR>x a : ℝ<GOAL>a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
<VAR>x : ℝ<GOAL>x ^ 1 = x
<VAR>x : ℝ<GOAL>0 ^ x ≤ 1
<VAR>x : ℝ<GOAL>0 ≤ 0 ^ x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>0 ≤ x ^ y
<VAR>x y : ℝ<VAR>hx_nonneg : 0 ≤ x<GOAL>|x ^ y| = |x| ^ y
<VAR>x y : ℝ<GOAL>|x ^ y| ≤ |x| ^ y
<VAR>x y : ℝ<GOAL>|x ^ y| ≤ rexp (Real.log x * y)
<VAR>x y : ℝ<VAR>hx_nonneg : 0 ≤ x<GOAL>‖x ^ y‖ = ‖x‖ ^ y
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y z : ℝ<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>h : y + z ≠ 0<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>w x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hw : w ≠ 0<VAR>h : y + z = w<GOAL>x ^ w = x ^ y * x ^ z
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 ≤ z<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<GOAL>x ^ y * x ^ z ≤ x ^ (y + z)
<VAR>ι : Type u_1<VAR>a : ℝ<VAR>ha : 0 < a<VAR>f : ι → ℝ<VAR>s : Finset ι<GOAL>a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
<VAR>ι : Type u_1<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>h : ∀ x ∈ s, 0 ≤ f x<GOAL>a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>x ^ (-y) = (x ^ y)⁻¹
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y z : ℝ<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<VAR>h : y - z ≠ 0<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>hf : HasCompactSupport f<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>HasCompactSupport fun x => f x ^ r
<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>y : ℂ<GOAL>↑x ^ y = (-↑x) ^ y * Complex.exp (↑π * Complex.I * y)
<VAR>x : ℂ<VAR>y : ℝ<GOAL>x ^ ↑y = ↑(Complex.abs x ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * Complex.I)
<VAR>x : ℂ<VAR>y : ℝ<GOAL>(x ^ ↑y).re = Complex.abs x ^ y * Real.cos (x.arg * y)
<VAR>x : ℂ<VAR>y : ℝ<GOAL>(x ^ ↑y).im = Complex.abs x ^ y * Real.sin (x.arg * y)
<VAR>z : ℂ<VAR>hz : z ≠ 0<VAR>w : ℂ<GOAL>Complex.abs (z ^ w) = Complex.abs z ^ w.re / rexp (z.arg * w.im)
<VAR>z w : ℂ<VAR>h : z = 0 → w.re = 0 → w = 0<GOAL>Complex.abs (z ^ w) = Complex.abs z ^ w.re / rexp (z.arg * w.im)
<VAR>z w : ℂ<GOAL>Complex.abs (z ^ w) ≤ Complex.abs z ^ w.re / rexp (z.arg * w.im)
<VAR>x : ℂ<VAR>y : ℝ<GOAL>Complex.abs (x ^ ↑y) = Complex.abs x ^ y
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.abs (x ^ (↑n)⁻¹) = Complex.abs x ^ (↑n)⁻¹
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y : ℂ<GOAL>Complex.abs (↑x ^ y) = x ^ y.re
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℂ<VAR>hy : y.re ≠ 0<GOAL>Complex.abs (↑x ^ y) = x ^ y.re
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℂ<GOAL>0 < ‖↑n ^ s‖
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<GOAL>x ^ (y * z) = (x ^ y) ^ z
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>n : ℤ<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y - ↑n) = x ^ y / x ^ n
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℤ<VAR>h : y + ↑n ≠ 0<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>x y : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : y + ↑n ≠ 0<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℤ<VAR>h : y - ↑n ≠ 0<GOAL>x ^ (y - ↑n) = x ^ y / x ^ n
<VAR>x y : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : y - ↑n ≠ 0<GOAL>x ^ (y - ↑n) = x ^ y / x ^ n
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<GOAL>x ^ (y + 1) = x ^ y * x
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<GOAL>x ^ (y - 1) = x ^ y / x
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>h : y + 1 ≠ 0<GOAL>x ^ (y + 1) = x ^ y * x
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>h : 1 + y ≠ 0<GOAL>x ^ (1 + y) = x * x ^ y
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>h : y - 1 ≠ 0<GOAL>x ^ (y - 1) = x ^ y / x
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>h : 1 - y ≠ 0<GOAL>x ^ (1 - y) = x / x ^ y
<VAR>x : ℝ<GOAL>x ^ 2 = x ^ 2
<VAR>x : ℝ<GOAL>x ^ (-1) = x⁻¹
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>(x * y) ^ z = x ^ z * y ^ z
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>x⁻¹ ^ y = (x ^ y)⁻¹
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>z : ℝ<GOAL>(x / y) ^ z = x ^ z / y ^ z
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>Real.log (x ^ y) = y * Real.log x
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hz : 0 < z<GOAL>y * Real.log x = Real.log z ↔ x ^ y = z
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>(x ^ y) ^ y⁻¹ = x
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>(x ^ y⁻¹) ^ y = x
<VAR>x : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>x : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℕ<VAR>z : ℝ<GOAL>x ^ (↑n * z) = (x ^ n) ^ z
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℤ<VAR>z : ℝ<GOAL>x ^ (↑n * z) = (x ^ n) ^ z
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>n : ℤ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hxy : x < y<VAR>hz : 0 < z<GOAL>x ^ z < y ^ z
<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>StrictMonoOn (fun x => x ^ r) (Set.Ici 0)
<VAR>x y z : ℝ<VAR>h : 0 ≤ x<VAR>h₁ : x ≤ y<VAR>h₂ : 0 ≤ z<GOAL>x ^ z ≤ y ^ z
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>MonotoneOn (fun x => x ^ r) (Set.Ici 0)
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hxy : x < y<VAR>hz : z < 0<GOAL>y ^ z < x ^ z
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<GOAL>y ^ z ≤ x ^ z
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ^ z < y ^ z ↔ x < y
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ^ z ≤ y ^ z ↔ x ≤ y
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ^ z < y ^ z ↔ y < x
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ^ z ≤ y ^ z ↔ y ≤ x
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x < y ^ z⁻¹ ↔ x ^ z < y
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ < y ↔ x < y ^ z
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x < y ^ z⁻¹ ↔ y < x ^ z
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ^ z⁻¹ < y ↔ y ^ z < x
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x
<VAR>x y z : ℝ<VAR>hx : 1 < x<VAR>hyz : y < z<GOAL>x ^ y < x ^ z
<VAR>x y z : ℝ<VAR>hx : 1 ≤ x<VAR>hyz : y ≤ z<GOAL>x ^ y ≤ x ^ z
<VAR>x y z : ℝ<VAR>hy : 0 < y<VAR>hxy : y < x<VAR>hz : z < 0<GOAL>x ^ z < y ^ z
<VAR>r : ℝ<VAR>hr : r < 0<GOAL>StrictAntiOn (fun x => x ^ r) (Set.Ioi 0)
<VAR>z x y : ℝ<VAR>hy : 0 < y<VAR>hxy : y ≤ x<VAR>hz : z ≤ 0<GOAL>x ^ z ≤ y ^ z
<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>AntitoneOn (fun x => x ^ r) (Set.Ioi 0)
<VAR>x y z : ℝ<VAR>hx : 1 < x<GOAL>x ^ y ≤ x ^ z ↔ y ≤ z
<VAR>x y z : ℝ<VAR>hx : 1 < x<GOAL>x ^ y < x ^ z ↔ y < z
<VAR>x y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<VAR>hyz : z < y<GOAL>x ^ y < x ^ z
<VAR>x y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x ≤ 1<VAR>hyz : z ≤ y<GOAL>x ^ y ≤ x ^ z
<VAR>x y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<GOAL>x ^ y ≤ x ^ z ↔ z ≤ y
<VAR>x y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<GOAL>x ^ y < x ^ z ↔ z < y
<VAR>x z : ℝ<VAR>hx1 : 0 ≤ x<VAR>hx2 : x < 1<VAR>hz : 0 < z<GOAL>x ^ z < 1
<VAR>x z : ℝ<VAR>hx1 : 0 ≤ x<VAR>hx2 : x ≤ 1<VAR>hz : 0 ≤ z<GOAL>x ^ z ≤ 1
<VAR>x z : ℝ<VAR>hx : 1 < x<VAR>hz : z < 0<GOAL>x ^ z < 1
<VAR>x z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : z ≤ 0<GOAL>x ^ z ≤ 1
<VAR>x z : ℝ<VAR>hx : 1 < x<VAR>hz : 0 < z<GOAL>1 < x ^ z
<VAR>x z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : 0 ≤ z<GOAL>1 ≤ x ^ z
<VAR>x z : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x < 1<VAR>hz : z < 0<GOAL>1 < x ^ z
<VAR>x z : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x ≤ 1<VAR>hz : z ≤ 0<GOAL>1 ≤ x ^ z
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 < y<GOAL>x ^ y < 1 ↔ x < 1
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
<VAR>x y z : ℝ<VAR>hx0 : 0 ≤ x<VAR>hx1 : x ≤ 1<VAR>hz : 0 ≤ z<VAR>hyz : z ≤ y<GOAL>x ^ y ≤ x ^ z
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>Set.InjOn (fun y => y ^ x) {y | 0 ≤ y}
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>x ^ z = y ^ z ↔ x = y
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>x ^ z⁻¹ = y ↔ x = y ^ z
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>x = y ^ z⁻¹ ↔ x ^ z = y
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>x ≤ y ^ z ↔ Real.log x ≤ z * Real.log y
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 < y<VAR>h : Real.log x ≤ z * Real.log y<GOAL>x ≤ y ^ z
<VAR>x y z : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>x < y ^ z ↔ Real.log x < z * Real.log y
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 < y<VAR>h : Real.log x < z * Real.log y<GOAL>x < y ^ z
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y
<VAR>x t : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>ht : 0 < t<GOAL>|Real.log x * x ^ t| < 1 / t
<VAR>x ε : ℝ<VAR>hx : 0 ≤ x<VAR>hε : 0 < ε<GOAL>Real.log x ≤ x ^ ε / ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>Real.log ↑n ≤ ↑n ^ ε / ε
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>StrictMono fun x => b ^ x
<VAR>b : ℝ<VAR>hb : 1 ≤ b<GOAL>Monotone fun x => b ^ x
<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>StrictAnti fun x => b ^ x
<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b ≤ 1<GOAL>Antitone fun x => b ^ x
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>‖Complex.log ↑n‖ ≤ ↑n ^ ε / ε
<VAR>x : ℝ<GOAL>√x = x ^ (1 / 2)
<VAR>x : ℝ<VAR>r : ℝ<VAR>hx : 0 ≤ x<GOAL>x ^ (r / 2) = √x ^ r
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℚ<VAR>h : x < y<VAR>hy : 0 < y<GOAL>∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>x : ℂ<GOAL>(x ^ 2⁻¹).re = √((Complex.abs x + x.re) / 2)
<VAR>x : ℂ<VAR>hx : 0 ≤ x.im<GOAL>(x ^ 2⁻¹).im = √((Complex.abs x - x.re) / 2)
<VAR>x : ℂ<VAR>hx : x.im < 0<GOAL>(x ^ 2⁻¹).im = -√((Complex.abs x - x.re) / 2)
<VAR>x : ℂ<GOAL>|(x ^ 2⁻¹).im| = √((Complex.abs x - x.re) / 2)
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsNat b nb<VAR>pe' : Mathlib.Meta.NormNum.IsNat (a ^ nb) ne<GOAL>Mathlib.Meta.NormNum.IsNat (a ^ b) ne
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)<VAR>pe' : Mathlib.Meta.NormNum.IsNat (a ^ Int.negOfNat nb) ne<GOAL>Mathlib.Meta.NormNum.IsNat (a ^ b) ne
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsNat b nb<VAR>pe' : Mathlib.Meta.NormNum.IsInt (a ^ nb) (Int.negOfNat ne)<GOAL>Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)<VAR>pe' : Mathlib.Meta.NormNum.IsInt (a ^ Int.negOfNat nb) (Int.negOfNat ne)<GOAL>Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)
<VAR>a b : ℝ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsNat b nb<VAR>pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb) num den<GOAL>Mathlib.Meta.NormNum.IsRat (a ^ b) num den
<VAR>a b : ℝ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)<VAR>pe' : Mathlib.Meta.NormNum.IsRat (a ^ Int.negOfNat nb) num den<GOAL>Mathlib.Meta.NormNum.IsRat (a ^ b) num den
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>0 ≤ PiTensorProduct.projectiveSeminormAux p
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>PiTensorProduct.projectiveSeminormAux (p + q) ≤ PiTensorProduct.projectiveSeminormAux p + PiTensorProduct.projectiveSeminormAux q
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : 𝕜<GOAL>PiTensorProduct.projectiveSeminormAux (List.map (fun y => (a * y.1, y.2)) p) = ‖a‖ * PiTensorProduct.projectiveSeminormAux p
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>BddBelow (Set.range fun p => PiTensorProduct.projectiveSeminormAux ↑p)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>PiTensorProduct.projectiveSeminorm x = ⨅ p, PiTensorProduct.projectiveSeminormAux ↑p
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>m : (i : ι) → E i<GOAL>PiTensorProduct.projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i : ι, ‖m i‖
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖(PiTensorProduct.lift f.toMultilinearMap) x‖ ≤ PiTensorProduct.projectiveSeminorm x * ‖f‖
<VAR>b : ℂ<VAR>c T : ℝ<GOAL>‖cexp (-b * (↑T + ↑c * Complex.I) ^ 2)‖ = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))
<VAR>b : ℂ<VAR>hb : b.re ≠ 0<VAR>c T : ℝ<GOAL>‖cexp (-b * (↑T + ↑c * Complex.I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<VAR>T : ℝ<VAR>hT : 0 ≤ T<GOAL>‖GaussianFourier.verticalIntegral b c T‖ ≤ 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Filter.Tendsto (GaussianFourier.verticalIntegral b c) Filter.atTop (𝓝 0)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>MeasureTheory.Integrable (fun x => cexp (-b * (↑x + ↑c * Complex.I) ^ 2)) MeasureTheory.volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>∫ (x : ℝ), cexp (-b * (↑x + ↑c * Complex.I) ^ 2) = (↑π / b) ^ (1 / 2)
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<GOAL>MeasureTheory.Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) MeasureTheory.volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c d : ℂ<GOAL>MeasureTheory.Integrable (fun x => cexp (-b * ↑x ^ 2 + c * ↑x + d)) MeasureTheory.volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>t : ℂ<GOAL>∫ (x : ℝ), cexp (Complex.I * t * ↑x) * cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<GOAL>(𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + Complex.I * c) ^ 2)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>MeasureTheory.Integrable (fun v => cexp (-∑ i : ι, b i * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) MeasureTheory.volume
<VAR>b : ℂ<VAR>ι : Type u_2<VAR>Fintype ι<VAR>hb : 0 < b.re<VAR>c : ι → ℂ<GOAL>MeasureTheory.Integrable (fun v => cexp (-b * ∑ i : ι, ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) MeasureTheory.volume
<VAR>b : ℂ<VAR>ι : Type u_2<VAR>Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<GOAL>MeasureTheory.Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) MeasureTheory.volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<GOAL>MeasureTheory.Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) MeasureTheory.volume
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>∫ (v : ι → ℝ), cexp (-∑ i : ι, b i * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i)) = ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
<VAR>b : ℂ<VAR>ι : Type u_2<VAR>Fintype ι<VAR>hb : 0 < b.re<VAR>c : ι → ℂ<GOAL>∫ (v : ι → ℝ), cexp (-b * ∑ i : ι, ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i)) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i : ι, c i ^ 2) / (4 * b))
<VAR>b : ℂ<VAR>ι : Type u_2<VAR>Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<GOAL>∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))