Knihovna obsahuje počítačem-verifikovaný kód v Leanu 4 pro pokročilou práci s Němyckého operátory v prostorech integrovatelných funkcí. Jako ukázkové příklady použití hlavních matematických vět byly zvoleny nelineární integrální funkcionály. Kromě toho jsou tam, kde jsou obecné matematické věty těžko srozumitelné, explicitně doplněny o významné speciální případy (typicky pro eukleidovské prostory). Hlavním přínosem knihovny je zpřístupnění matematických tvrzení, která jsou formálně zverifikována až na úroveň základních axiomů.

Accurate prediction of corona discharge ignition voltages Ui is essential for the design and reliability assessment of high-voltage (HV) systems. This article presents a combined experimental and numerical study focused on the evaluation of Ui for various electrode geometries, gap distances, and pressures in ambient or synthetic air. Based on a new analysis of experimental data, two numerical optimization models were developed and implemented in COMSOL Multiphysics to determine ignition voltages with minimal computational cost. Both models are founded on two physically motivated assumptions: a constant critical electron avalanche intensity at corona onset and symmetry of the ignition electric field profile under low field homogeneity conditions with respect to varying gap distances. The first method is based on integration of the effective ionization coefficient along the discharge path, while the second relies on the local electric field at the electrode tip. In both cases, the Nelder–Mead optimization algorithm is employed to identify the critical voltage corresponding to corona inception. The proposed methods were validated against experimental data over a wide range of pressures, electrode configurations, and field homogeneity conditions. The predicted ignition voltages show good agreement with measurements, with a typical deviation of approximately 5% and a maximum error below 10% in a limited number of cases. While the integration-based optimization provides higher robustness and reduced dependence on empirical input, the field-based optimization offers simplicity and rapid implementation. The presented approaches enable efficient parametric studies and provide practical tools for HV insulation analysis, the design of corona-resistant components, and the definition of boundary conditions (BCs) in more advanced discharge simulations.

This dataset contains raw AE signals from drilling titanium alloy Ti-6Al-4V (18 experiments, 180 holes, drill D = 2.5 mm), FFT-filtered data (band 90–400 kHz), and features extracted using the TSfresh library for machine learning. The dataset supports research on tool wear prediction and process condition classification.