arXiv subjects

Tetsuya Sato

Publications and source records attributed to Tetsuya Sato.

At least 19 recordsLinked to original sources

arXiv2026

Edgeworth expansions in sphericity testing under high-dimensional two-step monotone incomplete data and their computable error bounds

In this paper, we consider the sphericity test for a one-sample problem under high-dimensional two-step monotone incomplete data. Existing asymptotic expansions for the null distributions of the likelihood ratio test (LRT) statistic and modified LRT statistic deteriorate in high-dimensional settings. Therefore, we derive an Edgeworth expansion for the null distribution of the LRT statistic in such settings and obtain its computable error bounds. Furthermore, we demonstrate that our proposed Edgeworth expansion provide better approximation accuracy than the existing asymptotic expansion. We also conduct numerical experiments using Monte Carlo simulations to evaluate the maximum absolute error between the distribution function of the standardized test statistic and the Edgeworth expansion for the null distribution of the LRT statistic, as well as to assess the performance of the computable error bounds. Finally, by deriving a Cornish-Fisher expansion for the null distribution of the LRT statistic in high-dimensional settings, we evaluate the empirical Type I error rates via Monte Carlo simulations.

math.ST↗

arXiv2025

Multipolar orbital relaxation of the $t_{2g}$ states

Using a nonperturbative approach, the relaxation rate of orbital dipolar and quadrupolar moments is computed analytically for the t2g states. In the presence of short-range impurities and in the absence of spin-orbit coupling, the orbital relaxation emerges from the competition between momentum scattering and the effect of the crystal field. In the case of weak disorder, the orbital relaxation time is proportional to the momentum scattering time: each scattering event contributes to destroying the orbital moment. In the case of strong disorder, the effect of the crystal field is averaged out, and the orbital relaxation time is inversely proportional to the momentum scattering. We finally find that the dipolar and quadrupolar orbital moments are coupled by the crystal field, resulting in a complex dynamical behavior upon orbital injection.

cond-mat.mes-hall↗

arXiv2025

Orbital Accumulation Induced by Chiral Phonons

We theoretically investigate orbital accumulation driven by chiral phonons via orbital-dependent electron-lattice coupling. We derive a formula for the orbital accumulation induced by classical lattice dynamics or nonequilibrium phonons, emphasizing the rectified second-order response of the orbital moment to lattice displacement. We show that chiral phonons primarily couple to orbital quadrupole moments and that static orbital dipole accumulation can be generated at second order in the lattice displacement. Our study provides a useful method for generating orbital accumulation without using spin-orbit interactions and suggests a strategy to boost its magnitude by harnessing band structure hot spots associated with orbital degeneracy.

cond-mat.mes-hall↗

arXiv2024

Formalization of Differential Privacy in Isabelle/HOL

Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism.

cs.LO↗

arXiv2024

Fluctuations in Spin Dynamics Excited by Pulsed Light

We theoretically investigate nonequilibrium spin fluctuations in a ferromagnet induced by a light pulse. Using a Lindblad equation consistent with the Landau-Lifshitz-Gilbert equation, we compute the autocorrelation function of magnetization. Our analysis reveals that this function comprises both thermal and nonequilibrium components. To examine the latter in detail, we introduce a Fano factor similar to nonequilibrium current noise in electronic circuits. We demonstrate that this factor encapsulates insights into the transfer of spin units to the environment. Our findings lay the groundwork for nonequilibrium spin noise spectroscopy, offering valuable insights into spin relaxation dynamics.

cond-mat.mes-hall↗

arXiv2023

Formalizing Statistical Causality via Modal Logic

We propose a formal language for describing and explaining statistical causality. Concretely, we define Statistical Causality Language (StaCL) for expressing causal effects and specifying the requirements for causal inference. StaCL incorporates modal operators for interventions to express causal properties between probability distributions in different possible worlds in a Kripke model. We formalize axioms for probability distributions, interventions, and causal predicates using StaCL formulas. These axioms are expressive enough to derive the rules of Pearl's do-calculus. Finally, we demonstrate by examples that StaCL can be used to specify and explain the correctness of statistical causal inference.

cs.AI↗

arXiv2022

Appearance of ferromagnetism in Pt(100) ultrathin films originated from quantum-well states

Ferromagnetism was observed in a Pt(100) ultrathin film deposited on a SrTiO3(100) substrate. The ferromagnetism, which appears in films with thicknesses of 2.2-4.4 nm, periodically changes with a period of approximately 1 nm (5-6 monolayers) depending on the film thickness. This is consistent with the period derived from the quantum-well states formed in the thin film. X-ray magnetic circular dichroism measurements show the evidence of appearance of intrinsic ferromagnetism in Pt(100) ultra-thin film. In addition, present results suggest a possibility that the orbital magnetic moment of pure Pt is much smaller than that of the Pt/ferromagnetic multilayer system. These results will provide a potential new mechanism for origin of the large magnetic anisotropy in Pt components.

cond-mat.mtrl-sci↗

arXiv2022

Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs

We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, we define belief Hoare logic (BHL) for formalizing and reasoning about the statistical beliefs acquired via hypothesis testing. This program logic is sound and relatively complete with respect to a Kripke model for hypothesis tests. We demonstrate by examples that BHL is useful for reasoning about practical issues in hypothesis testing. In our framework, we clarify the importance of prior beliefs in acquiring statistical beliefs through hypothesis testing, and discuss the whole picture of the justification of statistical inference inside and outside the program logic.

cs.AI↗

arXiv2022

Divergences on Monads for Relational Program Logics

Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Towards a general framework for such logics, in this paper, we formalize quantitative difference between computational effects as divergence on monad, then develop a relational program logic acRL that supports generic computational effects and divergences on them. To give a categorical semantics of acRL supporting divergences, we give a method to obtain graded strong relational liftings from divergences on monads. We derive two instantiations of acRL for the verification of 1) various differential privacy of higher-order functional probabilistic programs and 2) difference of distribution of costs between higher-order functional programs with probabilistic choice and cost counting operations.

cs.PL↗

arXiv2021

Fluctuation theorem for spin transport at insulating ferromagnetic junctions

General relations for nonequilibrium spin transport at a magnetic junction between a normal metal and a ferromagnetic insulator are derived from the quantum fluctuation theorem. They include the extended Onsager relations between the spin conductance and the spin-current noise that hold for nonequilibrium states driven by an external current. These relations, that are valid for a general setup of spin Hall magnetoresistance, provide a comprehensive viewpoint for understanding of unidirectional spin Hall magnetoresistance in insulating ferromagnetic junctions.

cond-mat.mes-hall↗

arXiv2021

Higher-order probabilistic adversarial computations: Categorical semantics and program logics

Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed $λ$-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.

cs.LO↗

arXiv2021

Graded Hoare Logic and its Categorical Semantics

Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.

cs.LO↗

arXiv2020

Formal verification of higher-order probabilistic programs

Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru, derive their expressiveness from a powerful combination of continuous distributions, conditioning, and higher-order functions. Although very important for practical applications, these combined features raise fundamental challenges for program semantics and verification. Several recent works offer promising answers to these challenges, but their primary focus is on semantical issues. In this paper, we take a step further and we develop a set of program logics, named PPV, for proving properties of programs written in an expressive probabilistic higher-order language with continuous distributions and operators for conditioning distributions by real-valued functions. Pleasingly, our program logics retain the comfortable reasoning style of informal proofs thanks to carefully selected axiomatizations of key results from probability theory. The versatility of our logics is illustrated through the formal verification of several intricate examples from statistics, probabilistic inference, and machine learning. We further show the expressiveness of our logics by giving sound embeddings of existing logics. In particular, we do this in a parametric way by showing how the semantics idea of (unary and relational) TT-lifting can be internalized in our logics. The soundness of PPV follows by interpreting programs and assertions in quasi-Borel spaces (QBS), a recently proposed variant of Borel spaces with a good structure for interpreting higher order probabilistic programs.

cs.LO↗

arXiv2019

Relational $\star$-Liftings for Differential Privacy

Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. This construction can be defined in two styles. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have each have their own strengths: the universal version is more general than the existential ones, while existential liftings are known to satisfy more precise composition principles. We propose a novel, existential version of approximate lifting, called $\star$-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, yielding cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and consider more general approximate liftings based on $f$-divergences.

cs.LO↗

arXiv2019

Switching of magnetism via modifying phase shift of quantum-well states by tailoring the interface electronic structure

We demonstrate control of the magnetism of Pd(100) ultrathin films, which show d-electron quantum-well induced ferromagnetism, via modulation of the interface electronic state using density functional calculation. From an analysis based on the phase model, forming the Au/Pd(100) interface induces hybridization of the wave function of d-electron quantum-well states, and modulates the term of the scattering phase shift as a function of the reciprocal lattice point. In contrast, forming the Al interface, which has only s-electrons at the Fermi energy, cannot modify the scattering phase shift. Our finding indicates the possibility of modifying the phase shift by tailoring the interface electronic states using hybridization of the wave function, and this efficiently changes the density of states near the Fermi energy of Pd films, and the switching between paramagnetism and ferromagnetism occurs based on the condition for ferromagnetism (Stoner criterion).

cond-mat.mtrl-sci↗

arXiv2019

Hypothesis Testing Interpretations and Renyi Differential Privacy

Differential privacy is a de facto standard in data privacy, with applications in the public and private sectors. A way to explain differential privacy, which is particularly appealing to statistician and social scientists is by means of its statistical hypothesis testing interpretation. Informally, one cannot effectively test whether a specific individual has contributed her data by observing the output of a private mechanism---any test cannot have both high significance and high power. In this paper, we identify some conditions under which a privacy definition given in terms of a statistical divergence satisfies a similar interpretation. These conditions are useful to analyze the distinguishability power of divergences and we use them to study the hypothesis testing interpretation of some relaxations of differential privacy based on Renyi divergence. This analysis also results in an improved conversion rule between these definitions and differential privacy.

cs.LG↗

arXiv2019

Manipulation of magnetization in Pd(100) ultrathin films with quantum well structure using modification of Schottky barrier potentials

The magnetization of Pd(100) ultrathin films that show ferromagnetism due to quantum well states was manipulated by changing the quantum well state with an applied bias voltage. The voltage dependence of the magnetic moment of Pd/SrTiO$_{3-x}$/Ti/Au intrinsically depends on the Pd film thickness. The induced change in the magnetic moment is due to the modulation of the phase shift at the interface between the Pd thin film and the semiconductor SrTiO$_{3-x}$ substrate.

cond-mat.mtrl-sci↗

arXiv2018

Codensity Lifting of Monads and its Dual

We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations which were not supported by its precursor, categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended pseudometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We also introduce the dual method called density lifting of comonads. We next study the liftings of algebraic operations to the codensity liftings of monads. We also give a characterisation of the class of liftings of monads along posetal fibrations with fibred small meets as a limit of a certain large diagram.

cs.LO↗