LeafLusin.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Compact sets with continuous root-leaf data

The Lusin step in EKL (2006), Section 4.3, is applied to a countable family of compactly supported tests determining locally finite real measures. A finer Polish topology and inner regularity provide a compact set in the original topology, outside any specified null set.

lemma OAI.DukePrimeDegree.continuousOn_of_finer_compact line 23

theorem OAI.DukePrimeDegree.exists_compact_continuousOn_outside_null line 40

Source documentation

A compact Lusin set avoiding a prescribed measurable null set.

theorem exists_compact_continuousOn_outside_null
    {Y Z : Type*} [tY : TopologicalSpace Y] [PolishSpace Y]
    [mY : MeasurableSpace Y] [BorelSpace Y]
    [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (f : Y → Z) (hf : Measurable f)
    (N : Set Y) (hN : MeasurableSet N) (hNzero : μ N = 0)
    (ε : ℝ≥0∞) (hε : ε ≠ 0) :
    ∃ K : Set Y, IsCompact K ∧ K ⊆ Nᶜ ∧ μ Kᶜ < ε ∧ ContinuousOn f K := by
…

theorem OAI.DukePrimeDegree.exists_compact_continuousOn_metrizable line 66

Source documentation

The compact-set version only needs a metrizable source and inner regularity; the source need not be equipped with a complete metric.

theorem exists_compact_continuousOn_metrizable
    {Y Z : Type*} [TopologicalSpace Y] [MetrizableSpace Y]
    [MeasurableSpace Y] [BorelSpace Y]
    [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z]
    (μ : Measure Y) [IsFiniteMeasure μ] [Measure.InnerRegularCompactLTTop μ]
    (f : Y → Z) (hf : Measurable f)
    (N : Set Y) (hN : MeasurableSet N) (hNzero : μ N = 0)
    (ε : ℝ≥0∞) (hε : ε ≠ 0) :
    ∃ K : Set Y, IsCompact K ∧ K ⊆ Nᶜ ∧ μ Kᶜ < ε ∧ ContinuousOn f K := by
…

def OAI.DukePrimeDegree.intrinsicLeafData line 116
lemma OAI.DukePrimeDegree.measurable_intrinsicLeafData line 123
lemma OAI.DukePrimeDegree.intrinsicLeafData_eq_iff line 132
theorem OAI.DukePrimeDegree.exists_compact_continuous_rootLeafData line 148