ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>DifferentiableAt ℂ (mellin f) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>f : ℝ → E<VAR>s : ℂ<VAR>hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume<VAR>hf_top : f =O[Filter.atTop] fun t => rexp (-a * t)<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>ha : 0 < a<VAR>f : ℝ → E<VAR>s : ℂ<VAR>hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume<VAR>hf_top : f =O[Filter.atTop] fun t => rexp (-a * t)<VAR>hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>hs_bot : b < s.re<GOAL>DifferentiableAt ℂ (mellin f) s
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>HasMellin ((Set.Ioc 0 1).indicator fun x => 1) s (1 / s)
<VAR>a : ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re + a.re<GOAL>HasMellin ((Set.Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in Filter.atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Filter.Tendsto c Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun n => u (c n) / ↑(c n)) Filter.atTop (𝓝 l)<GOAL>Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Filter.Tendsto c Filter.atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Filter.Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) Filter.atTop (𝓝 l)<GOAL>Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (𝓝 l)
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<GOAL>∑ i ∈ Finset.filter (fun x => j < c ^ x) (Finset.range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<GOAL>∑ i ∈ Finset.filter (fun x => j < ↑⌊c ^ x⌋₊) (Finset.range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
<VAR>f : ℕ → ℝ<GOAL>(∃ r, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, |f i|) Filter.atTop (𝓝 r)) → Summable f
<VAR>𝕜 : Type u_4<VAR>NormedAddCommGroup 𝕜<GOAL>Filter.Tendsto norm (𝓝[≠] 0) (𝓝[>] 0)
<VAR>𝕜 : Type u_4<VAR>NormedDivisionRing 𝕜<GOAL>Filter.Tendsto (fun x => ‖x⁻¹‖) (𝓝[≠] 0) Filter.atTop
<VAR>𝕜 : Type u_4<VAR>NormedDivisionRing 𝕜<VAR>m : ℤ<VAR>hm : m < 0<GOAL>Filter.Tendsto (fun x => ‖x ^ m‖) (𝓝[≠] 0) Filter.atTop
<VAR>ι : Type u_4<VAR>𝕜 : Type u_5<VAR>𝔸 : Type u_6<VAR>NormedDivisionRing 𝕜<VAR>NormedAddCommGroup 𝔸<VAR>Module 𝕜 𝔸<VAR>BoundedSMul 𝕜 𝔸<VAR>l : Filter ι<VAR>ε : ι → 𝕜<VAR>f : ι → 𝔸<VAR>hε : Filter.Tendsto ε l (𝓝 0)<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<GOAL>Filter.Tendsto (ε • f) l (𝓝 0)
<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<GOAL>ContinuousAt (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>ContinuousAt Inv.inv x ↔ x ≠ 0
<VAR>r₁ r₂ : ℝ<VAR>h₁ : 0 ≤ r₁<VAR>h₂ : r₁ < r₂<GOAL>(fun n => r₁ ^ n) =o[Filter.atTop] fun n => r₂ ^ n
<VAR>r₁ r₂ : ℝ<VAR>h₁ : 0 ≤ r₁<VAR>h₂ : r₁ ≤ r₂<GOAL>(fun n => r₁ ^ n) =O[Filter.atTop] fun n => r₂ ^ n
<VAR>r₁ r₂ : ℝ<VAR>h : |r₁| < |r₂|<GOAL>(fun n => r₁ ^ n) =o[Filter.atTop] fun n => r₂ ^ n
<VAR>f : ℕ → ℝ<VAR>R : ℝ<GOAL>[∃ a ∈ Set.Ioo (-R) R, f =o[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo (-R) R, f =O[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[Filter.atTop] fun x => a ^ x, ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n, ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n].TFAE
<VAR>R : Type u_4<VAR>NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<GOAL>(fun n => ↑n ^ k) =o[Filter.atTop] fun n => r ^ n
<VAR>R : Type u_4<VAR>NormedRing R<VAR>r : ℝ<VAR>hr : 1 < r<GOAL>Nat.cast =o[Filter.atTop] fun n => r ^ n
<VAR>R : Type u_4<VAR>NormedRing R<VAR>k : ℕ<VAR>r₁ : R<VAR>r₂ : ℝ<VAR>h : ‖r₁‖ < r₂<GOAL>(fun n => ↑n ^ k * r₁ ^ n) =o[Filter.atTop] fun n => r₂ ^ n
<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<GOAL>Filter.Tendsto (fun n => ↑n ^ k / r ^ n) Filter.atTop (𝓝 0)
<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : |r| < 1<GOAL>Filter.Tendsto (fun n => ↑n ^ k * r ^ n) Filter.atTop (𝓝 0)
<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>h'r : r < 1<GOAL>Filter.Tendsto (fun n => ↑n ^ k * r ^ n) Filter.atTop (𝓝 0)
<VAR>r : ℝ<VAR>hr : |r| < 1<GOAL>Filter.Tendsto (fun n => ↑n * r ^ n) Filter.atTop (𝓝 0)
<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>h'r : r < 1<GOAL>Filter.Tendsto (fun n => ↑n * r ^ n) Filter.atTop (𝓝 0)
<VAR>R : Type u_4<VAR>NormedRing R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>Filter.Tendsto (fun n => x ^ n) Filter.atTop (𝓝 0)
<VAR>r : ℝ<VAR>h : |r| < 1<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0)
<VAR>K : Type u_4<VAR>NormedDivisionRing K<VAR>ξ : K<VAR>h : ‖ξ‖ < 1<GOAL>HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
<VAR>K : Type u_4<VAR>NormedDivisionRing K<VAR>ξ : K<VAR>h : ‖ξ‖ < 1<GOAL>Summable fun n => ξ ^ n
<VAR>K : Type u_4<VAR>NormedDivisionRing K<VAR>ξ : K<VAR>h : ‖ξ‖ < 1<GOAL>∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹
<VAR>r : ℝ<VAR>h : |r| < 1<GOAL>HasSum (fun n => r ^ n) (1 - r)⁻¹
<VAR>r : ℝ<VAR>h : |r| < 1<GOAL>Summable fun n => r ^ n
<VAR>r : ℝ<VAR>h : |r| < 1<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<VAR>K : Type u_4<VAR>NormedDivisionRing K<VAR>ξ : K<GOAL>(Summable fun n => ξ ^ n) ↔ ‖ξ‖ < 1
<VAR>R : Type u_4<VAR>NormedRing R<VAR>k : ℕ<VAR>r : R<VAR>hr : ‖r‖ < 1<GOAL>Summable fun n => ‖↑n ^ k * r ^ n‖
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>k : ℕ<VAR>r : R<VAR>hr : ‖r‖ < 1<GOAL>Summable fun n => ↑n ^ k * r ^ n
<VAR>𝕜 : Type u_4<VAR>NormedDivisionRing 𝕜<VAR>CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<GOAL>HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
<VAR>𝕜 : Type u_4<VAR>NormedDivisionRing 𝕜<VAR>CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<GOAL>∑' (n : ℕ), ↑n * r ^ n = r / (1 - r) ^ 2
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>C r : ℝ<VAR>hr : r < 1<VAR>u : ℕ → α<VAR>h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n<GOAL>CauchySeq u
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<VAR>n : ℕ<GOAL>dist (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hr : r < 1<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<GOAL>CauchySeq fun s => ∑ x ∈ s, f x
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hr : r < 1<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<VAR>a : α<VAR>ha : HasSum f a<VAR>n : ℕ<GOAL>‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>dist (∑ k ∈ Finset.range (n + 1), u k) (∑ k ∈ Finset.range n, u k) = ‖u n‖
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>r : ℝ<VAR>hr : r < 1<VAR>h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range n, u k
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>r : ℝ<VAR>hr : r < 1<VAR>h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>N : ℕ<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k<GOAL>∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>Summable fun n => x ^ n
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>(∑' (i : ℕ), x ^ i) * (1 - x) = 1
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>(1 - x) * ∑' (i : ℕ), x ^ i = 1
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)
<VAR>R : Type u_4<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>(1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1
<VAR>α : Type u_4<VAR>SeminormedAddCommGroup α<VAR>CompleteSpace α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr₁ : r < 1<VAR>h : ∀ᶠ (n : ℕ) in Filter.atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖<GOAL>Summable f
<VAR>α : Type u_4<VAR>NormedAddCommGroup α<VAR>CompleteSpace α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl₁ : l < 1<VAR>hf : ∀ᶠ (n : ℕ) in Filter.atTop, f n ≠ 0<VAR>h : Filter.Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) Filter.atTop (𝓝 l)<GOAL>Summable f
<VAR>α : Type u_4<VAR>SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∃ᶠ (n : ℕ) in Filter.atTop, ‖f n‖ ≠ 0<VAR>h : ∀ᶠ (n : ℕ) in Filter.atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖<GOAL>¬Summable f
<VAR>α : Type u_4<VAR>SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl : 1 < l<VAR>h : Filter.Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) Filter.atTop (𝓝 l)<GOAL>¬Summable f
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>CompleteSpace α<VAR>f : ℕ → α<VAR>w z : α<VAR>h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i<VAR>hz : ‖z‖ < ‖w‖<GOAL>Summable fun n => f n * z ^ n
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>CompleteSpace α<VAR>f : ℕ → α<VAR>z : α<VAR>h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i<VAR>hz : ‖z‖ < 1<GOAL>Summable fun n => f n * z ^ n
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, f i • z i
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Antitone f<VAR>hf0 : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>hzb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, f i • z i
<VAR>n : ℕ<GOAL>‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1
<VAR>f : ℕ → ℝ<VAR>hfa : Monotone f<VAR>hf0 : Filter.Tendsto f Filter.atTop (𝓝 0)<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i
<VAR>f : ℕ → ℝ<VAR>hfa : Monotone f<VAR>hf0 : Filter.Tendsto f Filter.atTop (𝓝 0)<GOAL>∃ l, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>hfa : Antitone f<VAR>hf0 : Filter.Tendsto f Filter.atTop (𝓝 0)<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i
<VAR>f : ℕ → ℝ<VAR>hfa : Antitone f<VAR>hf0 : Filter.Tendsto f Filter.atTop (𝓝 0)<GOAL>∃ l, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (𝓝 l)
<VAR>E : Type u_4<VAR>OrderedRing E<VAR>TopologicalSpace E<VAR>OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (𝓝 l)<VAR>hfm : Monotone f<VAR>k : ℕ<GOAL>l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i
<VAR>E : Type u_4<VAR>OrderedRing E<VAR>TopologicalSpace E<VAR>OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (𝓝 l)<VAR>hfm : Monotone f<VAR>k : ℕ<GOAL>∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i ≤ l
<VAR>E : Type u_4<VAR>OrderedRing E<VAR>TopologicalSpace E<VAR>OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (𝓝 l)<VAR>hfa : Antitone f<VAR>k : ℕ<GOAL>∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l
<VAR>E : Type u_4<VAR>OrderedRing E<VAR>TopologicalSpace E<VAR>OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (𝓝 l)<VAR>hfa : Antitone f<VAR>k : ℕ<GOAL>l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
<VAR>x : ℝ<GOAL>Summable fun n => x ^ n / ↑n !
<VAR>x : ℝ<GOAL>Filter.Tendsto (fun n => x ^ n / ↑n !) Filter.atTop (𝓝 0)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>StarAddMonoid E<VAR>self : NormedStarGroup E<VAR>x : E<GOAL>‖x⋆‖ = ‖x‖
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>StarAddMonoid E<VAR>NormedStarGroup E<VAR>x : E<GOAL>‖x⋆‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>StarAddMonoid E<VAR>NormedStarGroup E<GOAL>Isometry star
<VAR>E : Type u_4<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>self : CstarRing E<VAR>x : E<GOAL>‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>‖x⋆ * x‖ = ‖x‖ * ‖x‖
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>‖x * x⋆‖ = ‖x‖ * ‖x‖
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>‖x * x⋆‖₊ = ‖x‖₊ * ‖x‖₊
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>‖x⋆ * x‖₊ = ‖x‖₊ * ‖x‖₊
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>x⋆ * x = 0 ↔ x = 0
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>x⋆ * x ≠ 0 ↔ x ≠ 0
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>x * x⋆ = 0 ↔ x = 0
<VAR>E : Type u_2<VAR>NonUnitalNormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<GOAL>x * x⋆ ≠ 0 ↔ x ≠ 0
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>Nontrivial E<GOAL>‖1‖ = 1
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>Nontrivial E<VAR>U : ↥(unitary E)<GOAL>‖↑U‖ = 1
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>Nontrivial E<VAR>U : E<VAR>hU : U ∈ unitary E<GOAL>‖U‖ = 1
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>U : ↥(unitary E)<VAR>A : E<GOAL>‖↑U * A‖ = ‖A‖
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>U : ↥(unitary E)<VAR>A : E<GOAL>‖U • A‖ = ‖A‖
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>U : E<VAR>A : E<VAR>hU : U ∈ unitary E<GOAL>‖U * A‖ = ‖A‖
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>A : E<VAR>U : ↥(unitary E)<GOAL>‖A * ↑U‖ = ‖A‖
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>A : E<VAR>U : E<VAR>hU : U ∈ unitary E<GOAL>‖A * U‖ = ‖A‖
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : E<VAR>hx : IsSelfAdjoint x<VAR>n : ℕ<GOAL>‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>x : ↥(selfAdjoint E)<VAR>n : ℕ<GOAL>‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>CommSemiring 𝕜<VAR>StarRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>StarAddMonoid E<VAR>NormedStarGroup E<VAR>Module 𝕜 E<VAR>StarModule 𝕜 E<GOAL>⇑(starₗᵢ 𝕜) = star
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>CommSemiring 𝕜<VAR>StarRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>StarAddMonoid E<VAR>NormedStarGroup E<VAR>Module 𝕜 E<VAR>StarModule 𝕜 E<VAR>x : E<GOAL>(starₗᵢ 𝕜) x = x⋆
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>CommSemiring 𝕜<VAR>StarRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>StarAddMonoid E<VAR>NormedStarGroup E<VAR>Module 𝕜 E<VAR>StarModule 𝕜 E<GOAL>(starₗᵢ 𝕜).toContinuousLinearEquiv = starL 𝕜
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Fact (FiniteDimensional.finrank K V = 2)<GOAL>FiniteDimensional K V
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>o.areaForm = let z := AlternatingMap.constLinearEquivOfIsEmpty.symm; let y := (LinearMap.llcomp ℝ E (E [⋀^Fin 0]→ₗ[ℝ] ℝ) ℝ) ↑z ∘ₗ AlternatingMap.curryLeftLinearMap; y ∘ₗ AlternatingMap.curryLeftLinearMap o.volumeForm
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) y = o.volumeForm ![x, y]
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(o.areaForm x) x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) y = -(o.areaForm y) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>(-o).areaForm = -o.areaForm
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>o.areaForm' x = LinearMap.toContinuousLinearMap (o.areaForm x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>|(o.areaForm x) y| ≤ ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) y ≤ ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>|(o.areaForm x) y| = ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>hF : Fact (FiniteDimensional.finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x y : F<GOAL>(((Orientation.map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>(o.areaForm (φ x)) (φ y) = (o.areaForm x) y
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>o.rightAngleRotationAux₁ = let to_dual := (InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm; ↑to_dual.symm ∘ₗ o.areaForm
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotationAux₁ x, y⟫_ℝ = (o.areaForm x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪x, o.rightAngleRotationAux₁ y⟫_ℝ = -(o.areaForm x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>o.rightAngleRotation = LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotation x, y⟫_ℝ = (o.areaForm x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪x, o.rightAngleRotation y⟫_ℝ = -(o.areaForm x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>o.rightAngleRotation (o.rightAngleRotation x) = -x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>⟪o.rightAngleRotation x, x⟫_ℝ = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪x, o.rightAngleRotation y⟫_ℝ = -⟪o.rightAngleRotation x, y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotation x, y⟫_ℝ = -⟪x, o.rightAngleRotation y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotation x, o.rightAngleRotation y⟫_ℝ = ⟪x, y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm (o.rightAngleRotation x)) y = -⟪x, y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) (o.rightAngleRotation y) = ⟪x, y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.areaForm x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>o.rightAngleRotation.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(-o).rightAngleRotation x = -o.rightAngleRotation x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>(-o).rightAngleRotation = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>hF : Fact (FiniteDimensional.finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x : F<GOAL>((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x : E<GOAL>φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>Fact (FiniteDimensional.finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<GOAL>((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<GOAL>o.rightAngleRotation.trans φ = φ.trans o.rightAngleRotation