ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : ℝ<VAR>f : ℕ → ℕ<VAR>hm : 1 < m<VAR>fi : ∀ (i : ℕ), i ≤ f i<GOAL>Summable fun i => 1 / m ^ f i
<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε
<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>Countable ι<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>Countable ι<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>Countable ι<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ε' i < ε
<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>Countable ι<VAR>w : ι → ℝ≥0∞<VAR>hw : ∀ (i : ι), w i ≠ ⊤<GOAL>∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε
<GOAL>Filter.Tendsto Nat.factorial Filter.atTop Filter.atTop
<GOAL>Filter.Tendsto (fun n => ↑n ! / ↑n ^ n) Filter.atTop (𝓝 0)
<VAR>α : Type u_4<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>Filter.Tendsto (fun x => ⌊x⌋₊) Filter.atTop Filter.atTop
<VAR>α : Type u_4<VAR>LinearOrderedSemiring α<VAR>FloorSemiring α<GOAL>Filter.Tendsto (fun x => ⌈x⌉₊) Filter.atTop Filter.atTop
<VAR>α : Type u_4<VAR>LinearOrderedSemifield α<VAR>FloorSemiring α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<GOAL>Filter.Tendsto (fun x => ⌊a * ↑x⌋₊) Filter.atTop Filter.atTop
<VAR>R : Type u_4<VAR>TopologicalSpace R<VAR>LinearOrderedField R<VAR>OrderTopology R<VAR>FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>Filter.Tendsto (fun x => ↑⌊a * x⌋₊ / x) Filter.atTop (𝓝 a)
<VAR>R : Type u_4<VAR>TopologicalSpace R<VAR>LinearOrderedField R<VAR>OrderTopology R<VAR>FloorRing R<GOAL>Filter.Tendsto (fun x => ↑⌊x⌋₊ / x) Filter.atTop (𝓝 1)
<VAR>R : Type u_4<VAR>TopologicalSpace R<VAR>LinearOrderedField R<VAR>OrderTopology R<VAR>FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>Filter.Tendsto (fun x => ↑⌈a * x⌉₊ / x) Filter.atTop (𝓝 a)
<VAR>R : Type u_4<VAR>TopologicalSpace R<VAR>LinearOrderedField R<VAR>OrderTopology R<VAR>FloorRing R<GOAL>Filter.Tendsto (fun x => ↑⌈x⌉₊ / x) Filter.atTop (𝓝 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Filter.Tendsto (fun x => x / n) Filter.atTop Filter.atTop
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<GOAL>Summable fun i => ⟪↑f i, ↑g i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<GOAL>⟪f, g⟫_𝕜 = ∑' (i : ι), ⟪↑f i, ↑g i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<GOAL>HasSum (fun i => ⟪↑f i, ↑g i⟫_𝕜) ⟪f, g⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<GOAL>⟪lp.single 2 i a, f⟫_𝕜 = ⟪a, ↑f i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<GOAL>⟪f, lp.single 2 i a⟫_𝕜 = ⟪↑f i, a⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<GOAL>Summable fun i => (V i) (↑f i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<GOAL>hV.linearIsometry f = ∑' (i : ι), (V i) (↑f i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<GOAL>HasSum (fun i => (V i) (↑f i)) (hV.linearIsometry f)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>i : ι<VAR>x : G i<GOAL>hV.linearIsometry (lp.single 2 i x) = (V i) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>∀ (i : ι), CompleteSpace (G i)<GOAL>LinearMap.range hV.linearIsometry.toLinearMap = (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>self : IsHilbertSum 𝕜 G V<GOAL>OrthogonalFamily 𝕜 G V
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>self : IsHilbertSum 𝕜 G V<GOAL>Function.Surjective ⇑⋯.linearIsometry
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>∀ (i : ι), CompleteSpace (G i)<VAR>hVortho : OrthogonalFamily 𝕜 G V<VAR>hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure<GOAL>IsHilbertSum 𝕜 G V
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>F : ι → Submodule 𝕜 E<VAR>∀ (i : ι), CompleteSpace ↥(F i)<VAR>hFortho : OrthogonalFamily 𝕜 (fun i => ↥(F i)) fun i => (F i).subtypeₗᵢ<VAR>hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure<GOAL>IsHilbertSum 𝕜 (fun i => ↥(F i)) fun i => (F i).subtypeₗᵢ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>w : ↥(lp G 2)<GOAL>hV.linearIsometryEquiv.symm w = ∑' (i : ι), (V i) (↑w i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>w : ↥(lp G 2)<GOAL>HasSum (fun i => (V i) (↑w i)) (hV.linearIsometryEquiv.symm w)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>i : ι<VAR>x : G i<GOAL>hV.linearIsometryEquiv.symm (lp.single 2 i x) = (V i) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>↑(W₀.sum fun a b => hV.linearIsometryEquiv ((V a) b)) = ⇑W₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hsp : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure<GOAL>IsHilbertSum 𝕜 (fun x => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>K : Submodule 𝕜 E<VAR>hK : CompleteSpace ↥K<GOAL>IsHilbertSum 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>i : ι<GOAL>b.repr.symm (lp.single 2 i 1) = (fun i => b.repr.symm (lp.single 2 i 1)) i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>i : ι<GOAL>b.repr ((fun i => b.repr.symm (lp.single 2 i 1)) i) = lp.single 2 i 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>v : E<VAR>i : ι<GOAL>↑(b.repr v) i = ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, v⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<GOAL>Orthonormal 𝕜 fun i => b.repr.symm (lp.single 2 i 1)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<GOAL>HasSum (fun i => ↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) (b.repr.symm f)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>x : E<GOAL>HasSum (fun i => ↑(b.repr x) i • (fun i => b.repr.symm (lp.single 2 i 1)) i) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<GOAL>(Submodule.span 𝕜 (Set.range fun i => b.repr.symm (lp.single 2 i 1))).topologicalClosure = ⊤
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>x y : E<GOAL>HasSum (fun i => ⟪x, (fun i => b.repr.symm (lp.single 2 i 1)) i⟫_𝕜 * ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, y⟫_𝕜) ⟪x, y⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>x y : E<GOAL>Summable fun i => ⟪x, (fun i => b.repr.symm (lp.single 2 i 1)) i⟫_𝕜 * ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, y⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<VAR>x y : E<GOAL>∑' (i : ι), ⟪x, (fun i => b.repr.symm (lp.single 2 i 1)) i⟫_𝕜 * ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : HilbertBasis ι 𝕜 E<GOAL>⇑b.toOrthonormalBasis = fun i => b.repr.symm (lp.single 2 i 1)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<VAR>CompleteSpace ↥U<VAR>b : HilbertBasis ι 𝕜 ↥U<VAR>x : E<GOAL>HasSum (fun i => ⟪↑((fun i => b.repr.symm (lp.single 2 i 1)) i), x⟫_𝕜 • (fun i => b.repr.symm (lp.single 2 i 1)) i) ((orthogonalProjection U) x)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>b : HilbertBasis ι 𝕜 E<GOAL>(⨆ J, Submodule.span 𝕜 ↑(Finset.image (fun i => b.repr.symm (lp.single 2 i 1)) J)).topologicalClosure = ⊤
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>h : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure<VAR>i : ι<GOAL>⋯.linearIsometryEquiv.symm (lp.single 2 i 1) = v i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hsp : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure<GOAL>(fun i => (HilbertBasis.mk hv hsp).repr.symm (lp.single 2 i 1)) = v
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥<GOAL>(fun i => (HilbertBasis.mkOfOrthogonalEqBot hv hsp).repr.symm (lp.single 2 i 1)) = v
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<GOAL>(fun i => b.toHilbertBasis.repr.symm (lp.single 2 i 1)) = ⇑b
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>s : Set E<VAR>hs : Orthonormal 𝕜 Subtype.val<GOAL>∃ w b, s ⊆ w ∧ (fun i => b.repr.symm (lp.single 2 i 1)) = Subtype.val
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<GOAL>∃ w b, (fun i => b.repr.symm (lp.single 2 i 1)) = Subtype.val
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>self : BoxIntegral.Prepartition I<GOAL>(↑self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>self : BoxIntegral.Prepartition I<VAR>J : BoxIntegral.Box ι<GOAL>J ∈ self.boxes → J ≤ I
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>J ∈ π.boxes ↔ J ∈ π
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>s : Finset (BoxIntegral.Box ι)<VAR>h₁ : ∀ J ∈ s, J ≤ I<VAR>h₂ : (↑s).Pairwise (Disjoint on BoxIntegral.Box.toSet)<GOAL>J ∈ { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ } ↔ J ∈ s
<VAR>ι : Type u_1<VAR>I J₁ J₂ : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h₁ : J₁ ∈ π<VAR>h₂ : J₂ ∈ π<VAR>h : J₁ ≠ J₂<GOAL>Disjoint ↑J₁ ↑J₂
<VAR>ι : Type u_1<VAR>I J₁ J₂ : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>x : ι → ℝ<VAR>h₁ : J₁ ∈ π<VAR>h₂ : J₂ ∈ π<VAR>hx₁ : x ∈ J₁<VAR>hx₂ : x ∈ J₂<GOAL>J₁ = J₂
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h₁ : J₁ ∈ π<VAR>h₂ : J₂ ∈ π<VAR>hle₁ : J ≤ J₁<VAR>hle₂ : J ≤ J₂<GOAL>J₁ = J₂
<VAR>ι : Type u_1<VAR>I J₁ J₂ : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h₁ : J₁ ∈ π<VAR>h₂ : J₂ ∈ π<VAR>hle : J₁ ≤ J₂<GOAL>J₁ = J₂
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>hJ : J ∈ π<GOAL>J ≤ I
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>hJ : J ∈ π<GOAL>I.lower ≤ J.lower
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>hJ : J ∈ π<GOAL>J.upper ≤ I.upper
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>Function.Injective BoxIntegral.Prepartition.boxes
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : ∀ (J : BoxIntegral.Box ι), J ∈ π₁ ↔ J ∈ π₂<GOAL>π₁ = π₂
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>h : J ≤ I<GOAL>(BoxIntegral.Prepartition.single I J h).boxes = {J}
<VAR>ι : Type u_1<VAR>I J J' : BoxIntegral.Box ι<VAR>h : J ≤ I<GOAL>J' ∈ BoxIntegral.Prepartition.single I J h ↔ J' = J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<GOAL>π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∃ J' ∈ π₂, J ≤ J'
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>J ∈ ⊤ ↔ J = I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>⊤.boxes = {I}
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>J ∉ ⊥
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>⊥.boxes = ∅
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>x : ι → ℝ<GOAL>Set.InjOn (fun J => {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ BoxIntegral.Box.Icc J}
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>Fintype ι<VAR>x : ι → ℝ<GOAL>(Finset.filter (fun J => x ∈ BoxIntegral.Box.Icc J) π.boxes).card ≤ 2 ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>π.iUnion = ⋃ J ∈ π, ↑J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>π.iUnion = ⋃ J ∈ π.boxes, ↑J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>x : ι → ℝ<GOAL>x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>h : J ≤ I<GOAL>(BoxIntegral.Prepartition.single I J h).iUnion = ↑J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>⊤.iUnion = ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ : BoxIntegral.Prepartition I<GOAL>π₁.iUnion = ∅ ↔ π₁ = ⊥
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>⊥.iUnion = ∅
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : J ∈ π<GOAL>↑J ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>π.iUnion ⊆ ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : π₁ ≤ π₂<GOAL>π₁.iUnion ⊆ π₂.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>Disjoint π₁.boxes π₂.boxes
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<GOAL>π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h₁ : π₁.boxes ⊆ π₂.boxes<VAR>h₂ : π₂.iUnion ⊆ π₁.iUnion<GOAL>π₁ = π₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnion πi).boxes = π.boxes.biUnion fun J => (πi J).boxes
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>π.biUnion πi ≤ π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>(π.biUnion fun x => ⊤) = π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>πi₁ πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>h : π₁ = π₂<VAR>hi : ∀ J ∈ π₁, πi₁ J = πi₂ J<GOAL>π₁.biUnion πi₁ = π₂.biUnion πi₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>πi₁ πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>h : π₁ = π₂<VAR>hi : ∀ J ≤ I, πi₁ J = πi₂ J<GOAL>π₁.biUnion πi₁ = π₂.biUnion πi₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>f : BoxIntegral.Box ι → M<GOAL>∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hJ : J ∈ π.biUnion πi<GOAL>π.biUnionIndex πi J ∈ π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>J : BoxIntegral.Box ι<GOAL>π.biUnionIndex πi J ≤ I
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hJ : J ∈ π.biUnion πi<GOAL>J ∈ πi (π.biUnionIndex πi J)
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hJ : J ∈ π.biUnion πi<GOAL>J ≤ π.biUnionIndex πi J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hJ : J ∈ π<VAR>J' : BoxIntegral.Box ι<VAR>hJ' : J' ∈ πi J<GOAL>π.biUnionIndex πi J' = J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>πi' : BoxIntegral.Box ι → (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnion fun J => (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun J => πi' (π.biUnionIndex πi J) J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>boxes : Finset (WithBot (BoxIntegral.Box ι))<VAR>h₁ : ∀ J ∈ boxes, J ≤ ↑I<VAR>h₂ : (↑boxes).Pairwise Disjoint<GOAL>J ∈ BoxIntegral.Prepartition.ofWithBot boxes h₁ h₂ ↔ ↑J ∈ boxes
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>boxes : Finset (WithBot (BoxIntegral.Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<GOAL>(BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>boxes : Finset (WithBot (BoxIntegral.Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'<GOAL>BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>boxes : Finset (WithBot (BoxIntegral.Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'<GOAL>π ≤ BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>boxes₁ : Finset (WithBot (BoxIntegral.Box ι))<VAR>le_of_mem₁ : ∀ J ∈ boxes₁, J ≤ ↑I<VAR>pairwise_disjoint₁ : (↑boxes₁).Pairwise Disjoint<VAR>boxes₂ : Finset (WithBot (BoxIntegral.Box ι))<VAR>le_of_mem₂ : ∀ J ∈ boxes₂, J ≤ ↑I<VAR>pairwise_disjoint₂ : (↑boxes₂).Pairwise Disjoint<VAR>H : ∀ J ∈ boxes₁, J ≠ ⊥ → ∃ J' ∈ boxes₂, J ≤ J'<GOAL>BoxIntegral.Prepartition.ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ ≤ BoxIntegral.Prepartition.ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>boxes : Finset (WithBot (BoxIntegral.Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>f : BoxIntegral.Box ι → M<GOAL>∑ J ∈ (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J = ∑ J ∈ boxes, Option.elim' 0 f J
<VAR>ι : Type u_1<VAR>I J J₁ : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ⊓ ↑J'