INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
The HOL-Light library of Multivariate Real analysis in Rocq
No full textInternational audienceIn this paper we present Coq-HOL-Light, a library with more than 20,000 mathematical theorems on Real analysis in Rocq. This library is a translation from the HOL-Light proof assistant. By proving the equivalence between a number of types, functions and predicates in HOL-Light and their counterpart in the Rocq standart library, we make this library directly usable in Rocq developments. We also present our indexing and retrieval tools, specially tailored for searching mathematical entities in the Coq-HOL-Light library with special facilities for the Rocq community. All tools underpinning our methodology are publicly available guarantying the reproducibility of the processes detailed in this paper. We argue that this work is relevant to researchers and practitioners who wish to harness HOL-Light's comprehensive analysis library to support the construction of Rocq developments
Quantum theory does not need complex numbers
No full textThe longstanding debate over whether quantum theory fundamentally requires complex numbers-or if their use is merely a convenient choice-has persisted for decades. Until recently, this question was considered open. However, in [M.-O. Renou et al, Nature 600, 625-629, 2021], a decisive argument was presented asserting that quantum theory needs complex numbers. In this work, we demonstrate that a formulation of quantum theory based solely on real numbers is indeed possible while retaining key features such as theory-representation locality (i.e. local physical operations are represented by local changes to the states) and the positive semi-definiteness of its states and effects. We observe that the standard system combination rule-the tensor product-was derived after the development of single-system complex quantum theory. By starting from a single-system quantum theory using only real numbers, we derive a combination rule that produces a real quantum theory with properties analogous to those of conventional complex quantum theory. We also prove that the conventional tensor product rule can also lead to a real and representation-local theory, albeit with a modified characterization of the state space. We thus conclude that complex numbers are a mere convenience in quantum theory. CONTENTS 1. Positivity-preserving mapping on a single system 2. Positivity-preserving mapping on two subsystems C. Explicit constructions of the M (•) map D. Proof of Theorem 2
Leveraging Multimodal Explanatory Annotations For Video Interpretation With Modality Specific Dataset
No full textWe examine the impact of concept-informed supervision on multimodal video interpretation models using MOByGaze, a dataset containing human-annotated explanatory concepts. We introduce Concept Modality Specific Datasets (CMSDs), which consist of data subsets categorized by the modality (visual, textual, or audio) of annotated concepts. Models trained on CMSDs outperform those using traditional legacy training in both early and late fusion approaches. Notably, this approach enables late fusion models to achieve performance close to that of early fusion models. These findings underscore the importance of modality-specific annotations in developing robust, self-explainable video models and contribute to advancing interpretable multimodal learning in complex video analysis
Optimal sub-Gaussian variance proxy for truncated Gaussian and exponential random variables
No full textInternational audienceThis paper establishes the optimal sub-Gaussian variance proxy for truncated Gaussian and truncated exponential random variables. The proofs are based initially on reducing each distribution to their standardized versions. Geometrically, for the normal distribution, our argument consists of fitting a parabola to another parabola-looking function, which emerges from its moment generating function. For the exponential case, we show that the optimal variance proxy is the unique solution to a pair of equations and then provide this solution explicitly. Moreover, we demonstrate that truncated Gaussian variables exhibit strict sub-Gaussian behavior if and only if they are symmetric, meaning their truncation is symmetric with respect to the mean. Conversely, truncated exponential variables are shown to never exhibit strict sub-Gaussianity
Harnessing ecological niche modeling of Listeria monocytogenes for biopreservation system engineering
No full textInternational audienceBiopreservation is a microbiome engineering technology based on the use of microorganisms as protective cultures and/or their metabolites, which can be used to mitigate the presence of pathogens in food. This study explores the potential of ecological niche modeling to guide the selection of biopreservation candidates. A luminescent strain of Listeria monocytogenes was utilized in a multivariate high-throughput competition assay, assessing a combination of abiotic factors (i.e. glucose, NaCl, pH in a factorial design) and biotic variables (i.e. various competing microorganisms). The resulting data were analyzed using two parallel methods: k-means clustering and Response Surface Modeling (RSM). Integrating the outputs of these approaches allowed for grouping competitors based on both inhibition strength and niche modeling characteristics. Competitors were categorized into five groups, distinguished by their inhibition levels against L. monocytogenes and the shape of their response surfaces, with some groups displaying complementary features. Weighted Niche Reduction (WNR) calculations derived from model predictions identified the strain combination Carnobacterium maltaromaticum CP14 and Leuconostoc pseudomesenteroides PTF6 as having enhanced inhibitory properties. This study highlights promising possibilities for the bottom-up engineering of synthetic communities for biopreservation applications
Intermediation Platforms and Geopolitical Asymmetries, Lessons from a Pandemic
No full textInternational audienceTo a large extent, and particularly before vaccines became available, human societies owed their resilience during the COVID-19 pandemic to non-pharmaceutical interventions, i.e. social distancing combined with more invasive digital systems. In this paper, we consider the digital applications developed during 2020-2021, the two first years of the pandemic. We introduce a typology based on the services offered and the data flows they require, between both public and private actors. A detailed timeline of these developments shows that countries’ strategies have evolved in strong coherence with their overall digital policy. Our study demonstrates that this exogenous crisis has reinforced the critical role of intermediation platforms for maintaining society’s essential functions. Their increased centrality has contributed to intensifying information asymmetries and power imbalances, already at stake before the pandemic, both between platforms and states, as well as between countries, leading to new geopolitical equilibria
An inquiry into Search Engine Neutrality: the case of movements against police violence in France and the U.S.
No full textInternational audienceThe digital transformation has revolutionized information consumption, with search engines playing a pivotal role in shaping user access to diverse media. Employing algorithms, these engines influence content visibility and aggregate news sources, significantly molding public opinion. As gatekeepers of information, search engines impact media outlet visibility, affecting online traffic, revenue, and journalistic diversity. In breaking news and societal issues, search engines expedite information dissemination, influencing initial narratives. Understanding their role is crucial for transparency and user access to diverse information. Focusing on movements against police violence, our paper conducts a comparative analysis across 12 search engines for terms "Black Lives Matter" and "Justice pour Adama". Our innovative methodology identifies biases in information diversity, providing insights into the dynamics shaping visibility of societal issues.</div
Target trial emulation to replicate randomised clinical trials using registry data in multiple sclerosis
No full textInternational audienceBackground: Target trial emulation (TTE) offers a formal framework for causal inference using observational data, but its validity must be evaluated in each research domain by replicating randomised clinical trials (RCTs). We aimed to replicate eight RCTs evaluating the efficacy of disease-modifying therapies (DMTs) in multiple sclerosis (MS) using French registry data.Methods: This multicentre, retrospective, observational study was conducted using data extracted in December 2023 from the Observatoire Français de la Sclérose en Plaques (OFSEP) database. For each emulated trial, patients were included when they initiated one of the DMT evaluated in the corresponding RCT and met its inclusion criteria. Clinical outcomes were the annualised relapse rate and 3-month confirmed Expanded Disability Status Scale progression. Radiological outcomes were new/enlarged T2-lesions and new gadolinium-enhanced T1-lesions on a brain MRI. A targeted maximum likelihood estimator was used to estimate the treatment effect adjusted for confounding factors between groups and corrected for censoring and missing outcome assessment.Results: 14 111 patients were included in eight emulated trials: ASSESS (fingolimod vs glatiramer acetate), BEYOND (interferon beta vs glatiramer acetate), CONFIRM (dimethyl fumarate (DMF) vs glatiramer acetate), OPERA (ocrelizumab vs interferon beta), REGARD (interferon beta vs glatiramer acetate), RIFUND-MS (rituximab vs DMF), TENERE (teriflunomide vs interferon beta) and TRANSFORMS (fingolimod vs interferon beta). Treatment effects estimated in emulated trials were concordant with RCT findings in seven of eight trials for relapse rate, and in all six trials assessing disability progression. Radiological outcomes were more challenging to replicate; concordance was achieved in three of five trials for new T2-lesions, and one of four trials for new gadolinium-enhanced T1-lesions.Conclusion: The combined use of a TTE methodology and high-quality registry data is a valid tool to evaluate treatment effectiveness in MS
Separation rates for the detection of synchronization of interacting point processes in a mean field frame. Application to neuroscience.
No full textInternational audiencePermutation tests have been proposed by Albert et al. (2015) to detect dependence between point processes, modeling in particular spike trains, that is the time occurrences of action potentials emitted by neurons. Our present work focuses on exhibiting a criterion on the separation rate to ensure that the Type II errors of these tests are controlled non asymptotically. This criterion is then discussed in two major models in neuroscience: the jittering Poisson model and Hawkes processes having components interacting in a mean field frame and evolving in stationary regime. For both models, we obtain a lower bound of the size of the sample necessary to detect the dependency between two neurons