diff --git a/.gitignore b/.gitignore
index 9a6c5c58..1ec55595 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,7 +17,10 @@ _site/
 .cursor/
 Claude.md
 analysis/.repair
+**/.env
+**/.aider.conf.yml
 
 # miscellaneous files
 **/tobeIgnored/
-**/tmp
\ No newline at end of file
+**/tmp
+**/docker/
\ No newline at end of file
diff --git a/analysis/Analysis/MeasureTheory/Section_1_3_1.lean b/analysis/Analysis/MeasureTheory/Section_1_3_1.lean
index 77fa3be0..a1b5a35a 100644
--- a/analysis/Analysis/MeasureTheory/Section_1_3_1.lean
+++ b/analysis/Analysis/MeasureTheory/Section_1_3_1.lean
@@ -36,7 +36,18 @@ def ComplexSimpleFunction {d:ℕ} (f: EuclideanSpace' d → ℂ) : Prop := ∃ (
 
 
 @[coe]
-abbrev RealSimpleFunction.toComplex {d:ℕ} (f: EuclideanSpace' d → ℝ) (df: RealSimpleFunction f) : ComplexSimpleFunction (Real.complex_fun f) := by sorry
+abbrev RealSimpleFunction.toComplex {d:ℕ} (f: EuclideanSpace' d → ℝ) (df: RealSimpleFunction f) : ComplexSimpleFunction (Real.complex_fun f) := by
+  obtain ⟨k, c, E, hmes, heq⟩ := df
+  use k, fun i => Complex.ofReal (c i), E
+  constructor
+  · exact hmes
+  · ext x
+    simp only [Real.complex_fun, Complex.indicator, heq]
+    simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+    rw [Complex.ofReal_sum]
+    congr 1
+    ext i
+    exact Complex.ofReal_mul (c i) ((E i).indicator' x)
 
 instance RealSimpleFunction.coe_complex {d:ℕ} (f: EuclideanSpace' d → ℝ) : Coe (RealSimpleFunction f) (ComplexSimpleFunction (Real.complex_fun f)) := {
   coe := RealSimpleFunction.toComplex f
@@ -700,6 +711,78 @@ lemma weightedMeasureSum_eq_of_eq {d k k' : ℕ}
         congr 1; ext i; congr 1; exact (hmes_decomp' i).symm
     _ = weightedMeasureSum c' E' := rfl
 
+/-! ### Single-family atoms (k' = 0 specialization)
+
+When working with a single family of sets (no second family to compare against),
+we specialize the atom machinery with k' = 0. -/
+
+/-- The atom for a single family of sets, using k' = 0 in the general atom definition -/
+def singleAtom {X : Type*} {k : ℕ} (E : Fin k → Set X) (n : Fin (2^k)) : Set X :=
+  atom E (fun _ : Fin 0 => ∅) ⟨n.val, by simp only [add_zero]; exact n.isLt⟩
+
+/-- Single atoms are pairwise disjoint -/
+lemma singleAtom_pairwiseDisjoint {X : Type*} {k : ℕ} (E : Fin k → Set X) :
+    Set.univ.PairwiseDisjoint (singleAtom E) := by
+  intro i _ j _ hij
+  simp only [Function.onFun, singleAtom]
+  have hlt_i : i.val < 2^(k+0) := by simp only [add_zero]; exact i.isLt
+  have hlt_j : j.val < 2^(k+0) := by simp only [add_zero]; exact j.isLt
+  have hij' : (⟨i.val, hlt_i⟩ : Fin (2^(k+0))) ≠ ⟨j.val, hlt_j⟩ := by
+    intro h; apply hij; ext; exact Fin.mk.inj h
+  exact atom_pairwiseDisjoint E (fun _ : Fin 0 => ∅) (by simp : i ∈ Set.univ) (by simp : j ∈ Set.univ) hij'
+
+/-- Membership in singleAtom is determined by bit pattern -/
+lemma mem_singleAtom_iff {X : Type*} {k : ℕ} (E : Fin k → Set X) (n : Fin (2^k)) (x : X) :
+    x ∈ singleAtom E n ↔ ∀ i : Fin k, n.val.testBit i.val ↔ x ∈ E i := by
+  simp only [singleAtom, atom, Set.mem_setOf_eq]
+  constructor
+  · intro ⟨h1, _⟩ i
+    specialize h1 i
+    rw [atomMembership_eq_testBit] at h1
+    convert h1 using 1
+  · intro h
+    constructor
+    · intro i
+      rw [atomMembership_eq_testBit]
+      exact h i
+    · intro i; exact Fin.elim0 i
+
+/-- Every point is in exactly one singleAtom -/
+lemma exists_unique_singleAtom {X : Type*} [DecidableEq X] {k : ℕ} (E : Fin k → Set X) (x : X) :
+    ∃! n : Fin (2^k), x ∈ singleAtom E n := by
+  let n : ℕ := atomIndexOf E (fun _ : Fin 0 => ∅) x
+  have hn_lt : n < 2^k := by
+    have := atomIndexOf_lt E (fun _ : Fin 0 => ∅) x
+    simp only [add_zero] at this
+    exact this
+  use ⟨n, hn_lt⟩
+  constructor
+  · simp only
+    rw [mem_singleAtom_iff]
+    intro i
+    exact atomIndexOf_testBit_E E (fun _ : Fin 0 => ∅) x i
+  · intro m hm
+    ext
+    rw [mem_singleAtom_iff] at hm
+    apply Nat.eq_of_testBit_eq
+    intro j
+    by_cases hj : j < k
+    · have h1 := hm ⟨j, hj⟩
+      have h2 := atomIndexOf_testBit_E E (fun _ : Fin 0 => ∅) x ⟨j, hj⟩
+      by_cases hx : x ∈ E ⟨j, hj⟩
+      · rw [h1.mpr hx, h2.mpr hx]
+      · have hm_false : (m.val.testBit j) = false := Bool.eq_false_iff.mpr (fun ht => hx (h1.mp ht))
+        have hn_false : (n.testBit j) = false := Bool.eq_false_iff.mpr (fun ht => hx (h2.mp ht))
+        rw [hm_false, hn_false]
+    · have hm_lt : m.val < 2^k := m.isLt
+      have hn_lt' : (atomIndexOf E (fun _ : Fin 0 => ∅) x) < 2^k := hn_lt
+      rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hm_lt (Nat.pow_le_pow_right (by norm_num : 1 ≤ 2) (le_of_not_gt hj)))]
+      rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hn_lt' (Nat.pow_le_pow_right (by norm_num : 1 ≤ 2) (le_of_not_gt hj)))]
+
+/-- The value on atom n is the sum of coefficients for sets containing that atom -/
+noncomputable def atomValue {k : ℕ} (c : Fin k → ℝ) (n : Fin (2^k)) : ℝ :=
+  ∑ i : Fin k, if n.val.testBit i.val then c i else 0
+
 end UnsignedSimpleFunction.IntegralWellDef
 
 /-- Lemma 1.3.4 (Well-definedness of simple integral) -/
@@ -741,18 +824,201 @@ def AlmostEverywhereEqual {d:ℕ} {X: Type*} (f g: EuclideanSpace' d → X) : Pr
 def Support {X Y: Type*} [Zero Y] (f: X → Y) : Set X := { x | f x ≠ 0 }
 
 lemma UnsignedSimpleFunction.support_measurable {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: UnsignedSimpleFunction f) : LebesgueMeasurable (Support f) := by
-  sorry
+  -- Extract the representation: f = ∑ i, c(i) • EReal.indicator(E_i)
+  obtain ⟨k, c, E, hmes_nonneg, heq⟩ := hf
+  -- Define E' i = E i if c i > 0, else ∅
+  let E' : Fin k → Set (EuclideanSpace' d) := fun i => if c i > 0 then E i else ∅
+  -- Each E' i is measurable
+  have hE'_meas : ∀ i, LebesgueMeasurable (E' i) := fun i => by
+    simp only [E']
+    split_ifs with h
+    · exact (hmes_nonneg i).1
+    · exact LebesgueMeasurable.empty
+  -- Key: Support f = ⋃ i, E' i
+  have h_eq : Support f = ⋃ i, E' i := by
+    ext x
+    simp only [Support, Set.mem_setOf_eq, Set.mem_iUnion, E']
+    constructor
+    · -- (⊆) If f(x) ≠ 0, some c_i > 0 and x ∈ E_i
+      intro hne
+      rw [heq] at hne
+      simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] at hne
+      -- Sum of nonneg terms is nonzero, so some term is nonzero
+      have h_exists := Finset.exists_ne_zero_of_sum_ne_zero hne
+      obtain ⟨i, _, hi_ne⟩ := h_exists
+      use i
+      -- c i * indicator ≠ 0 means c i > 0 and x ∈ E i
+      by_cases hc : c i > 0
+      · simp only [hc, ↓reduceIte]
+        by_cases hx : x ∈ E i
+        · exact hx
+        · -- If x ∉ E i, then indicator is 0, so c i * 0 = 0, contradiction
+          simp only [EReal.indicator, Real.EReal_fun, Set.indicator'_of_notMem hx,
+                     EReal.coe_zero, mul_zero] at hi_ne
+          exact absurd rfl hi_ne
+      · -- c i ≤ 0, but c i ≥ 0, so c i = 0
+        have hc_zero : c i = 0 := le_antisymm (le_of_not_gt hc) (hmes_nonneg i).2
+        simp only [hc_zero, zero_mul] at hi_ne
+        exact absurd rfl hi_ne
+    · -- (⊇) If x ∈ E' i for some i, then f(x) ≠ 0
+      intro ⟨i, hi⟩
+      split_ifs at hi with hc
+      · -- c i > 0 and x ∈ E i
+        rw [heq]
+        simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+        -- f(x) ≥ c i * indicator(E i)(x) = c i > 0
+        have h_term_pos : c i * EReal.indicator (E i) x > 0 := by
+          simp only [EReal.indicator, Real.EReal_fun, Set.indicator'_of_mem hi,
+                     EReal.coe_one, mul_one]
+          exact hc
+        -- Sum of nonneg terms with one positive term is positive
+        have h_sum_nonneg : ∀ j, 0 ≤ c j * EReal.indicator (E j) x := fun j =>
+          mul_nonneg (hmes_nonneg j).2 (EReal.indicator_nonneg' (E j) x)
+        have h_sum_pos : 0 < ∑ j : Fin k, c j * EReal.indicator (E j) x := by
+          calc 0 < c i * EReal.indicator (E i) x := h_term_pos
+            _ ≤ ∑ j : Fin k, c j * EReal.indicator (E j) x :=
+                Finset.single_le_sum (fun j _ => h_sum_nonneg j) (Finset.mem_univ i)
+        exact ne_of_gt h_sum_pos
+      · -- hi : x ∈ ∅, contradiction
+        exact absurd hi (Set.notMem_empty x)
+  rw [h_eq]
+  exact LebesgueMeasurable.finite_union hE'_meas
 
 lemma AlmostAlways.ofAlways {d:ℕ} {P: EuclideanSpace' d → Prop} (h: ∀ x, P x) : AlmostAlways P := by
-  sorry
+  -- AlmostAlways P means IsNull { x | ¬ P x }, i.e., Lebesgue_outer_measure { x | ¬ P x } = 0
+  -- If ∀ x, P x, then { x | ¬ P x } = ∅
+  unfold AlmostAlways IsNull
+  have h_empty : { x | ¬ P x } = ∅ := by
+    ext x
+    simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_not]
+    exact h x
+  rw [h_empty]
+  exact Lebesgue_outer_measure.of_empty d
 
 lemma AlmostAlways.mp {d:ℕ} {P Q: EuclideanSpace' d → Prop} (hP: AlmostAlways P) (himp: ∀ x, P x → Q x) : AlmostAlways Q := by
-  sorry
+  -- AlmostAlways P means IsNull { x | ¬ P x }, i.e., Lebesgue_outer_measure { x | ¬ P x } = 0
+  -- If P → Q everywhere, then ¬Q → ¬P (contrapositive), so { x | ¬ Q x } ⊆ { x | ¬ P x }
+  unfold AlmostAlways IsNull at *
+  -- hP : Lebesgue_outer_measure { x | ¬ P x } = 0
+  -- Goal: Lebesgue_outer_measure { x | ¬ Q x } = 0
+  have h_subset : { x | ¬ Q x } ⊆ { x | ¬ P x } := by
+    intro x hx
+    simp only [Set.mem_setOf_eq] at *
+    exact fun hp => hx (himp x hp)
+  -- By monotonicity: measure { x | ¬ Q x } ≤ measure { x | ¬ P x } = 0
+  have h_le := Lebesgue_outer_measure.mono h_subset
+  rw [hP] at h_le
+  exact le_antisymm h_le (Lebesgue_outer_measure.nonneg _)
 
 lemma AlmostAlways.countable {d:ℕ} {I: Type*} [Countable I] {P: I → EuclideanSpace' d → Prop} (hP: ∀ i, AlmostAlways (P i)) : AlmostAlways (fun x ↦ ∀ i, P i x) := by
-  sorry
-
--- TODO: AlmostEverywhereEqual is an Equiv
+  -- AlmostAlways (fun x ↦ ∀ i, P i x) means IsNull { x | ¬ ∀ i, P i x }
+  -- { x | ¬ ∀ i, P i x } = { x | ∃ i, ¬ P i x } = ⋃ᵢ { x | ¬ P i x }
+  -- Each { x | ¬ P i x } is null by hP, and a countable union of null sets is null
+  unfold AlmostAlways IsNull at *
+  -- Goal: Lebesgue_outer_measure { x | ¬ ∀ i, P i x } = 0
+  -- hP i : Lebesgue_outer_measure { x | ¬ P i x } = 0
+  have h_eq : { x | ¬ ∀ i, P i x } = ⋃ i, { x | ¬ P i x } := by
+    ext x
+    simp only [Set.mem_setOf_eq, Set.mem_iUnion, not_forall]
+  rw [h_eq]
+  -- Need: Lebesgue_outer_measure (⋃ i, { x | ¬ P i x }) = 0
+  -- Use countable type I via Encodable
+  cases nonempty_encodable I with
+  | intro enc =>
+    -- Now have Encodable I, can use ℕ-indexed union
+    -- Reindex via Encodable.encode
+    let E' : ℕ → Set (EuclideanSpace' d) := fun n => match @Encodable.decode I enc n with
+      | some i => { x | ¬ P i x }
+      | none => ∅
+    have h_subset : (⋃ i : I, { x | ¬ P i x }) ⊆ ⋃ n : ℕ, E' n := by
+      intro x hx
+      simp only [Set.mem_iUnion] at hx ⊢
+      obtain ⟨i, hi⟩ := hx
+      use @Encodable.encode I enc i
+      simp only [E', @Encodable.encodek I enc]
+      exact hi
+    have h_le := Lebesgue_outer_measure.mono h_subset
+    have h_E'_null : ∀ n, Lebesgue_outer_measure (E' n) = 0 := fun n => by
+      simp only [E']
+      cases h : @Encodable.decode I enc n with
+      | none => exact Lebesgue_outer_measure.of_empty d
+      | some i => exact hP i
+    -- By countable subadditivity: m(⋃ E'_n) ≤ ∑' n, m(E'_n) = ∑' n, 0 = 0
+    have h_sum_zero : ∑' n, Lebesgue_outer_measure (E' n) = 0 := by
+      simp only [h_E'_null, tsum_zero]
+    have h_union_le := Lebesgue_outer_measure.union_le E'
+    have h_bound : Lebesgue_outer_measure (⋃ i : I, { x | ¬ P i x }) ≤ 0 :=
+      calc Lebesgue_outer_measure (⋃ i : I, { x | ¬ P i x })
+          ≤ Lebesgue_outer_measure (⋃ n, E' n) := h_le
+        _ ≤ ∑' n, Lebesgue_outer_measure (E' n) := h_union_le
+        _ = 0 := h_sum_zero
+    exact le_antisymm h_bound (Lebesgue_outer_measure.nonneg _)
+
+/-- Almost everywhere equality is reflexive -/
+lemma AlmostEverywhereEqual.refl {d:ℕ} {X: Type*} (f: EuclideanSpace' d → X) :
+    AlmostEverywhereEqual f f :=
+  -- {x | f x ≠ f x} = ∅, which is null
+  AlmostAlways.ofAlways (fun _ => rfl)
+
+/-- Almost everywhere equality is symmetric -/
+lemma AlmostEverywhereEqual.symm {d:ℕ} {X: Type*} {f g: EuclideanSpace' d → X}
+    (h: AlmostEverywhereEqual f g) : AlmostEverywhereEqual g f := by
+  -- {x | g x ≠ f x} = {x | f x ≠ g x}, same set
+  unfold AlmostEverywhereEqual AlmostAlways IsNull at *
+  convert h using 2
+  ext x
+  exact ne_comm
+
+/-- Almost everywhere equality is transitive -/
+lemma AlmostEverywhereEqual.trans {d:ℕ} {X: Type*} {f g h: EuclideanSpace' d → X}
+    (hfg: AlmostEverywhereEqual f g) (hgh: AlmostEverywhereEqual g h) :
+    AlmostEverywhereEqual f h := by
+  -- {x | f x ≠ h x} ⊆ {x | f x ≠ g x} ∪ {x | g x ≠ h x}
+  -- Union of two null sets is null
+  unfold AlmostEverywhereEqual AlmostAlways IsNull at *
+  have h_subset : {x | f x ≠ h x} ⊆ {x | f x ≠ g x} ∪ {x | g x ≠ h x} := by
+    intro x hx
+    simp only [Set.mem_setOf_eq, Set.mem_union] at *
+    by_contra hc
+    push_neg at hc
+    exact hx (hc.1.trans hc.2)
+  -- Express union as ℕ-indexed union for countable subadditivity
+  let E : ℕ → Set (EuclideanSpace' d) := fun n =>
+    match n with
+    | 0 => {x | f x ≠ g x}
+    | 1 => {x | g x ≠ h x}
+    | _ => ∅
+  have h_union_eq : {x | f x ≠ g x} ∪ {x | g x ≠ h x} = ⋃ n, E n := by
+    ext x
+    simp only [Set.mem_union, Set.mem_iUnion, E]
+    constructor
+    · intro hx
+      cases hx with
+      | inl hl => exact ⟨0, hl⟩
+      | inr hr => exact ⟨1, hr⟩
+    · intro ⟨n, hn⟩
+      match n with
+      | 0 => exact Or.inl hn
+      | 1 => exact Or.inr hn
+      | n + 2 => exact absurd hn (Set.notMem_empty x)
+  have h_E_null : ∀ n, Lebesgue_outer_measure (E n) = 0 := fun n => by
+    match n with
+    | 0 => exact hfg
+    | 1 => exact hgh
+    | n + 2 => exact Lebesgue_outer_measure.of_empty d
+  have h_sum_zero : ∑' n, Lebesgue_outer_measure (E n) = 0 := by simp only [h_E_null, tsum_zero]
+  have h_union_le := Lebesgue_outer_measure.union_le E
+  have h_bound : Lebesgue_outer_measure {x | f x ≠ h x} ≤ 0 :=
+    calc Lebesgue_outer_measure {x | f x ≠ h x}
+        ≤ Lebesgue_outer_measure (⋃ n, E n) := by rw [← h_union_eq]; exact Lebesgue_outer_measure.mono h_subset
+      _ ≤ ∑' n, Lebesgue_outer_measure (E n) := h_union_le
+      _ = 0 := h_sum_zero
+  exact le_antisymm h_bound (Lebesgue_outer_measure.nonneg _)
+
+/-- Almost everywhere equality is an equivalence relation -/
+theorem AlmostEverywhereEqual.equivalence {d:ℕ} {X: Type*} :
+    Equivalence (@AlmostEverywhereEqual d X) :=
+  ⟨refl, symm, trans⟩
 
 /-- Exercise 1.3.1 (i) (Unsigned linearity) -/
 lemma UnsignedSimpleFunction.integral_add {d:ℕ} {f g: EuclideanSpace' d → EReal} (hf: UnsignedSimpleFunction f) (hg: UnsignedSimpleFunction g) :
@@ -810,15 +1076,170 @@ def RealSimpleFunction.AbsolutelyIntegrable {d:ℕ} {f: EuclideanSpace' d → 
 def ComplexSimpleFunction.AbsolutelyIntegrable {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : Prop :=
   (hf.abs).integ < ⊤
 
-def RealSimpleFunction.pos {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : UnsignedSimpleFunction (EReal.pos_fun f) := by sorry
+/-! ### Disjoint representation for RealSimpleFunction
+
+Measure-theory specific lemmas for the disjoint representation of simple functions. -/
+
+namespace RealSimpleFunction.DisjointRepr
+
+open UnsignedSimpleFunction.IntegralWellDef
+
+/-- Single atoms are measurable -/
+lemma singleAtom_measurable {d k : ℕ} {E : Fin k → Set (EuclideanSpace' d)}
+    (hE : ∀ i, LebesgueMeasurable (E i)) (n : Fin (2^k)) :
+    LebesgueMeasurable (singleAtom E n) := by
+  simp only [singleAtom]
+  exact atom_measurable hE (fun i => Fin.elim0 i) ⟨n.val, by simp only [add_zero]; exact n.isLt⟩
+
+/-- On a point in singleAtom n, the original sum equals atomValue n -/
+lemma sum_indicator_eq_atomValue {d k : ℕ} (c : Fin k → ℝ) (E : Fin k → Set (EuclideanSpace' d))
+    (n : Fin (2^k)) (x : EuclideanSpace' d) (hx : x ∈ singleAtom E n) :
+    (∑ i : Fin k, (c i) * (E i).indicator' x) = atomValue c n := by
+  simp only [atomValue]
+  apply Finset.sum_congr rfl
+  intro i _
+  rw [mem_singleAtom_iff] at hx
+  by_cases hbit : (n.val.testBit i.val) = true
+  · simp only [hbit, ↓reduceIte]
+    have hx_in : x ∈ E i := (hx i).mp hbit
+    simp only [Set.indicator'_of_mem hx_in, mul_one]
+  · have hbit_false : (n.val.testBit i.val) = false := Bool.eq_false_iff.mpr hbit
+    have hx_out : x ∉ E i := fun h => hbit ((hx i).mpr h)
+    simp only [Set.indicator'_of_notMem hx_out, mul_zero, hbit_false, Bool.false_eq_true,
+      ↓reduceIte]
+
+/-- The original function equals the sum over atoms with atomValue coefficients -/
+lemma eq_sum_atomValue_indicator {d k : ℕ} (c : Fin k → ℝ) (E : Fin k → Set (EuclideanSpace' d)) :
+    (∑ i : Fin k, (c i) • (E i).indicator') = ∑ n : Fin (2^k), (atomValue c n) • (singleAtom E n).indicator' := by
+  classical
+  ext x
+  simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+  have ⟨n, hn_mem, hn_unique⟩ := exists_unique_singleAtom E x
+  have hrhs : (∑ m : Fin (2^k), atomValue c m * (singleAtom E m).indicator' x) = atomValue c n := by
+    rw [Finset.sum_eq_single n]
+    · simp only [Set.indicator'_of_mem hn_mem, mul_one]
+    · intro m _ hm_ne
+      have hx_notin : x ∉ singleAtom E m := fun h => hm_ne (hn_unique m h)
+      simp only [Set.indicator'_of_notMem hx_notin, mul_zero]
+    · intro h; exact absurd (Finset.mem_univ n) h
+  rw [hrhs]
+  exact sum_indicator_eq_atomValue c E n x hn_mem
+
+end RealSimpleFunction.DisjointRepr
+
+/-- Disjoint representation: any RealSimpleFunction has an equivalent representation
+    with pairwise disjoint, measurable sets. -/
+lemma RealSimpleFunction.disjoint_representation {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) :
+    ∃ (n:ℕ) (v: Fin n → ℝ) (A: Fin n → Set (EuclideanSpace' d)),
+      (∀ i, LebesgueMeasurable (A i)) ∧
+      Set.univ.PairwiseDisjoint A ∧
+      f = ∑ i, (v i) • (A i).indicator' := by
+  open UnsignedSimpleFunction.IntegralWellDef in
+  obtain ⟨k, c, E, hmes, heq⟩ := hf
+  use 2^k, UnsignedSimpleFunction.IntegralWellDef.atomValue c,
+      UnsignedSimpleFunction.IntegralWellDef.singleAtom E
+  refine ⟨?_, ?_, ?_⟩
+  · exact fun i => DisjointRepr.singleAtom_measurable hmes i
+  · exact UnsignedSimpleFunction.IntegralWellDef.singleAtom_pairwiseDisjoint E
+  · rw [heq]
+    exact DisjointRepr.eq_sum_atomValue_indicator c E
 
-def RealSimpleFunction.neg {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : UnsignedSimpleFunction (EReal.neg_fun f) := by sorry
+def RealSimpleFunction.pos {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : UnsignedSimpleFunction (EReal.pos_fun f) := by
+  -- Use disjoint representation: f = ∑ i, v_i • A_i.indicator' with disjoint A_i
+  obtain ⟨n, v, A, hA_meas, hA_disj, heq⟩ := hf.disjoint_representation
+  -- The positive part is ∑ i, (max(v_i, 0)).toEReal • EReal.indicator(A_i)
+  use n, fun i => (max (v i) 0).toEReal, A
+  constructor
+  · intro i
+    constructor
+    · exact hA_meas i
+    · exact EReal.coe_nonneg.mpr (le_max_right (v i) 0)
+  · ext x
+    simp only [EReal.pos_fun, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+    -- Since atoms are disjoint, x is in at most one atom
+    by_cases hx_in : ∃ j, x ∈ A j
+    · -- x is in exactly one atom due to disjointness (we use exists version)
+      obtain ⟨j, hj⟩ := hx_in
+      -- The sum on both sides only has one nonzero term
+      have hlhs : f x = v j := by
+        rw [heq]
+        simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+        rw [Finset.sum_eq_single j]
+        · simp only [Set.indicator'_of_mem hj, mul_one]
+        · intro i _ hi_ne
+          have hx_notin : x ∉ A i := by
+            intro hx_in_i
+            have := hA_disj (Set.mem_univ i) (Set.mem_univ j) hi_ne
+            simp only [Function.onFun, Set.disjoint_left] at this
+            exact this hx_in_i hj
+          simp only [Set.indicator'_of_notMem hx_notin, mul_zero]
+        · intro h; exact absurd (Finset.mem_univ j) h
+      have hrhs : (∑ i : Fin n, (max (v i) 0).toEReal * EReal.indicator (A i) x) =
+                  (max (v j) 0).toEReal := by
+        rw [Finset.sum_eq_single j]
+        · simp only [EReal.indicator, Real.EReal_fun, Set.indicator'_of_mem hj, EReal.coe_one, mul_one]
+        · intro i _ hi_ne
+          have hx_notin : x ∉ A i := by
+            intro hx_in_i
+            have := hA_disj (Set.mem_univ i) (Set.mem_univ j) hi_ne
+            simp only [Function.onFun, Set.disjoint_left] at this
+            exact this hx_in_i hj
+          simp only [EReal.indicator, Real.EReal_fun, Set.indicator'_of_notMem hx_notin, EReal.coe_zero, mul_zero]
+        · intro h; exact absurd (Finset.mem_univ j) h
+      rw [hlhs, hrhs]
+    · -- x is not in any atom, so f(x) = 0
+      push_neg at hx_in
+      have hlhs : f x = 0 := by
+        rw [heq]
+        simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+        apply Finset.sum_eq_zero
+        intro i _
+        simp only [Set.indicator'_of_notMem (hx_in i), mul_zero]
+      have hrhs : (∑ i : Fin n, (max (v i) 0).toEReal * EReal.indicator (A i) x) = 0 := by
+        apply Finset.sum_eq_zero
+        intro i _
+        simp only [EReal.indicator, Real.EReal_fun, Set.indicator'_of_notMem (hx_in i), EReal.coe_zero, mul_zero]
+      rw [hlhs, hrhs]
+      simp only [max_self, EReal.coe_zero]
+
+def RealSimpleFunction.neg {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : UnsignedSimpleFunction (EReal.neg_fun f) := by
+  -- neg_fun f = pos_fun (-f), and -f = (-1) • f is a simple function
+  have h : EReal.neg_fun f = EReal.pos_fun ((-1 : ℝ) • f) := by
+    ext x; simp only [EReal.neg_fun, EReal.pos_fun, Pi.smul_apply, smul_eq_mul, neg_one_mul]
+  rw [h]
+  exact (hf.smul (-1)).pos
 
 noncomputable def RealSimpleFunction.integ {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : ℝ := (hf.pos).integ.toReal - (hf.neg).integ.toReal
 
-def ComplexSimpleFunction.re {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : RealSimpleFunction (Complex.re_fun f) := by sorry
-
-def ComplexSimpleFunction.im {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : RealSimpleFunction (Complex.im_fun f) := by sorry
+def ComplexSimpleFunction.re {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : RealSimpleFunction (Complex.re_fun f) := by
+  -- If f = ∑ i, c_i • Complex.indicator(E_i), then Re(f) = ∑ i, Re(c_i) • indicator'(E_i)
+  obtain ⟨k, c, E, hmes, heq⟩ := hf
+  use k, fun i => (c i).re, E
+  constructor
+  · exact hmes
+  · ext x
+    simp only [Complex.re_fun, heq, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+    -- Goal: (∑ i, c i * Complex.indicator (E i) x).re = ∑ i, (c i).re * (E i).indicator' x
+    rw [Complex.re_sum]
+    congr 1; ext i
+    -- Goal: (c i * Complex.indicator (E i) x).re = (c i).re * (E i).indicator' x
+    simp only [Complex.indicator, Real.complex_fun]
+    rw [Complex.re_mul_ofReal]
+
+def ComplexSimpleFunction.im {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : RealSimpleFunction (Complex.im_fun f) := by
+  -- If f = ∑ i, c_i • Complex.indicator(E_i), then Im(f) = ∑ i, Im(c_i) • indicator'(E_i)
+  obtain ⟨k, c, E, hmes, heq⟩ := hf
+  use k, fun i => (c i).im, E
+  constructor
+  · exact hmes
+  · ext x
+    simp only [Complex.im_fun, heq, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+    -- Goal: (∑ i, c i * Complex.indicator (E i) x).im = ∑ i, (c i).im * (E i).indicator' x
+    rw [Complex.im_sum]
+    congr 1; ext i
+    -- Goal: (c i * Complex.indicator (E i) x).im = (c i).im * (E i).indicator' x
+    simp only [Complex.indicator, Real.complex_fun]
+    rw [Complex.im_mul_ofReal]
 
 noncomputable def ComplexSimpleFunction.integ {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : ℂ :=
   hf.re.integ + Complex.I * hf.im.integ
diff --git a/analysis/Analysis/MeasureTheory/Section_1_3_2.lean b/analysis/Analysis/MeasureTheory/Section_1_3_2.lean
index 8cfb0b0e..bf5a18de 100644
--- a/analysis/Analysis/MeasureTheory/Section_1_3_2.lean
+++ b/analysis/Analysis/MeasureTheory/Section_1_3_2.lean
@@ -20,6 +20,331 @@ def FiniteMeasureSupport {d:ℕ} {Y:Type*} [Zero Y] (f: EuclideanSpace' d → Y)
 
 def PointwiseAeConvergesTo {d:ℕ} {Y:Type*} [TopologicalSpace Y] (f: ℕ → (EuclideanSpace' d → Y)) (g: EuclideanSpace' d → Y) : Prop := AlmostAlways (fun x ↦ Filter.atTop.Tendsto (fun n ↦ f n x) (nhds (g x)))
 
+/-!
+## Helper lemmas for Lemma 1.3.9
+
+The proof follows the book's implication chain. We establish explicit edges and
+let `tfae_finish` compute the transitive closure.
+
+**Explicit edges declared:**
+- (i) ⟺ (ii): by definition of UnsignedMeasurable
+- (ii) ⟹ (iii): pointwise everywhere implies pointwise a.e.
+- (iv) ⟹ (ii): monotone sequences in [0,∞] converge to their supremum
+- (iii) ⟹ (v): via limsup representation (main technical work)
+- (v) ⟺ (vi): countable unions/intersections
+- (vi) ⟺ (vii): complementation
+- (v) ⟺ (viii): complementation
+- (v)-(viii) ⟹ (ix): intervals are intersections of half-intervals
+- (ix) ⟹ (x): open sets are countable unions of intervals
+- (x) ⟺ (xi): complementation
+- (x) ⟹ (vii): {f < λ} = f⁻¹'(Iio λ) and Iio λ is open
+- (v)-(xi) ⟹ (iv): construction of approximating sequence
+
+**Derived transitively (by tfae_finish):**
+- (ix) ⟹ (v) or (vi): via (ix) → (x) → (vii) → (vi) → (v)
+- (x) ⟹ (v)-(ix): via (x) → (vii) → (vi) → (v) → (viii)/(ix)
+-/
+
+namespace UnsignedMeasurable.TFAE_helpers
+
+variable {d : ℕ} {f : EuclideanSpace' d → EReal}
+
+-- Statement abbreviations for clarity (using indices as in the book)
+private abbrev stmt_i (f : EuclideanSpace' d → EReal) := UnsignedMeasurable f
+private abbrev stmt_ii (f : EuclideanSpace' d → EReal) :=
+  ∃ (g: ℕ → EuclideanSpace' d → EReal), (∀ n, UnsignedSimpleFunction (g n)) ∧ (∀ x, Filter.atTop.Tendsto (fun n ↦ g n x) (nhds (f x)))
+private abbrev stmt_iii (f : EuclideanSpace' d → EReal) :=
+  ∃ (g: ℕ → EuclideanSpace' d → EReal), (∀ n, UnsignedSimpleFunction (g n)) ∧ (PointwiseAeConvergesTo g f)
+private abbrev stmt_iv (f : EuclideanSpace' d → EReal) :=
+  ∃ (g: ℕ → EuclideanSpace' d → EReal), (∀ n, UnsignedSimpleFunction (g n) ∧ EReal.BoundedFunction (g n) ∧ FiniteMeasureSupport (g n)) ∧ (∀ x, Monotone (fun n ↦ g n x)) ∧ (∀ x, f x = iSup (fun n ↦ g n x))
+private abbrev stmt_v (f : EuclideanSpace' d → EReal) := ∀ t, MeasurableSet {x | f x > t}
+private abbrev stmt_vi (f : EuclideanSpace' d → EReal) := ∀ t, MeasurableSet {x | f x ≥ t}
+private abbrev stmt_vii (f : EuclideanSpace' d → EReal) := ∀ t, MeasurableSet {x | f x < t}
+private abbrev stmt_viii (f : EuclideanSpace' d → EReal) := ∀ t, MeasurableSet {x | f x ≤ t}
+private abbrev stmt_ix (f : EuclideanSpace' d → EReal) := ∀ I:BoundedInterval, MeasurableSet (f⁻¹' (Real.toEReal '' I.toSet))
+private abbrev stmt_x (f : EuclideanSpace' d → EReal) := ∀ U: Set EReal, IsOpen U → MeasurableSet (f⁻¹' U)
+private abbrev stmt_xi (f : EuclideanSpace' d → EReal) := ∀ K: Set EReal, IsClosed K → MeasurableSet (f⁻¹' K)
+
+/-! ### (i) ⟺ (ii): By definition of UnsignedMeasurable -/
+
+private lemma i_iff_ii (hf : Unsigned f) : stmt_i f ↔ stmt_ii f := by
+  simp only [UnsignedMeasurable]
+  constructor
+  · intro ⟨_, g, hg_simple, hg_conv⟩
+    exact ⟨g, hg_simple, hg_conv⟩
+  · intro ⟨g, hg_simple, hg_conv⟩
+    exact ⟨hf, g, hg_simple, hg_conv⟩
+
+/-! ### (ii) ⟹ (iii): Pointwise everywhere implies pointwise a.e. -/
+
+private lemma ii_imp_iii : stmt_ii f → stmt_iii f := by
+  intro ⟨g, hg_simple, hg_conv⟩
+  refine ⟨g, hg_simple, ?_⟩
+  -- AlmostAlways P means IsNull {x | ¬P x}
+  -- Since pointwise convergence holds everywhere, {x | ¬Tendsto} = ∅
+  simp only [PointwiseAeConvergesTo, AlmostAlways]
+  have h_empty : {x | ¬Filter.atTop.Tendsto (fun n ↦ g n x) (nhds (f x))} = ∅ := by
+    ext x
+    simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_not]
+    exact hg_conv x
+  rw [h_empty]
+  exact Lebesgue_outer_measure.of_empty d
+
+/-! ### (iv) ⟹ (ii): Monotone sequences in [0,∞] converge to their supremum -/
+
+private lemma iv_imp_ii : stmt_iv f → stmt_ii f := by
+  intro ⟨g, hg_props, hg_mono, hg_sup⟩
+  refine ⟨g, fun n => (hg_props n).1, ?_⟩
+  intro x
+  rw [hg_sup x]
+  -- For monotone sequences in EReal, g n x → iSup (g · x)
+  exact tendsto_atTop_iSup (hg_mono x)
+
+/-! ### (iii) ⟹ (v): Via limsup representation -/
+
+-- This is the main technical work of the proof
+private lemma iii_imp_v : stmt_iii f → stmt_v f := by
+  intro ⟨g, hg_simple, hg_ae_conv⟩
+  intro t
+  -- The key insight: f(x) = lim f_n(x) = lim sup f_n(x) a.e.
+  -- So {f > λ} = ⋃_{M≥1} ⋂_{N≥1} ⋃_{n≥N} {f_n > λ + 1/M} outside a null set
+  sorry
+
+/-! ### (v) ⟹ (vi): {f ≥ λ} = ⋂_{n≥1} {f > λ - 1/n} -/
+
+-- Helper: if x > n for all n ∈ ℕ, then x = ⊤
+private lemma EReal.eq_top_of_forall_nat_lt {x : EReal} (h : ∀ n : ℕ, x > n) : x = ⊤ := by
+  induction x using EReal.rec with
+  | bot =>
+    exfalso
+    have h0 : (⊥ : EReal) > (0 : ℕ) := h 0
+    simp only [Nat.cast_zero, gt_iff_lt, not_lt_bot] at h0
+  | top => rfl
+  | coe r =>
+    exfalso
+    have h1 : (r : EReal) > (⌈r⌉₊ : ℕ) := h ⌈r⌉₊
+    have h1' : r > (⌈r⌉₊ : ℕ) := by
+      simp only [gt_iff_lt] at h1 ⊢
+      rwa [show ((⌈r⌉₊ : ℕ) : EReal) = ((⌈r⌉₊ : ℕ) : ℝ) by norm_cast,
+           EReal.coe_lt_coe_iff] at h1
+    have h2 : r ≤ ⌈r⌉₊ := Nat.le_ceil r
+    linarith
+
+private lemma v_imp_vi : stmt_v f → stmt_vi f := by
+  intro hv t
+  -- Handle cases based on t
+  rcases eq_bot_or_bot_lt t with rfl | ht_bot
+  · -- t = ⊥: {f ≥ ⊥} = Set.univ
+    convert MeasurableSet.univ
+    ext x; simp
+  rcases eq_top_or_lt_top t with rfl | ht_top
+  · -- t = ⊤: {f ≥ ⊤} = {f = ⊤} = ⋂_{n ∈ ℕ} {f > n}
+    have h_eq : {x | f x ≥ ⊤} = ⋂ (n : ℕ), {x | f x > n} := by
+      ext x
+      simp only [Set.mem_setOf_eq, Set.mem_iInter, ge_iff_le, top_le_iff]
+      constructor
+      · intro hfx n
+        simp only [gt_iff_lt]
+        rw [hfx]; exact EReal.coe_lt_top n
+      · intro hfx
+        exact EReal.eq_top_of_forall_nat_lt hfx
+    rw [h_eq]
+    exact MeasurableSet.iInter (fun n => hv _)
+  · -- t is finite: use {f ≥ t} = ⋂_{n≥1} {f > t - 1/(n+1)}
+    -- Since t < ⊤ and ⊥ < t, we know t is a real number
+    induction t using EReal.rec with
+    | bot => exact (not_lt.mpr le_rfl ht_bot).elim
+    | top => exact (not_lt.mpr le_rfl ht_top).elim
+    | coe t' =>
+      -- Use {f ≥ t'} = ⋂_n {f > (t' - 1/(n+1) : ℝ)}
+      have h_eq : {x | f x ≥ (t' : EReal)} = ⋂ (n : ℕ), {x | f x > ((t' - 1 / (n + 1)) : ℝ)} := by
+        ext x
+        simp only [Set.mem_setOf_eq, Set.mem_iInter, ge_iff_le, gt_iff_lt]
+        constructor
+        · intro hfx n
+          have h1 : (0 : ℝ) < 1 / (n + 1) := by positivity
+          have h2 : (t' - 1 / (n + 1) : ℝ) < t' := by linarith
+          have h3 : ((t' - 1 / (n + 1)) : EReal) < (t' : EReal) := EReal.coe_lt_coe_iff.mpr h2
+          exact lt_of_lt_of_le h3 hfx
+        · intro hfx
+          by_contra h
+          push_neg at h
+          -- f x < t'
+          have hfx_lt_t' : f x < (t' : EReal) := h
+          -- Get a witness for f x being a real
+          have hfx_ne_bot : f x ≠ ⊥ := by
+            intro hfx_eq_bot
+            have hbot : ((t' - 1 / ((0 : ℕ) + 1)) : ℝ) < (⊥ : EReal) := by
+              simp only [Nat.cast_zero, zero_add, div_one]
+              rw [← hfx_eq_bot]
+              convert hfx 0 using 2
+              simp
+            exact not_lt_bot hbot
+          have hfx_ne_top : f x ≠ ⊤ := ne_top_of_lt hfx_lt_t'
+          -- So f x is a real
+          have hr : f x = (f x).toReal := (EReal.coe_toReal hfx_ne_top hfx_ne_bot).symm
+          set r := (f x).toReal with hr_def
+          rw [hr] at hfx_lt_t' hfx
+          have hr_lt_t' : r < t' := EReal.coe_lt_coe_iff.mp hfx_lt_t'
+          have hdiff_pos : 0 < t' - r := by linarith
+          obtain ⟨n, hn⟩ := exists_nat_gt (1 / (t' - r))
+          have h_n_pos : (0 : ℝ) < n := by
+            by_cases hn0 : n = 0
+            · subst hn0; simp at hn; linarith
+            · exact Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn0)
+          have hn' : 1 / ((n : ℝ) + 1) < t' - r := by
+            calc 1 / ((n : ℝ) + 1) < 1 / (n : ℝ) := by
+                  apply one_div_lt_one_div_of_lt h_n_pos; linarith
+              _ < 1 / (1 / (t' - r)) := by
+                  apply one_div_lt_one_div_of_lt (one_div_pos.mpr hdiff_pos) hn
+              _ = t' - r := one_div_one_div (t' - r)
+          -- So (t' - 1/(n+1) : ℝ) > r
+          have hcontra := hfx n
+          have hcontra' := EReal.coe_lt_coe_iff.mp hcontra
+          linarith
+      rw [h_eq]
+      exact MeasurableSet.iInter (fun n => hv _)
+
+/-! ### (vi) ⟹ (v): {f > λ} = ⋃_{q ∈ ℚ, q > λ} {f ≥ q} -/
+
+private lemma vi_imp_v : stmt_vi f → stmt_v f := by
+  intro hvi t
+  -- {f > t} = ⋃_{q : ℚ, q > t} {f ≥ q}
+  -- Since rationals are dense, for any x with f x > t, there exists q ∈ ℚ with t < q ≤ f x
+  have h_eq : {x | f x > t} = ⋃ (q : ℚ), if (t < ((q : ℝ) : EReal)) then {x | f x ≥ ((q : ℝ) : EReal)} else ∅ := by
+    ext x
+    simp only [Set.mem_setOf_eq, Set.mem_iUnion]
+    constructor
+    · intro hfx
+      -- f x > t, so there exists q ∈ ℚ with t < q < f x
+      obtain ⟨q, hq1, hq2⟩ := EReal.exists_rat_btwn_of_lt hfx
+      use q
+      simp only [hq1, if_true]
+      exact le_of_lt hq2
+    · intro ⟨q, hq⟩
+      by_cases h : t < ((q : ℝ) : EReal)
+      · simp only [h, if_true, Set.mem_setOf_eq] at hq
+        calc t < ((q : ℝ) : EReal) := h
+          _ ≤ f x := hq
+      · simp only [h, if_false, Set.mem_empty_iff_false] at hq
+  rw [h_eq]
+  -- This is a countable union of measurable sets
+  apply MeasurableSet.iUnion
+  intro q
+  split_ifs with h
+  · exact hvi ((q : ℝ) : EReal)
+  · exact MeasurableSet.empty
+
+/-! ### (v) ⟹ (viii): {f ≤ t} = {f > t}ᶜ -/
+
+private lemma v_imp_viii : stmt_v f → stmt_viii f := by
+  intro hv t
+  have h_eq : {x | f x ≤ t} = {x | f x > t}ᶜ := by ext x; simp [not_lt]
+  rw [h_eq]
+  exact MeasurableSet.compl (hv t)
+
+/-! ### (vi) ⟹ (vii): {f < t} = {f ≥ t}ᶜ -/
+
+private lemma vi_imp_vii : stmt_vi f → stmt_vii f := by
+  intro hvi t
+  have h_eq : {x | f x < t} = {x | f x ≥ t}ᶜ := by ext x; simp [not_le]
+  rw [h_eq]
+  exact MeasurableSet.compl (hvi t)
+
+/-! ### (vii) ⟹ (vi): {f ≥ t} = {f < t}ᶜ -/
+
+private lemma vii_imp_vi : stmt_vii f → stmt_vi f := by
+  intro hvii t
+  have h_eq : {x | f x ≥ t} = {x | f x < t}ᶜ := by ext x; simp [not_lt]
+  rw [h_eq]
+  exact MeasurableSet.compl (hvii t)
+
+/-! ### (viii) ⟹ (v): {f > t} = {f ≤ t}ᶜ -/
+
+private lemma viii_imp_v : stmt_viii f → stmt_v f := by
+  intro hviii t
+  have h_eq : {x | f x > t} = {x | f x ≤ t}ᶜ := by ext x; simp [not_le]
+  rw [h_eq]
+  exact MeasurableSet.compl (hviii t)
+
+/-! ### (v)-(viii) ⟹ (ix): Intervals are intersections of half-intervals -/
+
+private lemma v_to_viii_imp_ix (hv : stmt_v f) (hvi : stmt_vi f) (hvii : stmt_vii f) (hviii : stmt_viii f) :
+    stmt_ix f := by
+  intro I
+  cases I with
+  | Ioo a b =>
+    simp only [BoundedInterval.toSet]
+    have h_eq : f⁻¹' (Real.toEReal '' Set.Ioo a b) = {x | f x > a} ∩ {x | f x < b} := by
+      rw [EReal.image_coe_Ioo]
+      ext x
+      simp only [Set.mem_preimage, Set.mem_Ioo, Set.mem_inter_iff, Set.mem_setOf_eq, gt_iff_lt]
+    rw [h_eq]
+    exact MeasurableSet.inter (hv _) (hvii _)
+  | Icc a b =>
+    simp only [BoundedInterval.toSet]
+    have h_eq : f⁻¹' (Real.toEReal '' Set.Icc a b) = {x | f x ≥ a} ∩ {x | f x ≤ b} := by
+      rw [EReal.image_coe_Icc]
+      ext x
+      simp only [Set.mem_preimage, Set.mem_Icc, Set.mem_inter_iff, Set.mem_setOf_eq, ge_iff_le]
+    rw [h_eq]
+    exact MeasurableSet.inter (hvi _) (hviii _)
+  | Ioc a b =>
+    simp only [BoundedInterval.toSet]
+    have h_eq : f⁻¹' (Real.toEReal '' Set.Ioc a b) = {x | f x > a} ∩ {x | f x ≤ b} := by
+      rw [EReal.image_coe_Ioc]
+      ext x
+      simp only [Set.mem_preimage, Set.mem_Ioc, Set.mem_inter_iff, Set.mem_setOf_eq, gt_iff_lt]
+    rw [h_eq]
+    exact MeasurableSet.inter (hv _) (hviii _)
+  | Ico a b =>
+    simp only [BoundedInterval.toSet]
+    have h_eq : f⁻¹' (Real.toEReal '' Set.Ico a b) = {x | f x ≥ a} ∩ {x | f x < b} := by
+      rw [EReal.image_coe_Ico]
+      ext x
+      simp only [Set.mem_preimage, Set.mem_Ico, Set.mem_inter_iff, Set.mem_setOf_eq, ge_iff_le]
+    rw [h_eq]
+    exact MeasurableSet.inter (hvi _) (hvii _)
+
+/-! ### (ix) ⟹ (x): Open sets are countable unions of intervals -/
+
+private lemma ix_imp_x : stmt_ix f → stmt_x f := by
+  intro hix U hU
+  sorry -- Every open set in EReal is countable union of intervals
+
+/-! ### (x) ⟺ (xi): Complementation -/
+
+private lemma x_iff_xi : stmt_x f ↔ stmt_xi f := by
+  constructor
+  · intro hx K hK
+    have h_eq : f⁻¹' K = (f⁻¹' Kᶜ)ᶜ := by simp
+    rw [h_eq]
+    exact MeasurableSet.compl (hx _ hK.isOpen_compl)
+  · intro hxi U hU
+    have h_eq : f⁻¹' U = (f⁻¹' Uᶜ)ᶜ := by simp
+    rw [h_eq]
+    exact MeasurableSet.compl (hxi _ hU.isClosed_compl)
+
+/-! ### (x) ⟹ (vii): {f < λ} = f⁻¹'(Iio λ) and Iio λ is open -/
+
+private lemma x_imp_vii : stmt_x f → stmt_vii f := by
+  intro hx t
+  have h_open : IsOpen (Set.Iio t) := isOpen_Iio
+  have h_eq : {x | f x < t} = f⁻¹' (Set.Iio t) := rfl
+  rw [h_eq]
+  exact hx _ h_open
+
+/-! ### (v)-(xi) ⟹ (iv): Construction of approximating sequence -/
+
+private lemma v_to_xi_imp_iv (hf : Unsigned f) (hv : stmt_v f) (hvi : stmt_vi f)
+    (hvii : stmt_vii f) (hviii : stmt_viii f) (hix : stmt_ix f)
+    (hx : stmt_x f) (hxi : stmt_xi f) :
+    stmt_iv f := by
+  -- Construct f_n(x) = largest k·2^{-n} ≤ min(f(x), n) when |x| ≤ n, else 0
+  sorry
+
+end UnsignedMeasurable.TFAE_helpers
+
 /-- Lemma 1.3.9 (Equivalent notions of measurability).  Some slight changes to the statement have been made to make the claims cleaner to state -/
 theorem UnsignedMeasurable.TFAE {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: Unsigned f):
     [
@@ -34,8 +359,28 @@ theorem UnsignedMeasurable.TFAE {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: Un
       ∀ I:BoundedInterval, MeasurableSet (f⁻¹' (Real.toEReal '' I.toSet)),
       ∀ U: Set EReal, IsOpen U → MeasurableSet (f⁻¹' U),
       ∀ K: Set EReal, IsClosed K → MeasurableSet (f⁻¹' K)
-    ].TFAE
-  := by sorry
+    ].TFAE := by
+  open UnsignedMeasurable.TFAE_helpers in
+  -- Establish the implication graph
+  tfae_have 1 ↔ 2 := i_iff_ii hf
+  tfae_have 2 → 3 := ii_imp_iii
+  tfae_have 4 → 2 := iv_imp_ii
+  tfae_have 3 → 5 := iii_imp_v
+  tfae_have 5 → 6 := v_imp_vi
+  tfae_have 6 → 5 := vi_imp_v
+  tfae_have 5 → 8 := v_imp_viii
+  tfae_have 6 → 7 := vi_imp_vii
+  tfae_have 7 → 6 := vii_imp_vi
+  tfae_have 8 → 5 := viii_imp_v
+  tfae_have 5 → 9 := fun h => v_to_viii_imp_ix h (v_imp_vi h) (vi_imp_vii (v_imp_vi h)) (v_imp_viii h)
+  tfae_have 9 → 10 := ix_imp_x
+  tfae_have 10 ↔ 11 := x_iff_xi
+  tfae_have 10 → 7 := x_imp_vii
+  tfae_have 5 → 4 := fun hv => v_to_xi_imp_iv hf hv (v_imp_vi hv) (vi_imp_vii (v_imp_vi hv))
+    (v_imp_viii hv) (v_to_viii_imp_ix hv (v_imp_vi hv) (vi_imp_vii (v_imp_vi hv)) (v_imp_viii hv))
+    (ix_imp_x (v_to_viii_imp_ix hv (v_imp_vi hv) (vi_imp_vii (v_imp_vi hv)) (v_imp_viii hv)))
+    (x_iff_xi.mp (ix_imp_x (v_to_viii_imp_ix hv (v_imp_vi hv) (vi_imp_vii (v_imp_vi hv)) (v_imp_viii hv))))
+  tfae_finish
 
 /-- Exercise 1.3.3(i) -/
 theorem Continuous.UnsignedMeasurable {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: Continuous f) (hnonneg: Unsigned f): UnsignedMeasurable f := by sorry