Bourgin-Yang version of the Borsuk-Ulam theorem for Z(pk)-equivariant maps

Let G = Z(pk) be a cyclic group of prime power order and let V and W be orthogonal representations of G with V-G = W-G = W-G = {0}. Let S(V) be the sphere of V and suppose f: S(V) -> W is a G-equivariant mapping. We give an estimate for the dimension of the set f(-1){0} in terms of V and W. This extends the Bourgin-Yang version of the Borsuk-Ulam theorem to this class of groups. Using this estimate, we also estimate the size of the G-coincidences set of a continuous map from S(V) into a real vector space W'.

Lymphatic fluctuation in the parenchymal remodeling stage of acute interstitial pneumonia, organizing pneumonia, nonspecific interstitial pneumonia and idiopathic pulmonary fibrosis

Because the superficial lymphatics in the lungs are distributed in the subpleural, interlobular and peribroncovascular interstitium, lymphatic impairment may occur in the lungs of patients with idiopathic interstitial pneumonias (IIPs) and increase their severity. We investigated the distribution of lymphatics in different remodeling stages of IIPs by immunohistochemistry using the D2-40 antibody. Pulmonary tissue was obtained from 69 patients with acute interstitial pneumonia/diffuse alveolar damage (AIP/DAD, N = 24), cryptogenic organizing pneumonia/organizing pneumonia (COP/OP, N = 6), nonspecific interstitial pneumonia (NSIP/NSIP, N = 20), and idiopathic pulmonary fibrosis/usual interstitial pneumonia (IPF/UIP, N = 19). D2-40+ lymphatic in the lesions was quantitatively determined and associated with remodeling stage score. We observed an increase in the D2-40+ percent from DAD (6.66 +/- 1.11) to UIP (23.45 +/- 5.24, P = 0.008) with the advanced process of remodeling stage of the lesions. Kaplan-Meier survival curves showed a better survival for patients with higher lymphatic D2-40+ expression than 9.3%. Lymphatic impairment occurs in the lungs of IIPs and its severity increases according to remodeling stage. The results suggest that disruption of the superficial lymphatics may impair alveolar clearance, delay organ repair and cause severe disease progress mainly in patients with AIP/DAD. Therefore, lymphatic distribution may serve as a surrogate marker for the identification of patients at greatest risk for death due to IIPs.

Analysis of confinement potential fluctuation and band-gap renormalization effects on excitonic transition in GaAs/AlGaAs multiquantum wells grown on (100) and (311)A GaAs surfaces

The competition between confinement potential fluctuations and band-gap renormalization (BGR) in GaAs/AlxGa1-xAs quantum wells grown on [1 0 0] and [3 1 1]A GaAs substrates is evaluated. The results clearly demonstrate the coexistence of the band-tail states filling related to potential fluctuations and the band-gap renormalization caused by an increase in the density of photogenerated carriers during the photoluminescence (PL) experiments. Both phenomena have strong influence on temperature dependence of the PL-peak energy (E-PL(T)). As the photon density increases, the E-PL can shift to either higher or lower energies, depending on the sample temperature. The temperature at which the displacement changes from a blueshift to a redshift is governed by the magnitude of the potential fluctuations and by the variation of BGR with excitation density. A simple band-tail model with a Gaussian-like distribution of the density of state was used to describe the competition between the band-tail filling and the BGR effects on E-PL(T). (C) 2012 Elsevier B.V. All rights reserved.

On the zeros of polynomials: an extension of the Enestrom-Kakeya theorem

This paper presents an extension of the Enestrom-Kakeya theorem concerning the roots of a polynomial that arises from the analysis of the stability of Brown (K, L) methods. The generalization relates to relaxing one of the inequalities on the coefficients of the polynomial. Two results concerning the zeros of polynomials will be proved, one of them providing a partial answer to a conjecture by Meneguette (1994)[6]. (C) 2011 Elsevier Inc. All rights reserved.

Kleiner's theorem for unitary representations of posets

A subspace representation of a poset S = {s(1), ..., S-t} is given by a system (V; V-1, ..., V-t) consisting of a vector space V and its sub-spaces V-i such that V-i subset of V-j if s(i) (sic) S-j. For each real-valued vector chi = (chi(1), ..., chi(t)) with positive components, we define a unitary chi-representation of S as a system (U: U-1, ..., U-t) that consists of a unitary space U and its subspaces U-i such that U-i subset of U-j if S-i (sic) S-j and satisfies chi 1 P-1 + ... + chi P-t(t) = 1, in which P-i is the orthogonal projection onto U-i. We prove that S has a finite number of unitarily nonequivalent indecomposable chi-representations for each weight chi if and only if S has a finite number of nonequivalent indecomposable subspace representations; that is, if and only if S contains any of Kleiner's critical posets. (c) 2012 Elsevier Inc. All rights reserved.

Spectral fluctuation and 1/f(alpha) noise in the energy level statistics of interacting trapped bosons

It has been recently shown numerically that the transition from integrability to chaos in quantum systems and the corresponding spectral fluctuations are characterized by 1/f(alpha) noise with 1 <= alpha <= 2. The system of interacting trapped bosons is inhomogeneous and complex. The presence of an external harmonic trap makes it more interesting as, in the atomic trap, the bosons occupy partly degenerate single-particle states. Earlier theoretical and experimental results show that at zero temperature the low-lying levels are of a collective nature and high-lying excitations are of a single-particle nature. We observe that for few bosons, the P(s) distribution shows the Shnirelman peak, which exhibits a large number of quasidegenerate states. For a large number of bosons the low-lying levels are strongly affected by the interatomic interaction, and the corresponding level fluctuation shows a transition to a Wigner distribution with an increase in particle number. It does not follow Gaussian orthogonal ensemble random matrix predictions. For high-lying levels we observe the uncorrelated Poisson distribution. Thus it may be a very realistic system to prove that 1/f(alpha) noise is ubiquitous in nature.

Regularity at infinity of real mappings and a Morse-Sard theorem

We prove a new Morse-Sard-type theorem for the asymptotic critical values of semi-algebraic mappings and a new fibration theorem at infinity for C-2 mappings. We show the equivalence of three different types of regularity conditions which have been used in the literature in order to control the asymptotic behaviour of mappings. The central role of our picture is played by the p-regularity and its bridge toward the rho-regularity which implies topological triviality at infinity.

Kurzweil integral for Riesz space-valued functions: Uniform convergence theorem

Our objective here is to prove that the uniform convergence of a sequence of Kurzweil integrable functions implies the convergence of the sequence formed by its corresponding integrals.

A uniqueness theorem for the determination of sources in the Germain–Lagrange plate equation

We prove a uniqueness result related to the Germain–Lagrange dynamic plate differential equation. We consider the equation {∂2u∂t2+△2u=g⊗f,in ]0,+∞)×R2,u(0)=0,∂u∂t(0)=0, where uu stands for the transverse displacement, ff is a distribution compactly supported in space, and g∈Lloc1([0,+∞)) is a function of time such that g(0)≠0g(0)≠0 and there is a T0>0T0>0 such that g∈C1[0,T0[g∈C1[0,T0[. We prove that the knowledge of uu over an arbitrary open set of the plate for any interval of time ]0,T[]0,T[, 0

A fixed point theorem for Meir-Keeler contractions in ordered metric spaces

[EN] The purpose of this paper is to present some fixed point theorems for Meir-Keeler contractions in a complete metric space endowed with a partial order. MSC: 47H10.

A best proximity point theorem for Geraghty-contractions

[EN] The purpose of this paper is to provide sufficient conditions for the existence of a unique best proximity point for Geraghty-contractions.Our paper provides an extension of a result due to Geraghty (Proc. Am. Math. Soc. 40:604-608, 1973).

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Novel simulation methods for Coulomb and hydrodynamic interactions

This thesis presents new methods to simulate systems with hydrodynamic and electrostatic interactions. Part 1 is devoted to computer simulations of Brownian particles with hydrodynamic interactions. The main influence of the solvent on the dynamics of Brownian particles is that it mediates hydrodynamic interactions. In the method, this is simulated by numerical solution of the Navier--Stokes equation on a lattice. To this end, the Lattice--Boltzmann method is used, namely its D3Q19 version. This model is capable to simulate compressible flow. It gives us the advantage to treat dense systems, in particular away from thermal equilibrium. The Lattice--Boltzmann equation is coupled to the particles via a friction force. In addition to this force, acting on {it point} particles, we construct another coupling force, which comes from the pressure tensor. The coupling is purely local, i.~e. the algorithm scales linearly with the total number of particles. In order to be able to map the physical properties of the Lattice--Boltzmann fluid onto a Molecular Dynamics (MD) fluid, the case of an almost incompressible flow is considered. The Fluctuation--Dissipation theorem for the hybrid coupling is analyzed, and a geometric interpretation of the friction coefficient in terms of a Stokes radius is given. Part 2 is devoted to the simulation of charged particles. We present a novel method for obtaining Coulomb interactions as the potential of mean force between charges which are dynamically coupled to a local electromagnetic field. This algorithm scales linearly, too. We focus on the Molecular Dynamics version of the method and show that it is intimately related to the Car--Parrinello approach, while being equivalent to solving Maxwell's equations with freely adjustable speed of light. The Lagrangian formulation of the coupled particles--fields system is derived. The quasi--Hamiltonian dynamics of the system is studied in great detail. For implementation on the computer, the equations of motion are discretized with respect to both space and time. The discretization of the electromagnetic fields on a lattice, as well as the interpolation of the particle charges on the lattice is given. The algorithm is as local as possible: Only nearest neighbors sites of the lattice are interacting with a charged particle. Unphysical self--energies arise as a result of the lattice interpolation of charges, and are corrected by a subtraction scheme based on the exact lattice Green's function. The method allows easy parallelization using standard domain decomposition. Some benchmarking results of the algorithm are presented and discussed.

Fluctuation spectroscopy of single plasmonic nanostructures

Plasmonic nanoparticles are great candidates for sensing applications with optical read-out. Plasmon sensing is based on the interaction of the nanoparticle with electromagnetic waves where the particle scatters light at its resonance wavelength. This wavelength depends on several intrinsic factors like material, shape and size of the nanoparticle as well as extrinsic factors like the refractive index of the surrounding medium. The latter allows the nanoparticle to be used as a sensor; changes in the proximate environment can be directly monitored by the wavelength of the emitted light. Due to their minuscule size and high sensitivity this allows individual nanoparticles to report on changes in particle coverage.rnrnTo use this single particle plasmon sensor for future sensing applications it has to meet the demand for detection of incidents on the single molecule level, such as single molecule sensing or even the detection of conformational changes of a single molecule. Therefore, time resolution and sensitivity have to be enhanced as today’s measurement methods for signal read-out are too slow and not sensitive enough to resolve these processes. This thesis presents a new experimental setup, the 'Plasmon Fluctuation Setup', that leads to tremendous improvements in time resolution and sensitivity. This is achieved by implementation of a stronger light source and a more sensitive detector. The new setup has a time resolution in the microsecond regime, an advancement of 4-6 orders of magnitude to previous setups. Its resonance wavelength stability of 0.03 nm, measured with an exposure time of 10 ms, is an improvement of a factor of 20 even though the exposure time is 3000 times shorter than in previous reports. Thus, previously unresolvable wavelength changes of the plasmon sensor induced by minor local environmental alteration can be monitored with extremely high temporal resolution.rnrnUsing the 'Plasmon Fluctuation Setup', I can resolve adsorption events of single unlabeled proteins on an individual nanorod. Additionally, I monitored the dynamic evolution of a single protein binding event on a millisecond time scale. This feasibility is of high interest as the role of certain domains in the protein can be probed by a study of modified analytes without the need for labels possibly introducing conformational or characteristic changes to the target. The technique also resolves equilibrium fluctuations in the coverage, opening a window into observing Brownian dynamics of unlabeled macromolecules. rnrnA further topic addressed in this thesis is the usability of the nanoruler, two nanospheres connected with a spacer molecule, as a stiffness sensor for the interparticle linker under strong illumination. Here, I discover a light induced collapse of the nanoruler. Furthermore, I exploit the sensing volume of a fixed nanorod to study unlabeled analytes diffusing around the nanorod at concentrations that are too high for fluorescence correlation spectroscopy but realistic for biological systems. Additionally, local pH sensing with nanoparticles is achieved.