Mathlib.Measure­Theory.Analytic­Set­Universal­Measurability

theorem _root_.MeasureTheory.AnalyticSet.isCapacitable [PolishSpace Ω] {c : ChoquetCapacity Ω} {s : Set Ω} (hs : AnalyticSet s) : c.IsCapacitable s := by apply le_antisymm · rw [AnalyticSet] at hs rcases hs with rfl | ⟨f, hf, hfs⟩ · exact le_iSup_of_le ∅ (le_iSup_of_le (Set.empty_subset _) (le_iSup_of_le isCompact_empty le_rfl)) · subst hfs apply le_of_forall_lt_imp_le_of_dense intro t ht have hrange_union : range f = ⋃ k, f '' {g : ℕ → ℕ | g 0 ≤ k} := by rw [← Set.image_univ, show (Set.univ : Set (ℕ → ℕ)) = ⋃ k, {g : ℕ → ℕ | g 0 ≤ k} from by ext g simp [Set.mem_iUnion] exact ⟨g 0, le_refl _⟩, Set.image_iUnion] have hmono_base : Monotone (fun k => f '' {g : ℕ → ℕ | g 0 ≤ k}) := by intro a b hab exact Set.image_mono fun _ hx => hx.trans hab rw [hrange_union, c.iUnion_of_monotone' _ hmono_base] at ht obtain ⟨k₀, hk₀⟩ := lt_iSup_iff.mp ht have hcyl0 : f '' {g : ℕ → ℕ | g 0 ≤ k₀} = f '' Cyl (fun _ => k₀) 0 := by congr 1 ext g simp [Cyl] have rec_step : ∀ (M : ℕ → ℕ) (n : ℕ), t < c (f '' Cyl M n) → ∃ k, t < c (f '' Cyl (update M (n + 1) k) (n + 1)) := by intro M n hlt have hsplit : c (f '' Cyl M n) = ⨆ k, c (f '' (Cyl M n ∩ {g | g (n + 1) ≤ k})) := by conv_lhs => rw [cyl_succ_eq M n, Set.image_iUnion] exact c.iUnion_of_monotone' _ (fun _ _ h => Set.image_mono (monotone_cyl_split M n h)) rw [hsplit] at hlt obtain ⟨k, hk⟩ := lt_iSup_iff.mp hlt exact ⟨k, by rwa [cyl_inter_eq_cyl_update] at hk⟩ let build : (n : ℕ) → {M : ℕ → ℕ // t < c (f '' Cyl M n)} := fun n => Nat.rec ⟨fun _ => k₀, hcyl0 ▸ hk₀⟩ (fun m ⟨M, hM⟩ => ⟨Function.update M (m + 1) (choose (rec_step M m hM)), Classical.choose_spec (rec_step M m hM)⟩) n let Nseq : ℕ → (ℕ → ℕ) := fun n => (build n).val have hNseq_prop : ∀ n, t < c (f '' Cyl (Nseq n) n) := fun n => (build n).property have hNseq_consistent : ∀ n i, i ≤ n → Nseq (n + 1) i = Nseq n i := by intro n i hi show (update (Nseq n) (n + 1) _) i = Nseq n i exact Function.update_of_ne (by omega) .. let N : ℕ → ℕ := fun i => Nseq i i have hN_agree : ∀ n i, i ≤ n → N i = Nseq n i := by intro n induction n with | zero => intro i hi simp only [Nat.le_zero] at hi subst hi rfl | succ m ih => intro i hi by_cases heq : i = m + 1 · subst heq rfl · have him : i ≤ m := by omega show Nseq i i = Nseq (m + 1) i rw [hNseq_consistent m i him] exact ih i him have hcyl_eq : ∀ n, Cyl N n = Cyl (Nseq n) n := fun n => cyl_ext N (Nseq n) n (hN_agree n) have hcap_bound : ∀ n, t < c (f '' Cyl N n) := fun n => hcyl_eq n ▸ hNseq_prop n let K := f '' Bnd N have hK_compact : IsCompact K := (isCompact_bnd N).image hf have hK_sub : K ⊆ range f := Set.image_subset_range f _ have htK : t ≤ c K := by by_contra hnot have hcKt : c K < t := lt_of_not_ge hnot obtain ⟨U, hKU, hU, hcUt⟩ := c.exists_isOpen_superset_lt hK_compact hcKt obtain ⟨n, hn⟩ := exists_closure_image_cyl_subset hf N hU hKU have := (hcap_bound n).trans_le (c.mono subset_closure) exact (not_lt_of_ge hcUt.le) (this.trans_le (c.mono hn)) exact htK.trans (le_iSup_of_le K (le_iSup_of_le hK_sub (le_iSup_of_le hK_compact le_rfl))) · exact iSup_le fun K => iSup_le fun hKs => iSup_le fun _ => c.mono hKs

theorem lintegral_completion_eq_outerLIntegral [PolishSpace Ω] [BorelSpace Ω] {f : Ω → ℝ≥0∞} (hf : UpperSemianalytic f) (μ : Measure Ω) [IsFiniteMeasure μ] : (∫⁻ ω, f ω ∂μ.completion) = outerLIntegral μ f := by classical let m₀ : MeasurableSpace (NullMeasurableSpace Ω μ) := ‹MeasurableSpace Ω› have hm : m₀ ≤ (@NullMeasurableSpace.instMeasurableSpace Ω ‹MeasurableSpace Ω› μ) := by intro s hs change NullMeasurableSet s μ exact hs.nullMeasurableSet let μ' : @Measure (NullMeasurableSpace Ω μ) m₀ := by unfold m₀ NullMeasurableSpace exact μ have htrim : μ.completion.trim hm = μ' := by apply @Measure.ext (NullMeasurableSpace Ω μ) m₀ intro s hs rw [trim_measurableSet_eq hm hs] rfl have h_lintegral (g : Ω → ℝ≥0∞) (hg : Measurable g) : (∫⁻ ω, g ω ∂μ.completion) = ∫⁻ ω, g ω ∂μ := by have hμ' : (∫⁻ ω, g ω ∂μ') = ∫⁻ ω, g ω ∂μ := by unfold μ' m₀ NullMeasurableSpace rfl have hg' : @Measurable (NullMeasurableSpace Ω μ) ℝ≥0∞ m₀ _ g := by unfold m₀ NullMeasurableSpace exact hg have ht := @lintegral_trim (NullMeasurableSpace Ω μ) m₀ (@NullMeasurableSpace.instMeasurableSpace Ω ‹MeasurableSpace Ω› μ) μ.completion hm g hg' rw [← hμ', ← htrim] exact ht.symm rw [outerLIntegral] apply le_antisymm · refine le_iInf fun g ↦ le_iInf fun hg ↦ le_iInf fun hfg ↦ ?_ calc (∫⁻ ω, f ω ∂μ.completion) ≤ ∫⁻ ω, g ω ∂μ.completion := lintegral_mono hfg _ = ∫⁻ ω, g ω ∂μ := h_lintegral g hg · let hfm : AEMeasurable f μ := (hf.nullMeasurable μ).aemeasurable let g : Ω → ℝ≥0∞ := hfm.mk f have hgm : Measurable g := hfm.measurable_mk have hfg : f =ᵐ[μ] g := hfm.ae_eq_mk have hDnull : μ {ω | f ω ≠ g ω} = 0 := by rw [← compl_mem_ae_iff] have hfg' : {ω | f ω = g ω} ∈ ae μ := hfg simpa only [compl_setOf, Classical.not_not] using hfg' obtain ⟨N, hDN, hNm, hNnull⟩ := exists_measurable_superset_of_null hDnull let G : Ω → ℝ≥0∞ := N.piecewise (fun _ ↦ ⊤) g have hGm : Measurable G := by fun_prop have hfG : f ≤ G := by intro ω by_cases hω : ω ∈ N · simp [G, hω] · have hEq : f ω = g ω := by by_contra hne exact hω (hDN hne) simp [G, hω, hEq] have hGg : G =ᵐ[μ] g := by filter_upwards [compl_mem_ae_iff.2 hNnull] with ω hω have hωN : ω ∉ N := by simpa using hω simp [G, hωN] have hGf : G =ᵐ[μ.completion] f := by rw [μ.ae_completion] exact hGg.trans hfg.symm have houter : (⨅ (g : Ω → ℝ≥0∞) (_ : Measurable g) (_ : f ≤ g), ∫⁻ ω, g ω ∂μ) ≤ ∫⁻ ω, G ω ∂μ := iInf₂_le_of_le G hGm (iInf_le_of_le hfG le_rfl) calc (⨅ (g : Ω → ℝ≥0∞) (_ : Measurable g) (_ : f ≤ g), ∫⁻ ω, g ω ∂μ) ≤ ∫⁻ ω, G ω ∂μ := houter _ = ∫⁻ ω, G ω ∂μ.completion := (h_lintegral G hGm).symm _ = ∫⁻ ω, f ω ∂μ.completion := lintegral_congr_ae hGf