32 research outputs found
Formalized Haar Measure
No full textWe describe the formalization of the existence and uniqueness of the Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean’s mathematical library mathlib, and discuss the construction of product measures and the proof of Fubini’s theorem for the Bochner integral
Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality
No full textWe introduce an abstraction which allows arguments involving iterated integrals to be formalized conveniently in type-theory-based proof assistants. We call this abstraction the marginal construction, since it is connected to the marginal distribution in probability theory. The marginal construction gracefully handles permutations to the order of integration (Tonelli’s theorem in several variables), as well as arguments involving an induction over dimension.
We implement the marginal construction and several applications in the language Lean. The most difficult of these applications, the Gagliardo-Nirenberg-Sobolev inequality, is a foundational result in the theory of elliptic partial differential equations and has not previously been formalized
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
No full textWe describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model
The Effect of Moisture on the Granular Characteristics of Polymetallic Nodules in the Context of Bulk Handling
No full textIn recent decades, a significant amount of the research into deep sea polymetallic nodule mining has been conducted on the collecting vehicle and the riser system accommodating transport from the seabed to the mining support vessel. The topside operation, however, is less commonly described in the literature. This part of the operation deserves attention because it significantly impacts project risk and cost.After initial investigation the main research question was formed: What is the effect of moisture on the granular characteristics of polymetallic nodules in the context of bulk handling?Royal IHC provided a container with around 50 kg of polymetallic nodules from the Clarion Clipperton Zone. These nodules have been used in earlier research, focused on the degradation of nodules in transport from the seabed to the sea surface. Resulting in broken and damaged nodules. Therefore these are a good representation of nodules coming from the vertical transport system.The degraded nodules provide an unique opportunity to gain an understanding of the bulk behaviour of the nodules once they have arrived on the ship. Four experimental setups were used to understand the granular characteristics of degraded polymetallic nodules in a non-destructive manner. In the first setup, particle properties such as density, porosity, and water content have been measured. The second setup identifies the shape of degraded nodules. The third setup measures the angle of repose for different nodule sizes and water content. The last setup measures the friction factor for different nodule sizes and water content, while changing the sliding surface between steel or rubber. Lastly, clay has been added to the sliding surface experiment. Considering the angle of repose tests and the sliding and rolling friction angle, it is evident that the difference between dry and fully saturated nodules is minimal. For the friction angle: The maximum deviation between dry, saturated and CCZ clay is 8 % on steel and 9 % on rubber, corresponding to 2 degrees. For the angle of repose, the difference between dry and saturated is negligible. It is concluded that the moisture content only contributes minimal level to bulk behaviour of nodules.Offshore and Dredging Engineerin
Going beyond transactions: Theoretical perspectives and empirical studies on customer engagement behavior effectiveness
No full textRecent societal developments have altered customer-firm interactions. Social media (e.g., Twitter, Facebook, and Youtube) substantially increased the connectivity among customers and between customers and firms. Nowadays the relationship between customers and firms is no longer restricted to the moment of purchase. Customers communicate with other customers and/or companies outside the moment of purchase and do so more widespread, faster, and interactive than ever before. For instance, customers tweet about the latest movie they saw, customers like or comment on a company’s Facebook page, and/or customers post videos of themselves driving an expensive car. In light of these developments and their potential impact, customer engagement behaviors (i.e., non-transactional customer behaviors, such as customer word-of-mouth, customer co-creation in new product development, and customer feedback) have become a very important topic for companies. Despite the theoretical and managerial relevance of customer engagement behaviors, thorough empirical research on the effectiveness of customer engagement behaviors is largely lacking. This dissertation addresses this gap. In three interrelated research projects this dissertation identifies suited theoretical perspectives on outcomes of customer engagement behavior, empirically studies the impact of customer engagement behaviors on an individual customer performance metric (i.e., customer satisfaction) and an aggregated firm performance metric (i.e., market valuation), and identifies contingencies that drive these outcomes
Maintaining a library of formal mathematics
No full textThe Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.</p
Supplementary material for the CPP 2023 paper Formalising the h-Principle and Sphere Eversion
No full textThe supplementary material for the CPP 2023 paper Formalising the h-Principle and Sphere Eversion contains the formalisation of the result. It is a frozen version of the repository
https://github.com/leanprover-community/sphere-eversion
at commit
9cd599b74a419209e4204829efcd50008fdd1c2b
Only cpp2023.zip is required to compile the project, by extracting the files and following the instructions in the README.
These instructions will download mathlib (https://github.com/leanprover-community/mathlib) at commit cf9386b56953fb40904843af98b7a80757bbe7f9. For convenience, this version of mathlib has been provided as a separate compressed file mathlib.zip. Instead of following the step `leanproject get-mathlib-cache` in the README, one can extract that in the same folder
