OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixLeafKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable remaining-subgroup leaf kernels

The chosen leaf measure is measurable almost everywhere because its restrictions to the countable exhausting windows are actual normalized conditional kernels. This supplies a measurable kernel for integration.

  1. lemma OAI.DukePrimeDegree.RootPrefixBox.aemeasurable_leafMeasure_restrict_window line 26
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.aemeasurable_leafMeasure line 62
  3. def OAI.DukePrimeDegree.RootPrefixBox.leafKernel line 89
  4. lemma OAI.DukePrimeDegree.RootPrefixBox.ae_leafKernel_eq line 98