From 6323fa3c5989dc3e4200f196fb448e429e52e842 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 30 Sep 2026 16:06:48 +0530 Subject: [PATCH] Prove unsigned composition closure of measurable functions --- Analysis/MeasureTheory/Section_1_3_2.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_3_2.lean b/Analysis/MeasureTheory/Section_1_3_2.lean index 613c9a3a..b4f46720 100644 --- a/Analysis/MeasureTheory/Section_1_3_2.lean +++ b/Analysis/MeasureTheory/Section_1_3_2.lean @@ -1791,7 +1791,13 @@ theorem UnsignedMeasurable.aeEqual {d:ℕ} {f g: EuclideanSpace' d → EReal} (h theorem UnsignedMeasurable.aeLimit {d:ℕ} {f: EuclideanSpace' d → EReal} (g: ℕ → EuclideanSpace' d → EReal) (hf: ∀ n, UnsignedMeasurable (g n)) (hfn : Unsigned f) (heq: PointwiseAeConvergesTo g f) : UnsignedMeasurable f := by sorry /-- Exercise 1.3.3(vi) -/ -theorem UnsignedMeasurable.comp_cts {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: UnsignedMeasurable f) {φ: EReal → EReal} (hφ: Continuous φ) (hφnn : ∀ x ≥ 0, φ x ≥ 0) : UnsignedMeasurable (φ ∘ f) := by sorry +theorem UnsignedMeasurable.comp_cts {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: UnsignedMeasurable f) {φ: EReal → EReal} (hφ: Continuous φ) (hφnn : ∀ x ≥ 0, φ x ≥ 0) : UnsignedMeasurable (φ ∘ f) := by + have hnonneg : Unsigned (φ ∘ f) := fun x => hφnn (f x) (hf.1 x) + have h_source : UnsignedMeasurable f ↔ ∀ U, IsOpen U → LebesgueMeasurable (f ⁻¹' U) := + (UnsignedMeasurable.TFAE hf.1).out 0 9 + have h_target : UnsignedMeasurable (φ ∘ f) ↔ ∀ U, IsOpen U → LebesgueMeasurable ((φ ∘ f) ⁻¹' U) := + (UnsignedMeasurable.TFAE hnonneg).out 0 9 + exact h_target.mpr fun U hU => h_source.mp hf (φ ⁻¹' U) (hU.preimage hφ) /-- Exercise 1.3.3(vii) -/ theorem UnsignedMeasurable.add {d:ℕ} {f g: EuclideanSpace' d → EReal} (hf: UnsignedMeasurable f) (hg: UnsignedMeasurable g) : UnsignedMeasurable (f + g) := by sorry