Terence Tao Formalising Riemann-Stieltjes Integrals in Lean Mathlib

6:03 In Mathlib they try to formalise theories at the highest level of abstraction they can to avoid having to prove the same theorems many times for specific instantiations.  So for example, they use a general multi-dimensional integration theory of box-additive measures in Mathlib.Analysis.BoxIntegral.Basic:

In this file we define the integral of a function over a box in ℝⁿ. The same definition works for Riemann, Henstock-Kurzweil, and McShane integrals.

As usual, we represent ℝⁿ as the type of functions ι → ℝ for some finite type ι. A rectangular box (l, u] in ℝⁿ is defined to be the set {x : ι → ℝ | ∀ i, l i < x i ∧ x i ≤ u i}, see BoxIntegral.Box.

Let vol be a box-additive function on boxes in ℝⁿ with codomain E →L[ℝ] F. Given a function f : ℝⁿ → E, a box I and a tagged partition π of this box, the integral sum of f over π with respect to the volume vol is the sum of vol J (f (π.tag J)) over all boxes of π. Here π.tag J is the point (tag) in ℝⁿ associated with the box J.... 

When they prove the Fundamental Theorem of Calculus they do it for interval integrals in ℝ. See Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus. 

See Kathryn Hess - Comonads to Calculus and Vladimir Voevodsky - What if Current Foundations of Mathematics are Inconsistent. 

See Riemann–Stieltjes integral on Wikipedia and Box Integral on Wolfram Mathworld. 

Subscribe to Terence Tao. 

See Compression is all you need: Modeling Mathematics by Vitaly Aksenov, Eve Bodnia, Michael H. Freedman and Michael Mulligan .

 Subscribe to SAIR.

Today I found traces of a connection that doesn't seem to be very well known. It's that an Abstract Simplicial Complex which satisfies the Augmentation Property is a Matroid, and a Finite Simple Matroid is a Geometric Lattice. Then Simplicial sets are used to define quasi-categories, a basic notion of higher category theory. A construction analogous to that of simplicial sets can be carried out in any category, not just in the category of sets, yielding the notion of simplicial objects. See also Vladimir Voevodsky's talk on the meta-mathematical theory of dependent types in Thierry Coquand on Computational Interpretation of Topos Theory. 

See also Stefan Milius - Demystifying Codensity Monads through Duality for more on filters and ideals. 

See Mike Titelbaum and Ted Theodosopoulos - Topological Obstacles to Shared Priors.