SearcharxivSearch

arXiv subjects

Daniel Goldberg

Publications and source records attributed to Daniel Goldberg.

4 recordsLinked to original sources

From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

We formalize the Dirichlet integral and several of its classical applications in the Lean~4 proof assistant. Since the sinc function is not Lebesgue integrable on the positive half-line, the Dirichlet integral must be represented as the limit of integrals over bounded intervals. To avoid the difficulty of removing an exponential factor from a conditionally convergent integral, we instead pass through the absolutely integrable function \(\operatorname{sinc}^2\). We evaluate its integral by differentiation under the integral sign and dominated convergence, and then recover the Dirichlet integral from an identity between truncated integrals. Using these results, we formalize the convergence of the Dirichlet cutoff to the Heaviside function and derive several quadratic and bilinear trigonometric integral identities. Finally, we formalize Lobachevsky's integral formula for continuous periodic functions satisfying a reflection symmetry, using the density of cosine polynomials obtained from Mathlib's Fourier analysis on the additive circle.

cs.LO

A Formalization of the Laplace Transform and Its Inversion in Lean 4

We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem proved through real-variable integration and the Dirichlet integral. As an application, we formalize the Laplace-domain solution of the harmonic oscillator and identify its transform with that of $\sin(\omega t)$. We also discuss the principal analytic and formalization challenges encountered in the development.

cs.LO

Dynamic Breaking of Mirror Symmetry in Spin-Dependent Electron Transport through Chiral Media Causes Enantiomeric Excesses

Two fundamental questions have puzzled scientists for more than 150 years. How did life become homochiral and why was this specific handedness selected. Recently, it has been shown that homochirality could have emerged through the enantioselective interactions of molecules with magnetic substrates due to the asymmetric crystallization of an RNA precursor on a magnetite substrate, abundant on early Earth. This phenomenon is based on the chirality-induced spin selectivity,CISS, effect. Despite its robustness, this model could not provide an answer to the second question: why one specific handedness, D for RNA, was selected. Here we demonstrate that spin-involving processes can have different outcomes in the two enantiomers of chiral molecules. In chiral molecules with unpaired electrons or while electrons are passing through them, the total angular momentum vector, J, is aligned along the easy axis, which is defined by the magnetic anisotropy induced by the spin-orbit coupling and asymmetry of the molecular field. The magnitude J is the same for both enantiomers, but the vectors may be aligned differently relative to the molecular frame in the two enantiomers. This difference can be quantified by, for example, by the angle between J and electric dipole moment of the molecule. We show by direct measurements, theory, and ab initio calculations that dynamic spin processes in chiral molecules could result in different efficiencies of spin-related phenomena, including the interaction of chiral molecules with magnetic surfaces. The findings may provide an explanation for the specific homochirality in nature.

physics.chem-ph

TopoBERT: Plug and Play Toponym Recognition Module Harnessing Fine-tuned BERT

Extracting precise geographical information from textual contents is crucial in a plethora of applications. For example, during hazardous events, a robust and unbiased toponym extraction framework can provide an avenue to tie the location concerned to the topic discussed by news media posts and pinpoint humanitarian help requests or damage reports from social media. Early studies have leveraged rule-based, gazetteer-based, deep learning, and hybrid approaches to address this problem. However, the performance of existing tools is deficient in supporting operations like emergency rescue, which relies on fine-grained, accurate geographic information. The emerging pretrained language models can better capture the underlying characteristics of text information, including place names, offering a promising pathway to optimize toponym recognition to underpin practical applications. In this paper, TopoBERT, a toponym recognition module based on a one dimensional Convolutional Neural Network (CNN1D) and Bidirectional Encoder Representation from Transformers (BERT), is proposed and fine-tuned. Three datasets (CoNLL2003-Train, Wikipedia3000, WNUT2017) are leveraged to tune the hyperparameters, discover the best training strategy, and train the model. Another two datasets (CoNLL2003-Test and Harvey2017) are used to evaluate the performance. Three distinguished classifiers, linear, multi-layer perceptron, and CNN1D, are benchmarked to determine the optimal model architecture. TopoBERT achieves state-of-the-art performance (f1-score=0.865) compared to the other five baseline models and can be applied to diverse toponym recognition tasks without additional training.

cs.CL