OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootLeafKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable full upper-root 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.UpperRootBox.aemeasurable_leafMeasure_restrict_window line 22
  2. theorem OAI.DukePrimeDegree.UpperRootBox.aemeasurable_leafMeasure line 58
  3. def OAI.DukePrimeDegree.UpperRootBox.leafKernel line 85
  4. lemma OAI.DukePrimeDegree.UpperRootBox.ae_leafKernel_eq line 94