检索结果-内蒙古大学图书馆

14th Conference on Certified Programs and Proofs

作者： Baanen, Anne Villarello, Alain Chavarri Dahmen, Sander R. Vrije Univ Amsterdam Amsterdam Netherlands Lean FRO Redmond WA 98052 USA

ISBN: (纸本)9798400713477

number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the number fields section of the L-functions and modular forms database (LMFDB). These concern, for several number fields, the explicitly given integral basis of the ring of integers and the discriminant. To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.

关键词： formalized mathematics algebraic number theory tactics Lean Mathlib

来源：评论

学校读者我要写书评

暂无评论

An alternative GPU acceleration for a pseudopotential plane-waves density functional theory code with applications to metallic systems

引用

computer PHYSICS COMMUNICATIONS 2025年 308卷

作者： Gong, Xuejun Dal Corso, Andrea Int Sch Adv Studies SISSA Via Bonomea 265 I-34136 Trieste Italy CNR IOM Via Bonomea 265 I-34136 Trieste Italy

We present an alternative GPU acceleration for plane waves pseudopotentials electronic structure codes designed for systems that have small unit cells but require a large number of k points to sample the Brillouin zone as happens, for instance, in metals. We discuss the diagonalization of the Kohn and Sham equations and the solution of the linear system derived in density functional perturbation theory. Both problems take advantage from a rewriting of the routine that applies the Hamiltonian to the Bloch wave-functions to work simultaneously (in parallel on the GPU threads) on the wave-functions with different wave-vectors k, as many as allowed by the GPU memory. Our implementation is written in CUDA Fortran and makes extensive use of kernel routines that run on the GPU (GLOBAL routines) or can be called from inside the GPU kernel (DEVICE routines). We compare our method with the CPUs only calculation and with the approach currently implemented in Quantum ESPRESSO that uses GPU accelerated libraries for the FFT and for the linear algebra tasks such as the matrix-matrix multiplications as well as OpenACC directives for loop parallelization. We show in a realistic example that our method can give a significant improvement in the cases for which it has been designed.

关键词： Electronic structure Lattice dynamics Metals GPU Density functional perturbation theory

来源：评论

学校读者我要写书评

暂无评论

Some new techniques and progress towards the resolution of the conjecture of exceptional APN functions and absolutely irreducibility of a class of polynomials

引用

DESIGNS CODES AND CRYPTOGRAPHY 2023年第7期91卷 2481-2495页

作者： Delgado, Moises Janwa, Heeralal Agrinsoni, Carlos Univ Puerto Rico Dept Math 205 Calle Antonio R Barcelo Cayey PR 00736 USA Univ Puerto Rico Dept Math 17 Univ Ave Ste 1701 San Juan PR 00925 USA

Almost Perfect Nonlinear (APN) functions are very useful in cryptography, when they are used as S-Boxes due to their good resistance to differential cryptanalysis. Also, some of the curves and surfaces defined by the corresponding nonlinear functions have many rational points and have applications to algebraic-Geometric (AG) codes (Janwa and Wilson in Applied algebra, algebraic algorithms and error-correcting codes (San Juan, PR, 1993), vol 673, pp 180-194, Springer, Berlin, 1993, in IEEE Trans Inform theory, accepted). An APN function f : F-2(n) -> F-2(n) is called an exceptional APN if it is APN on infinitely many extensions of F2n. Aubry et al. (Contemp Math 518:23-31, 2010) conjectured that the only exceptional APN functions are the Gold and the Kasami-Welch monomial functions. They established that a polynomial function of odd degree is not an exceptional APN provided the degree is not a Gold number (2(k) + 1) or a Kasami-Welch number (2(2k) - 2(k) + 1). When the degree of the polynomial function is a Gold number, several partial results are known. Here, we prove the relative primeness conjecture of the Gold degree polynomials. This result helps us substantially to make advances toward the resolution of the exceptional APN conjecture in the Gold degree case. We prove that Gold degree polynomials of the form x(2k+1) + h(x), where deg(h) is an odd integer, cannot be exceptional APN (with a few natural exceptions). We also prove that the absolutely irreducible components of the KasamiWelch degree curves intersect transversally at a particular point. Consequently, we prove that Kasami-Welch degree functions of type x(22k-)2(k)+1 + h(x) produce absolutely irreducible surfaces in the case deg(h) = 3 (mod 4);and also deg(h) = 2(m-1) + 1 (mod 2(m)) under certain conditions. As a result, we show that the exceptional APN conjecture is true for these classes as well.

关键词： APN functions Exceptional APN functions Janwa-McGuire-Wilson conjecture Absolutely irreducible polynomials S-boxes Differential cryptanalysis

来源：评论

学校读者我要写书评

暂无评论

Pourchet's theorem in action: decomposing univariate nonnegative polynomials as sums of five squares 23

Pourchet's theorem in action: decomposing univariate nonnega...

引用

48th International Symposium on Symbolic and algebraic Computation (ISSAC)

作者： Magron, Victor Koprowski, Przemyslaw Vaccon, Tristan CNRS LAAS Toulouse France Inst Mathemat Toulouse Toulouse France Univ Silesia Katowice Inst Math Katowice Poland Univ Limoges CNRS XLIM UMR 7252 Limoges France

ISBN: (纸本)9798400700392

Pourchet proved in 1971 that every nonnegative univariate polynomial with rational coefficients is a sum of five or fewer squares. Nonetheless, there are no known algorithms for constructing such a decomposition. The sole purpose of the present paper is to present a set of algorithms that decompose a given nonnegative polynomial into a sum of six (five under some unproven conjecture or when allowing weights) squares of polynomials. Moreover, we prove that the binary complexity can be expressed polynomially in terms of classical operations of computer algebra and algorithmic number theory.

关键词： nonnegative univariate rational polynomial rational polynomial sums of squares decomposition real algebraic geometry norm equation

来源：评论

学校读者我要写书评

暂无评论

Estimation under group actions: Recovering orbits from invariants

引用

APPLIED AND COMPUTATIONAL HARMONIC ANALYSIS 2023年第1期66卷 236-319页

作者： Bandeira, Afonso S. Blum-Smith, Ben Kileel, Joe Niles-Weed, Jonathan Perry, Amelia Wein, Alexander S. Swiss Fed Inst Technol Dept Math Zurich Switzerland Johns Hopkins Univ Dept Appl Math & Stat Baltimore MD 21218 USA Univ Texas Austin Dept Math Austin TX USA Univ Texas Austin Oden Inst Austin TX USA NYU Courant Inst Math Sci New York NY USA NYU Ctr Data Sci New York NY USA MIT Dept Math Cambridge MA USA Univ Calif Davis Dept Math Davis CA USA

We study a class of orbit recovery problems in which we observe independent copies of an unknown element of Rp, each linearly acted upon by a random element of some group (such as Z/p or SO(3)) and then corrupted by additive Gaussian noise. We prove matching upper and lower bounds on the number of samples required to approximately recover the group orbit of this unknown element with high probability. These bounds, based on quantitative techniques in invariant theory, give a precise correspondence between the statistical difficulty of the estimation problem and algebraic properties of the group. Furthermore, we give computerassisted procedures to certify these properties that are computationally efficient in many cases of interest. The model is motivated by geometric problems in signal processing, computer vision, and structural biology, and applies to the reconstruction problem in cryo-electron microscopy (cryo-EM), a problem of significant practical interest. Our results allow us to verify (for a given problem size) that if cryo-EM images are corrupted by noise with variance & sigma;2, the number of images required to recover the molecule structure scales as & sigma;6. We match this bound with a novel (albeit computationally expensive) algorithm for ab initio reconstruction in cryo-EM, based on invariant features of degree at most 3. We further discuss how to recover multiple molecular structures from mixed (or heterogeneous) cryo-EM samples. & COPY;2023 Elsevier Inc. All rights reserved.

关键词： Signal processing Biomedical imaging Statistical aspects of information theory applications of lie groups applications of invariant theory applications theory applications of commutative algebra

来源：评论

学校读者我要写书评

暂无评论

Non-symmetric number Triangles Arising from Hypercomplex Function theory in Rⁿ⁺¹ 22nd

Non-symmetric Number Triangles Arising from Hypercomplex Fun...

引用

22nd International Conference on Computational Science and its applications (ICCSA)

作者： Cacao, Isabel Falcao, M. Irene Malonek, Helmuth R. Tomaz, Graca Univ Aveiro CIDMA Aveiro Portugal Univ Minho CMAT Braga Portugal Inst Politecn Guarda Guarda Portugal

The paper is focused on intrinsic properties of a one-parameter family of non-symmetric number triangles T (n), n >= 2, which arises in the construction of hyperholomorphic Appell polynomials.

ISBN: (纸本)9783031105364;9783031105357

The paper is focused on intrinsic properties of a one-parameter family of non-symmetric number triangles T (n), n >= 2, which arises in the construction of hyperholomorphic Appell polynomials.

关键词： Non-symmetric Pascal triangle Clifford algebra Recurrence relation

来源：评论

学校读者我要写书评

暂无评论

Parikh's Theorem Made Symbolic

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2024年第POPL期8卷 1945-1977页

作者： Hague, Matthew Jez, Artur Lin, Anthony W. Royal Holloway Univ London Dept Comp Sci Egham Hill Egham TW20 0EX Surrey England Univ Wroclaw Inst Comp Sci Joliot Curie 15 PL-50383 Wroclaw Poland Univ Kaiserslautern Landau Kaiserslautern Germany MPI SWS Paul Ehrlich StrBldg G 26 DE-67663 Kaiserslautern Germany

Parikh's Theorem is a fundamental result in automata theory with numerous applications in computer science. These include software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases), among others. Parikh's Theorem states that the letter-counting abstraction of a language recognized by finite automata or context-free grammars is definable in Linear Integer Arithmetic (a.k.a. Presburger Arithmetic). In fact, there is a linear-time algorithm computing existential Presburger formulas capturing such abstractions, which enables an efficient analysis via SMT-solvers. Unfortunately, real-world applications typically require large alphabets (e.g. Unicode, containing a million of characters) - which are well-known to be not amenable to explicit treatment of the alphabets - or even worse infinite alphabets. Symbolic automata have proven in the last decade to be an effective algorithmic framework for handling large finite or even infinite alphabets. A symbolic automaton employs an effective boolean algebra, which offers a symbolic representation of character sets (i.e. in terms of predicates) and often lends itself to an exponentially more succinct representation of a language. Instead of letter-counting, Parikh's Theorem for symbolic automata amounts to counting the number of times different predicates are satisfied by an input sequence. Unfortunately, naively applying Parikh's Theorem from classical automata theory to symbolic automata yields existential Presburger formulas of exponential size. In this paper, we provide a new construction for Parikh's Theorem for symbolic automata and grammars, which avoids this exponential blowup: our algorithm computes an existential formula in polynomial-time over (quantifier-free) Presburger and the base theory. In fact, our algorithm ex

关键词： Symbolic Automata Infinite Alphabets Decision Procedures Sequence theory String Constraints Abstraction Satisfiability Modulo Theories

来源：评论

学校读者我要写书评

暂无评论

Fully computer-Assisted Proofs in Extremal Combinatorics 37

Fully Computer-Assisted Proofs in Extremal Combinatorics

引用

37th AAAI Conference on Artificial Intelligence (AAAI) / 35th Conference on Innovative applications of Artificial Intelligence / 13th Symposium on Educational Advances in Artificial Intelligence

作者： Parczyk, Olaf Pokutta, Sebastian Spiegel, Christoph Szabo, Tibor Free Univ Berlin Inst Math Berlin Germany Tech Univ Berlin Inst Math Berlin Germany Zuse Inst Berlin Dept AI Soc Sci & Technol Berlin Germany

ISBN: (纸本)9781577358800

We present a fully computer-assisted proof system for solving a particular family of problems in Extremal Combinatorics. Existing techniques using Flag algebras have proven powerful in the past, but have so far lacked a computational counterpart to derive matching constructive bounds. We demonstrate that common search heuristics are capable of finding constructions far beyond the reach of human intuition. Additionally, the most obvious downside of such heuristics, namely a missing guarantee of global optimality, can often be fully eliminated in this case through lower bounds and stability results coming from the Flag algebra approach. To illustrate the potential of this approach, we study two related and well-known problems in Extremal Graph theory that go back to questions of Erdos from the 60s. Most notably, we present the first major improvement in the upper bound of the Ramsey multiplicity of K-4 in 25 years, precisely determine the first off-diagonal Ramsey multiplicity number, and settle the minimum number of independent sets of size four in graphs with clique number strictly less than five.

关键词： algebra

来源：评论

学校读者我要写书评

暂无评论

Whitney numbers of Combinatorial Geometries and Higher-Weight Dowling Lattices

引用

SIAM JOURNAL ON APPLIED algebra AND GEOMETRY 2022年第2期6卷 156-189页

作者： Ravagnani, Alberto Eindhoven Univ Technol Dept Math & Comp Sci NL-5612 AZ Eindhoven Netherlands

We study the Whitney numbers of the first kind of combinatorial geometries, in connection with the theory of error-correcting codes. The first part of the paper is devoted to general results relating the Mo "\bius functions of nested atomistic lattices, extending some classical theorems in combinatorics. We then specialize our results to restriction geometries, i.e., to sublattices \scrA of the lattice of subspaces of an \BbbFq-linear space, say, X, generated by a set of projective points A \subseteq X. In this context, we introduce the notion of subspace distribution and show that partial knowledge of the latter is equivalent to partial knowledge of the Whitney numbers of \scrA. This refines a classical result by Dowling. The most interesting applications of our results are to be seen in the theory of higher -weight Dowling lattices (HWDLs), to which we devote the second and most substantive part of the paper. These combinatorial geometries were introduced by Dowling in 1971 in connection with fundamental problems in coding theory, most notably the famous MDS conjecture. They were further studied by, among others, Zaslavsky, Bonin, Kung, Brini, and Games. To date, still very little is known about these lattices and the techniques to compute their Whitney numbers have not been discovered yet. In this paper, we bring forward the theory of HWDLs, computing their Whitney numbers for new infinite families of parameters. We also show that the second Whitney numbers of HWDLs are polynomials in the underlying field size q, whose coefficients are curious expressions involving the Bernoulli numbers. In passing, we obtain new results intersecting coding theory and enumerative combinatorics.

关键词： Whitney number combinatorial geometry coding theory higher-weight Dowling lattice

来源：评论

学校读者我要写书评

暂无评论

Some Generalized Clifford-Jacobi polynomials and Associated Spheroidal Wavelets

引用

Analysis in theory and applications 2022年第4期38卷 394-416页

作者： Sabrine Arfaoui Anouar Ben Mabrouk Algebra Number Theory and Nonlinear Analysis Laboratory LR18ES15Department of MathematicsFaculty of SciencesMonastir 5000Tunisia Department of Mathematics Higher Institute of Applied Mathematics and Computer ScienceStreet of Assad Ibn AlfouratKairouan University3100 Kairouan Tunisia Department of Mathematics Faculty of SciencesUniversity of TabukSaudi Arabia

In the present paper,by extending some fractional calculus to the framework of Clifford analysis,new classes of wavelet functions are ***,some classes of monogenic polynomials are provided based on 2-parameters weight functions which extend the classical Jacobi ones in the context of Clifford *** discovered polynomial sets are next applied to introduce new wavelet *** formula as well as Fourier-Plancherel rules have been *** main tool reposes on the extension of fractional derivatives,fractional integrals and fractional Fourier transforms to Clifford analysis.

关键词： Continuous wavelet transform Clifford analysis Clifford Fourier transform Fourier-plancherel fractional Fourier transform fractional derivatives fractional integrals fractional Clifford Fourier transform Monogenic functions.

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：