Related papers: Covering theorems and Lebesgue integration

We characterize the positive radial continuous and rotation invariant valuations $V$ defined on the star bodies of $\mathbb R^n$ as the applications on star bodies which admit an integral representation with respect to the Lebesgue measure.…

Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in…

In this paper we compare different definitions of the (largest) Lebesgue number of a cover $\mathcal{U}$ for a metric space $X$. We also introduce the relative version for the Lebesgue number of a covering family $\mathcal{U}$ for a subset…

A non-negative function f, defined on the real line or on a half-line, is said to be directly Riemann integrable (d.R.i.) if the upper and lower Riemann sums of f over the whole (unbounded) domain converge to the same finite limit, as the…

Let $\Omega \subset \mathbb{R}^d$ be a set with finite Lebesgue measure such that, for a fixed radius $r>0$, the Lebesgue measure of $\Omega \cap B_r (x)$ is equal to a positive constant when $x$ varies in the essential boundary of…

Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects.…

In 1973, E.J. McShane proposed an alternative definition of the Lebesgue integral based on Riemann sums, where gauges are used decide what tagged partitions are allowed. Such an approach does not require any preliminary knowledge of Measure…

In the present paper, we study a set that can be treated as a generalised set of subsums for a geometric series. This object was discovered independently in various mathematical aspects. For instance, it is closely related to various…

We consider symmetric non-negative definite bilinear forms on algebras of bounded real valued functions and investigate closability with respect to the supremum norm. In particular, any Dirichlet form gives rise to a sup-norm closable…

In this note we construct a measure $\mu$ on a $\sigma$-algebra $\mathcal{M}$ of subsets of the positive real axis, $\mathbb{R}_{>0}$, with the following multiplicative property: \[ \mu \left( \bigcup_j E_j \right) = \prod_j \mu(E_j) \] for…

We prove that a Radon measure $\mu$ on $\mathbb{R}^n$ can be written as $\mu=\sum_{i=0}^n\mu_i$, where each of the $\mu_i$ is an $i$-dimensional rectifiable measure if and only if for every Lipschitz function $f:\mathbb{R}^n\to\mathbb{R}$…

A classical theorem of Lusin states that all analytic sets are Lebesgue-measurable. In this article we established the reverse mathematical strength of Lusin's theorem, which depends on how precisely it is formalized. By doing so, we answer…

Let $[q] = \{0,1,\ldots,q-1\}$, let $\Delta[q]$ denote the simplex of probability measures on $[q]$, and let $\gamma$ denote the Lebesgue measure normalized on $\Delta[q]$. We prove that for any symmetric monotone function $f \colon[q]^n…

We investigate tiling properties of spectra of measures, i.e., sets $\Lambda$ in $\br$ such that $\{e^{2\pi i \lambda x}: \lambda\in\Lambda\}$ forms an orthogonal basis in $L^2(\mu)$, where $\mu$ is some finite Borel measure on $\br$. Such…

In this paper we explore the connection between quantitative rectifiability of measures and the $L^2$ boundedness of the codimension one Riesz transform. Among other things, we prove the following. Let $\mu$ be a Radon measure in $\mathbb…

Let $\Omega \subseteq {\bf R}^d$ be an open set of measure 1. An open set $D \subseteq {\bf R}^d$ is called a ``tight orthogonal packing region'' for $\Omega$ if $D-D$ does not intersect the zeros of the Fourier Transform of the indicator…

This is a continuation of our previous work [13]. Let $(\Sigma,g)$ be a closed Riemann surface, where the metric $g$ has conical singularities at finite points. Suppose $\mathbf{G}$ is a group whose elements are isometries acting on…

Let $\{\Lambda_n=\{\lambda_{1,n},\ldots,\lambda_{d_n,n}\}\}_n$ be a sequence of finite multisets of real numbers such that $d_n\to\infty$ as $n\to\infty$, and let $f:\Omega\subset\mathbb R^d\to\mathbb R$ be a Lebesgue measurable function…

Some properties of $m$-density points and density-degree functions are studied. Moreover the following main results are provided: \vskip2mm \begin{itemize} \item {\it Let $\lambda$ be a continuous differential form of degree $h$ in…

We present a new type of integral that is supposed to extend the usability of the Lebesgue integral in certain types of investigations. It is based on the Hausdorff dimension and measure. We examine the basic properties of the integral and…