This file axiomatizes the needed definitions and properties of the Lebesgue integral. It ignores all issues of measurability, but otherwise attempts to only axiomatize well-known results in analysis and measure theory.

Definitions

Using bool instead of Prop for the definition of an event is a little unusual, but allows us to define an indicator function that produces real numbers (which are in the Set universe). It's very possible there are other solutions to this problem, such as using excluded_middle_informative.

ifte is a function version of "if then else" which allows tactics like f_equal can deal with it more easily.

Axioms of integration

Assume that integration exists for all (non-negative) functions.

Assume the general form of linearity for integration.

In order to do any useful integration, we will need to axiomatize several measures involving real numbers. Assume that Entropy has a probability measure on it

Assume the Lebesgue measure restricted to non-negative reals. Throw in ∞ too, but it's just one point so it has no mass.

Assume lebesgue(0, r) = r

Assume that Lebesgue integration can be expressed as a Riemann integral of the "layer cake" function. (Leib and Loss, 1997). Despite the promise in the name to relate Lebesgue and Riemann integrals, it is phrased here as a relation just between Lebesgue and Lebesgue. Since the Lebesuge integral is defined strictly more often than and always agrees with the Riemann integral, this is still a valid assumption. This assumption turns out to be very useful for proving equalities of integrals between measure-isomorphic domains. It also can provide a way to deal with integration by non-axiomatized measures, e.g. pushfowards.

This assumption is usually presented as the first step in the definition of the Lebesgue integral.

(Lemma 5 in paper) This axiom states that entropy can be split into 2 IID entropies.

Define convenient, Haskelly syntax for working with markov kernels as a monad in the spirit of Giry (1980) and Panangaden (1999). For lack of a better name, let's call the SRel+ because we're removing the subprobability restriction from SRel.

This is the associativity law for SRel+. Panangaden proved this for subprobabilities, but his proof makes no use of that restriction, and is therefore just as good of a proof in this instance.

An actual definition of σ-finite here would be more challenging than rewarding, so we instead simply construct a short whitelist of measures that are known to be sigma finite and are safe to apply Tonelli's theorem to.

We axiomitize Tonelli's theorem for all combinations of the two measures listed above.

Consequences of the axioms

Measure combinators

two different ways to convert emptiness in an option to emptiness in a measure.

Two ways to reweight a Meas A. unif_score_meas reweights the entire measure by a constant. score_meas reweights dependent on each element in A.

Lemmas about integrals

Tactic for showing ∫ f dμ = ∫ g dμ by pointwise equality of f and g.

Derive some more immediately useful forms of linearity.

Some lemmas about integrating by the new measures

The remaining two monad laws for SRel+

Measures that may be safely interchanged

Tonelli's theorem will be too restricted to be of immediate use in dealing with some of our measures. We will need to prove a wider class of measures than just sigma-finite ones can be involved in an integral interchange.

interchangable is a symmetric relation. Unfortunately we can't use the Symmetry typeclass because it's a relation between different types.

Other lemmas

Use the fact that μEntropy is a probability measure to lift constant functions out of integrals.

Repharse integration_πL_πR in terms of >>=

Apply bind_πL_πR thrice in a convenient-to-use manner

Even more convenient ways to apply bind_πL_πR! These are very similar to what the evaluation relation will look like, and will be easily be applied there.

Lemma 5 in paper