ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<GOAL>ContDiff ℝ n ↑PartialHomeomorph.univUnitBall
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<GOAL>ContDiffOn ℝ n (↑PartialHomeomorph.univUnitBall.symm) (Metric.ball 0 1)
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<GOAL>ContDiff ℝ n fun x => ↑(Homeomorph.unitBall x)
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>c : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>ContDiff ℝ n ↑(PartialHomeomorph.unitBallBall c r hr)
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>c : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>ContDiff ℝ n ↑(PartialHomeomorph.unitBallBall c r hr).symm
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>c : E<VAR>r : ℝ<GOAL>ContDiff ℝ n ↑(PartialHomeomorph.univBall c r)
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>c : E<VAR>r : ℝ<GOAL>ContDiffOn ℝ n (↑(PartialHomeomorph.univBall c r).symm) (Metric.ball c r)
<VAR>ι : Type u_2<VAR>self : BoxIntegral.Box ι<VAR>i : ι<GOAL>self.lower i < self.upper i
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>I.lower ≤ I.upper
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<GOAL>I.lower i ≠ I.upper i
<VAR>ι : Type u_1<VAR>l u x : ι → ℝ<VAR>H : ∀ (i : ι), l i < u i<GOAL>x ∈ { lower := l, upper := u, lower_lt_upper := H } ↔ ∀ (i : ι), x i ∈ Set.Ioc (l i) (u i)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>x : ι → ℝ<GOAL>x ∈ ↑I ↔ x ∈ I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>x : ι → ℝ<GOAL>x ∈ I ↔ ∀ (i : ι), x i ∈ Set.Ioc (I.lower i) (I.upper i)
<VAR>ι : Type u_1<VAR>x : ι → ℝ<VAR>I : BoxIntegral.Box ι<GOAL>(x ∈ Set.univ.pi fun i => Set.Ioc (I.lower i) (I.upper i)) ↔ x ∈ I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>↑I = Set.univ.pi fun i => Set.Ioc (I.lower i) (I.upper i)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>I.upper ∈ I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>∃ x, x ∈ I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>(↑I).Nonempty
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>↑I ≠ ∅
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>∅ ≠ ↑I
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>I ≤ J ↔ ∀ x ∈ I, x ∈ J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>[I ≤ J, ↑I ⊆ ↑J, Set.Icc I.lower I.upper ⊆ Set.Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>↑I ⊆ ↑J ↔ I ≤ J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>I ≤ J ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
<VAR>ι : Type u_1<GOAL>Function.Injective BoxIntegral.Box.toSet
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>↑I = ↑J ↔ I = J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>H : ∀ (x : ι → ℝ), x ∈ I ↔ x ∈ J<GOAL>I = J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>h : Disjoint ↑I ↑J<GOAL>I ≠ J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>BoxIntegral.Box.Icc I = Set.Icc I.lower I.upper
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>I.upper ∈ BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>I.lower ∈ BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>IsCompact (BoxIntegral.Box.Icc I)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>BoxIntegral.Box.Icc I = Set.univ.pi fun i => Set.Icc (I.lower i) (I.upper i)
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>I ≤ J ↔ BoxIntegral.Box.Icc I ⊆ BoxIntegral.Box.Icc J
<VAR>ι : Type u_1<GOAL>Antitone fun I => I.lower
<VAR>ι : Type u_1<GOAL>Monotone fun I => I.upper
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>↑I ⊆ BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<GOAL>↑⊥ = ∅
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>↑↑I = ↑I
<VAR>ι : Type u_1<VAR>I : WithBot (BoxIntegral.Box ι)<GOAL>Option.isSome I = true ↔ (↑I).Nonempty
<VAR>ι : Type u_1<VAR>I : WithBot (BoxIntegral.Box ι)<GOAL>⋃ J, ⋃ (_ : ↑J = I), ↑J = ↑I
<VAR>ι : Type u_1<VAR>I J : WithBot (BoxIntegral.Box ι)<GOAL>↑I ⊆ ↑J ↔ I ≤ J
<VAR>ι : Type u_1<VAR>I J : WithBot (BoxIntegral.Box ι)<GOAL>↑I = ↑J ↔ I = J
<VAR>ι : Type u_1<VAR>l u : ι → ℝ<GOAL>BoxIntegral.Box.mk' l u = ⊥ ↔ ∃ i, u i ≤ l i
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>l u : ι → ℝ<GOAL>BoxIntegral.Box.mk' l u = ↑I ↔ l = I.lower ∧ u = I.upper
<VAR>ι : Type u_1<VAR>l u : ι → ℝ<GOAL>↑(BoxIntegral.Box.mk' l u) = Set.univ.pi fun i => Set.Ioc (l i) (u i)
<VAR>ι : Type u_1<VAR>I J : WithBot (BoxIntegral.Box ι)<GOAL>↑(I ⊓ J) = ↑I ∩ ↑J
<VAR>ι : Type u_1<VAR>I J : WithBot (BoxIntegral.Box ι)<GOAL>Disjoint ↑I ↑J ↔ Disjoint I J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>Disjoint ↑I ↑J ↔ Disjoint ↑I ↑J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>¬Disjoint ↑I ↑J ↔ (↑I ∩ ↑J).Nonempty
<VAR>n : ℕ<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>i : Fin (n + 1)<GOAL>∀ (a : Fin n), (I.face i).lower a = I.lower (i.succAbove a)
<VAR>n : ℕ<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>i : Fin (n + 1)<GOAL>∀ (a : Fin n), (I.face i).upper a = I.upper (i.succAbove a)
<VAR>n : ℕ<VAR>l u : Fin (n + 1) → ℝ<VAR>h : ∀ (i : Fin (n + 1)), l i < u i<VAR>i : Fin (n + 1)<GOAL>{ lower := l, upper := u, lower_lt_upper := h }.face i = { lower := l ∘ i.succAbove, upper := u ∘ i.succAbove, lower_lt_upper := ⋯ }
<VAR>n : ℕ<VAR>I J : BoxIntegral.Box (Fin (n + 1))<VAR>h : I ≤ J<VAR>i : Fin (n + 1)<GOAL>I.face i ≤ J.face i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>Monotone fun I => I.face i
<VAR>n : ℕ<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc (I.lower i) (I.upper i)<GOAL>Set.MapsTo (i.insertNth x) (BoxIntegral.Box.Icc (I.face i)) (BoxIntegral.Box.Icc I)
<VAR>n : ℕ<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioc (I.lower i) (I.upper i)<GOAL>Set.MapsTo (i.insertNth x) ↑(I.face i) ↑I
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>f : (Fin (n + 1) → ℝ) → X<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>h : ContinuousOn f (BoxIntegral.Box.Icc I)<VAR>i : Fin (n + 1)<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc (I.lower i) (I.upper i)<GOAL>ContinuousOn (f ∘ i.insertNth x) (BoxIntegral.Box.Icc (I.face i))
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>BoxIntegral.Box.Ioo I ⊆ ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>BoxIntegral.Box.Ioo I ⊆ BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<VAR>Finite ι<VAR>I : BoxIntegral.Box ι<VAR>J : ℕ → BoxIntegral.Box ι<VAR>hJ : Monotone J<VAR>hl : Filter.Tendsto (BoxIntegral.Box.lower ∘ J) Filter.atTop (𝓝 I.lower)<VAR>hu : Filter.Tendsto (BoxIntegral.Box.upper ∘ J) Filter.atTop (𝓝 I.upper)<GOAL>⋃ n, BoxIntegral.Box.Ioo (J n) = BoxIntegral.Box.Ioo I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>∃ J, (∀ (n : ℕ), BoxIntegral.Box.Icc (J n) ⊆ BoxIntegral.Box.Ioo I) ∧ Filter.Tendsto (BoxIntegral.Box.lower ∘ ⇑J) Filter.atTop (𝓝 I.lower) ∧ Filter.Tendsto (BoxIntegral.Box.upper ∘ ⇑J) Filter.atTop (𝓝 I.upper)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I J : BoxIntegral.Box ι<VAR>r : ℝ<VAR>h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r<GOAL>I.distortion = J.distortion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>i : ι<GOAL>nndist I.lower I.upper ≤ I.distortion * nndist (I.lower i) (I.upper i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>i : ι<GOAL>dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>c : ℝ≥0<VAR>h : I.distortion ≤ c<GOAL>Metric.diam (BoxIntegral.Box.Icc I) ≤ ↑c * (I.upper i - I.lower i)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<GOAL>y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Set ι<GOAL>I.splitCenterBox s ≤ I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s t : Set ι<VAR>h : s ≠ t<GOAL>Disjoint ↑(I.splitCenterBox s) ↑(I.splitCenterBox t)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>Function.Injective I.splitCenterBox
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>x : ι → ℝ<GOAL>(∃ s, x ∈ I.splitCenterBox s) ↔ x ∈ I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Set ι<GOAL>I.splitCenterBoxEmb s = I.splitCenterBox s
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>⋃ s, ↑(I.splitCenterBox s) = ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Set ι<VAR>i : ι<GOAL>(I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
<VAR>ι : Type u_1<VAR>p : BoxIntegral.Box ι → Prop<VAR>I : BoxIntegral.Box ι<VAR>H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J<VAR>H_nhds : ∀ z ∈ BoxIntegral.Box.Icc I, ∃ U ∈ 𝓝[BoxIntegral.Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ BoxIntegral.Box.Icc J → BoxIntegral.Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<GOAL>p I
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>u : A<GOAL>u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑circle
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>u : A<VAR>IsStarNormal u<VAR>hu : spectrum ℂ u ⊆ ↑circle<GOAL>u ∈ unitary A
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>u : A<VAR>hu : u ∈ unitary A<GOAL>spectrum ℂ u ⊆ ↑circle
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>self : InnerProductSpaceable E<VAR>x y : E<GOAL>‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>InnerProductSpaceable E
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>InnerProductSpaceable.innerProp' E ↑(-1)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : ℝ → E<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => inner_ 𝕜 (f x) (g x)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>‖x‖ ^ 2 = RCLike.re (inner_ 𝕜 x x)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x y : E<GOAL>(starRingEnd 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpaceable E<VAR>x y z : E<GOAL>‖x + y + z‖ * ‖x + y + z‖ = (‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) / 2 - ‖x - z‖ * ‖x - z‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpaceable E<VAR>x y z : E<GOAL>‖x + y - z‖ * ‖x + y - z‖ = (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 - ‖x + z‖ * ‖x + z‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpaceable E<VAR>x y z : E<GOAL>‖x + y + z‖ * ‖x + y + z‖ - ‖x + y - z‖ * ‖x + y - z‖ = ‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖ + (‖2 • z + y‖ * ‖2 • z + y‖ - ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpaceable E<VAR>y z : E<GOAL>‖2 • z + y‖ * ‖2 • z + y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpaceable E<VAR>y z : E<GOAL>‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpaceable E<VAR>y z : E<GOAL>(‖2 • z + y‖ * ‖2 • z + y‖ - ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 = ‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>x y z : E<GOAL>‖RCLike.I • (x + y) + z‖ * ‖RCLike.I • (x + y) + z‖ = (‖RCLike.I • (2 • x + y)‖ * ‖RCLike.I • (2 • x + y)‖ + ‖RCLike.I • y + 2 • z‖ * ‖RCLike.I • y + 2 • z‖) / 2 - ‖RCLike.I • x - z‖ * ‖RCLike.I • x - z‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>x y z : E<GOAL>‖RCLike.I • (x + y) - z‖ * ‖RCLike.I • (x + y) - z‖ = (‖RCLike.I • (2 • x + y)‖ * ‖RCLike.I • (2 • x + y)‖ + ‖RCLike.I • y - 2 • z‖ * ‖RCLike.I • y - 2 • z‖) / 2 - ‖RCLike.I • x + z‖ * ‖RCLike.I • x + z‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>y z : E<GOAL>‖RCLike.I • y + 2 • z‖ * ‖RCLike.I • y + 2 • z‖ = 2 * (‖RCLike.I • y + z‖ * ‖RCLike.I • y + z‖ + ‖z‖ * ‖z‖) - ‖RCLike.I • y‖ * ‖RCLike.I • y‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>y z : E<GOAL>‖RCLike.I • y - 2 • z‖ * ‖RCLike.I • y - 2 • z‖ = 2 * (‖RCLike.I • y - z‖ * ‖RCLike.I • y - z‖ + ‖z‖ * ‖z‖) - ‖RCLike.I • y‖ * ‖RCLike.I • y‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>x y z : E<GOAL>inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>n : ℕ<VAR>x y : E<GOAL>inner_ 𝕜 (↑n • x) y = ↑n * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>r : ℕ<GOAL>InnerProductSpaceable.innerProp' E ↑r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>n : ℤ<GOAL>InnerProductSpaceable.innerProp' E ↑n
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>r : ℚ<GOAL>InnerProductSpaceable.innerProp' E ↑r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>r : ℝ<GOAL>InnerProductSpaceable.innerProp' E ↑r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<GOAL>InnerProductSpaceable.innerProp' E RCLike.I
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<VAR>r : 𝕜<GOAL>InnerProductSpaceable.innerProp' E r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>InnerProductSpaceable E<GOAL>Nonempty (InnerProductSpace 𝕜 E)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>ContinuousStar A<VAR>CompleteSpace A<VAR>StarModule ℂ A<VAR>a : ↥(selfAdjoint A)<GOAL>↑(selfAdjoint.expUnitary a) = NormedSpace.exp ℂ (Complex.I • ↑a)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>ContinuousStar A<VAR>CompleteSpace A<VAR>StarModule ℂ A<VAR>a b : ↥(selfAdjoint A)<VAR>h : Commute ↑a ↑b<GOAL>selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary a * selfAdjoint.expUnitary b
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>ContinuousStar A<VAR>CompleteSpace A<VAR>StarModule ℂ A<VAR>a b : ↥(selfAdjoint A)<VAR>h : Commute ↑a ↑b<GOAL>Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>MeasurableSpace M<VAR>BorelSpace M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>f : M → F<VAR>μ : MeasureTheory.Measure M<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>MeasurableSpace M<VAR>BorelSpace M<VAR>T2Space M<VAR>f : M → F<VAR>μ : MeasureTheory.Measure M<VAR>U : Set M<VAR>hU : IsOpen U<VAR>hSig : IsSigmaCompact U<VAR>hf : MeasureTheory.LocallyIntegrableOn f U μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>MeasurableSpace M<VAR>BorelSpace M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>f : M → F<VAR>μ : MeasureTheory.Measure M<VAR>U : Set M<VAR>hU : IsOpen U<VAR>hf : MeasureTheory.LocallyIntegrableOn f U μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>MeasurableSpace M<VAR>BorelSpace M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>f f' : M → F<VAR>μ : MeasureTheory.Measure M<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hf' : MeasureTheory.LocallyIntegrable f' μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ<GOAL>∀ᵐ (x : M) ∂μ, f x = f' x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : E → F<VAR>μ : MeasureTheory.Measure E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : E) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f f' : E → F<VAR>μ : MeasureTheory.Measure E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hf' : MeasureTheory.LocallyIntegrable f' μ<VAR>h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = ∫ (x : E), g x • f' x ∂μ<GOAL>∀ᵐ (x : E) ∂μ, f x = f' x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : E → F<VAR>μ : MeasureTheory.Measure E<VAR>U : Set E<VAR>hU : IsOpen U<VAR>hf : MeasureTheory.LocallyIntegrableOn f U μ<VAR>h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : E), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : E) ∂μ, x ∈ U → f x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℂ 𝕜 E<VAR>c : 𝕜<GOAL>MellinConvergent (fun t => c • f t) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s a : ℂ<GOAL>MellinConvergent (fun t => ↑t ^ a • f t) s ↔ MellinConvergent f (s + a)
<VAR>f : ℝ → ℂ<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>a : ℂ<GOAL>MellinConvergent (fun t => f t / a) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / ↑a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s a : ℂ<GOAL>mellin (fun t => ↑t ^ a • f t) s = mellin f (s + a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℂ 𝕜 E<VAR>c : 𝕜<GOAL>mellin (fun t => c • f t) s = c • mellin f s
<VAR>f : ℝ → ℂ<VAR>s a : ℂ<GOAL>mellin (fun t => f t / a) s = mellin f s / a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<GOAL>mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>mellin (fun t => f (a * t)) s = ↑a ^ (-s) • mellin f s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>mellin (fun t => f (t * a)) s = ↑a ^ (-s) • mellin f s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>mellin (fun t => f t⁻¹) s = mellin f (-s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℝ → E<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>hg : MellinConvergent g s<GOAL>HasMellin (fun t => f t + g t) s (mellin f s + mellin g s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℝ → E<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>hg : MellinConvergent g s<GOAL>HasMellin (fun t => f t - g t) s (mellin f s - mellin g s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>T : Set ℝ<VAR>hT : T ⊆ Set.Ioi 0<VAR>hT' : MeasurableSet T<VAR>hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))<VAR>s : ℂ<GOAL>MeasureTheory.IntegrableOn (fun t => ↑t ^ (s - 1) • f t) T MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) T MeasureTheory.volume
<VAR>f : ℝ → ℝ<VAR>hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))<VAR>a s : ℝ<VAR>hf : f =O[Filter.atTop] fun x => x ^ (-a)<VAR>hs : s < a<GOAL>∃ c, 0 < c ∧ MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioi c) MeasureTheory.volume
<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<GOAL>∃ c, 0 < c ∧ MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioc 0 c) MeasureTheory.volume
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>s : ℝ<VAR>hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume<VAR>hf_top : f =O[Filter.atTop] fun x => x ^ (-a)<VAR>hs_top : s < a<VAR>hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>hs_bot : b < s<GOAL>MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioi 0) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>s : ℂ<VAR>hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume<VAR>hf_top : f =O[Filter.atTop] fun x => x ^ (-a)<VAR>hs_top : s.re < a<VAR>hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>hs_bot : b < s.re<GOAL>MellinConvergent f s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : b < a<VAR>hf : f =O[Filter.atTop] fun x => x ^ (-a)<GOAL>(fun t => Real.log t • f t) =O[Filter.atTop] fun x => x ^ (-b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : a < b<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-a)<GOAL>(fun t => Real.log t • f t) =O[𝓝[>] 0] fun x => x ^ (-b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>s : ℂ<VAR>hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume<VAR>hf_top : f =O[Filter.atTop] fun x => x ^ (-a)<VAR>hs_top : s.re < a<VAR>hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>hs_bot : b < s.re<GOAL>MellinConvergent (fun t => Real.log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t => Real.log t • f t) s) s