OAI/Analysis/FiniteFactor/CompactGraphLusin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.continuousOn_of_compact_graph line 12

   Source documentation

   A function whose graph is compact above Q is continuous on Q.

   theorem continuousOn_of_compact_graph {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
       [T2Space X] {f : X → Y} {K : Set (X × Y)} (hK : IsCompact K)
       (hgraph : ∀ z ∈ K, f z.1 = z.2) : ContinuousOn f (Prod.fst '' K) := by
   …

2. theorem OAI.FiniteFactor.exists_compact_lusin line 39

   Source documentation

   Lusin's theorem on Polish spaces, obtained from compact subsets of the measurable graph. The compact set can be required to lie in a prescribed Borel conull set.

   theorem exists_compact_lusin {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
       [PolishSpace X] [PolishSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
       [BorelSpace X] [BorelSpace Y] (μ : Measure X) [IsFiniteMeasure μ]
       {f : X → Y} (hf : Measurable f) {s : Set X} (hs : MeasurableSet s)
       (hfull : ∀ᵐ x ∂μ, x ∈ s) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
       ∃ Q, Q ⊆ s ∧ IsCompact Q ∧ μ Qᶜ < ε ∧ ContinuousOn f Q := by
   …