Please use the following text to cite this item or export to a predefined format:
Girg, Petr; Nečesal, Petr; Dvořák, Martin and Psutka, Jakub, 2026, Nemytskii operators in Lebesgue spaces, DSpace at University of West Bohemia, http://hdl.handle.net/20.500.14592/110
| dc.contributor.author | Girg, Petr |
| dc.contributor.author | Nečesal, Petr |
| dc.contributor.author | Dvořák, Martin |
| dc.contributor.author | Psutka, Jakub |
| dc.date.accessioned | 2026-07-29T08:37:52Z |
| dc.date.available | 2026-07-29T08:37:52Z |
| dc.date.issued | 2026 |
| dc.description | 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ů. |
| dc.description.abstract | The library contains computer-verified Lean 4 code for advanced work with Nemytskii operators in Lebesgue spaces. As illustrative applications of the main theorems, nonlinear integral functionals have been chosen. Moreover, wherever general theorems are difficult to understand, they are explicitly supplemented with important special cases (typically for Euclidean spaces). The principal contribution of the library is to make available mathematical results that have been formally verified down to the level of the underlying axioms. |
| dc.description.sponsorship | ZČU |
| dc.identifier.uri | http://hdl.handle.net/20.500.14592/110 |
| dc.language.iso | en |
| dc.publisher | Západočeská univerzita v Plzni |
| dc.rights | Apache License 2.0 |
| dc.rights.label | PUB |
| dc.rights.uri | http://opensource.org/licenses/Apache-2.0 |
| dc.subject | Carathéodoryho funkce |
| dc.subject | Němyckého operátory |
| dc.subject | silná spojitost |
| dc.subject | Lipschitzovská spojitost |
| dc.subject | Fréchetova diferencovatelnost |
| dc.subject | integrální funkcionál |
| dc.subject | reprezentace znalostí v matematice |
| dc.subject | formální verifikace |
| dc.title | Nemytskii operators in Lebesgue spaces |
| dc.type | software |
| local.files.count | 1 |
| local.files.size | 66000 |
| local.has.files | yes |
| local.subject.translated | Carathéodory functions |
| local.subject.translated | superposition operators |
| local.subject.translated | strong continuity |
| local.subject.translated | Lipschitz continuity |
| local.subject.translated | Fréchet differentiability |
| local.subject.translated | integral functional |
| local.subject.translated | mathematical knowledge representation |
| local.subject.translated | formal verification |
