diff --git a/analysis/Analysis/MeasureTheory/Section_1_3_5.lean b/analysis/Analysis/MeasureTheory/Section_1_3_5.lean index d75dc774..5399fed3 100644 --- a/analysis/Analysis/MeasureTheory/Section_1_3_5.lean +++ b/analysis/Analysis/MeasureTheory/Section_1_3_5.lean @@ -1,4 +1,5 @@ import Analysis.MeasureTheory.Section_1_3_4 +import Mathlib.Topology.UrysohnsLemma /-! # Introduction to Measure Theory, Section 1.3.5: Littlewood's three principles @@ -503,76 +504,199 @@ private lemma RealStepFunction.add' {d:ℕ} {f g : EuclideanSpace' d → ℝ} rw [hf_union x, hg_union x] simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, ← add_mul, ← Finset.sum_add_distrib] --- Helper: step functions are simple functions -private lemma RealStepFunction.simple {d:ℕ} {f : EuclideanSpace' d → ℝ} - (hf : RealStepFunction f) : RealSimpleFunction f := by +-- Helper: lift a real step function to a complex step function +private lemma RealStepFunction.toComplexStep {d:ℕ} {f : EuclideanSpace' d → ℝ} + (hf : RealStepFunction f) : ComplexStepFunction (Real.complex_fun f) := by obtain ⟨S, c, hf_eq⟩ := hf - set k := S.card - set e := S.equivFin - refine ⟨k, fun i => c (e.symm i), fun i => (e.symm i).val.toSet, ?_, ?_⟩ - · intro i - exact Jordan_measurable.lebesgue (IsElementary.jordanMeasurable (IsElementary.box (e.symm i).val)) - · rw [hf_eq]; ext x + refine ⟨S, fun B => ↑(c B), ?_⟩ + ext x + simp only [Real.complex_fun, Complex.indicator, hf_eq] + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [Complex.ofReal_sum] + congr 1; ext B + exact Complex.ofReal_mul (c B) ((B.val.toSet).indicator' x) + +-- Helper: complex step functions are closed under addition +private lemma ComplexStepFunction.add {d:ℕ} {f g : EuclideanSpace' d → ℂ} + (hf : ComplexStepFunction f) (hg : ComplexStepFunction g) : + ComplexStepFunction (f + g) := by + obtain ⟨S₁, c₁, hf_eq⟩ := hf + obtain ⟨S₂, c₂, hg_eq⟩ := hg + refine ⟨S₁ ∪ S₂, fun B => + (if h : B.val ∈ S₁ then c₁ ⟨B.val, h⟩ else 0) + + (if h : B.val ∈ S₂ then c₂ ⟨B.val, h⟩ else 0), ?_⟩ + -- Extend f-sum from S₁ to S₁ ∪ S₂ + have hf_union : ∀ x, (∑ B : ↥S₁, c₁ B • Complex.indicator (B.val.toSet)) x = + (∑ B : ↥(S₁ ∪ S₂), (if h : B.val ∈ S₁ then c₁ ⟨B.val, h⟩ else 0) • + Complex.indicator (B.val.toSet)) x := by + intro x + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + set ι : ↥S₁ → ↥(S₁ ∪ S₂) := fun B => ⟨B.val, Finset.mem_union_left S₂ B.prop⟩ + have hι_inj : Function.Injective ι := + fun ⟨a, _⟩ ⟨b, _⟩ h => Subtype.ext (Subtype.mk.inj h) + have h_zero : ∀ B : ↥(S₁ ∪ S₂), B ∉ Set.range ι → + (if h : B.val ∈ S₁ then c₁ ⟨B.val, h⟩ else 0) * Complex.indicator (B.val.toSet) x = 0 := by + intro ⟨B, hB⟩ hni + have : B ∉ S₁ := by intro hB₁; exact hni ⟨⟨B, hB₁⟩, Subtype.ext rfl⟩ + simp [this] + rw [← Finset.sum_filter_of_ne (fun B _ => not_imp_comm.mpr (h_zero B))] + have hfilter : Finset.univ.filter (fun B : ↥(S₁ ∪ S₂) => B ∈ Set.range ι) = + Finset.univ.image ι := by + ext ⟨B, hB⟩; simp only [Finset.mem_filter, Finset.mem_univ, true_and, + Finset.mem_image, Set.mem_range] + rw [hfilter, Finset.sum_image (fun _ _ _ _ h => hι_inj h)] + apply Finset.sum_congr rfl; intro ⟨B, hB⟩ _; simp only [ι, hB, dite_true] + -- Extend g-sum from S₂ to S₁ ∪ S₂ + have hg_union : ∀ x, (∑ B : ↥S₂, c₂ B • Complex.indicator (B.val.toSet)) x = + (∑ B : ↥(S₁ ∪ S₂), (if h : B.val ∈ S₂ then c₂ ⟨B.val, h⟩ else 0) • + Complex.indicator (B.val.toSet)) x := by + intro x simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] - exact (Equiv.sum_comp e.symm (fun B => c B * (B.val.toSet).indicator' x)).symm + set ι : ↥S₂ → ↥(S₁ ∪ S₂) := fun B => ⟨B.val, Finset.mem_union_right S₁ B.prop⟩ + have hι_inj : Function.Injective ι := + fun ⟨a, _⟩ ⟨b, _⟩ h => Subtype.ext (Subtype.mk.inj h) + have h_zero : ∀ B : ↥(S₁ ∪ S₂), B ∉ Set.range ι → + (if h : B.val ∈ S₂ then c₂ ⟨B.val, h⟩ else 0) * Complex.indicator (B.val.toSet) x = 0 := by + intro ⟨B, hB⟩ hni + have : B ∉ S₂ := by intro hB₂; exact hni ⟨⟨B, hB₂⟩, Subtype.ext rfl⟩ + simp [this] + rw [← Finset.sum_filter_of_ne (fun B _ => not_imp_comm.mpr (h_zero B))] + have hfilter : Finset.univ.filter (fun B : ↥(S₁ ∪ S₂) => B ∈ Set.range ι) = + Finset.univ.image ι := by + ext ⟨B, hB⟩; simp only [Finset.mem_filter, Finset.mem_univ, true_and, + Finset.mem_image, Set.mem_range] + rw [hfilter, Finset.sum_image (fun _ _ _ _ h => hι_inj h)] + apply Finset.sum_congr rfl; intro ⟨B, hB⟩ _; simp only [ι, hB, dite_true] + ext x + simp only [Pi.add_apply, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [hf_eq, hg_eq] + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [show (∑ B : ↥S₁, c₁ B * Complex.indicator (B.val.toSet) x) = + (∑ B : ↥S₁, c₁ B • Complex.indicator (B.val.toSet)) x from by + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]] + rw [show (∑ B : ↥S₂, c₂ B * Complex.indicator (B.val.toSet) x) = + (∑ B : ↥S₂, c₂ B • Complex.indicator (B.val.toSet)) x from by + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]] + rw [hf_union x, hg_union x] + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, ← add_mul, ← Finset.sum_add_distrib] + +-- Helper: complex step functions are closed under scalar multiplication +private lemma ComplexStepFunction.smul {d:ℕ} {f : EuclideanSpace' d → ℂ} + (hf : ComplexStepFunction f) (a : ℂ) : ComplexStepFunction (a • f) := by + obtain ⟨S, c, hf_eq⟩ := hf + exact ⟨S, fun B => a * c B, by + rw [hf_eq]; ext x + simp only [Pi.smul_apply, Finset.sum_apply, smul_eq_mul] + rw [Finset.mul_sum] + congr 1; ext B; rw [mul_assoc]⟩ + +-- Helper: the zero function is real absolutely integrable +private lemma RealAbsolutelyIntegrable.zero_fun {d:ℕ} : + RealAbsolutelyIntegrable (0 : EuclideanSpace' d → ℝ) := by + constructor + · exact ⟨fun _ => 0, fun _ => ⟨0, fun i => Fin.elim0 i, fun i => Fin.elim0 i, + fun i => Fin.elim0 i, by funext x; simp [Finset.univ_eq_empty]⟩, + fun _ => tendsto_const_nhds⟩ + · have h_zero : EReal.abs_fun (0 : EuclideanSpace' d → ℝ) = 0 := by + funext x; simp only [EReal.abs_fun, Pi.zero_apply, norm_zero]; rfl + rw [h_zero, UnsignedLebesgueIntegral] + have h_simple : UnsignedSimpleFunction (0 : EuclideanSpace' d → EReal) := by + use 0, fun i => Fin.elim0 i, fun i => Fin.elim0 i + exact ⟨fun i => Fin.elim0 i, by funext x; simp [Finset.univ_eq_empty]⟩ + rw [LowerUnsignedLebesgueIntegral.eq_simpleIntegral h_simple] + calc h_simple.integ = 0 := UnsignedSimpleFunction.integ_zero + _ < ⊤ := EReal.zero_lt_top + +-- Helper: PreL1.norm of zero ≤ any nonneg EReal value +private lemma PreL1.norm_zero_le {d:ℕ} {a : EReal} (ha : 0 ≤ a) : + PreL1.norm (0 : EuclideanSpace' d → ℝ) ≤ a := by + unfold PreL1.norm + have h_zero : EReal.abs_fun (0 : EuclideanSpace' d → ℝ) = 0 := by + funext x; simp only [EReal.abs_fun, Pi.zero_apply, norm_zero]; rfl + rw [h_zero, UnsignedLebesgueIntegral] + have h_simple : UnsignedSimpleFunction (0 : EuclideanSpace' d → EReal) := by + use 0, fun i => Fin.elim0 i, fun i => Fin.elim0 i + exact ⟨fun i => Fin.elim0 i, by funext x; simp [Finset.univ_eq_empty]⟩ + rw [LowerUnsignedLebesgueIntegral.eq_simpleIntegral h_simple, + UnsignedSimpleFunction.integ_zero] + exact ha --- Helper: absolutely integrable scalar * indicator implies finite measure -private lemma simple_abs_integrable_finite_measure {d:ℕ} +-- Helper: smul indicator is absolutely integrable when support has finite measure +private lemma RealAbsolutelyIntegrable.smul_indicator {d:ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) - {c : ℝ} (hc : c ≠ 0) - (hg_ai : RealAbsolutelyIntegrable (c • E.indicator')) : - Lebesgue_measure E < ⊤ := by - -- Step 1: EReal.abs_fun (c • E.indicator') = ‖c‖.toEReal • (Real.toEReal ∘ E.indicator') - have h_abs_eq : EReal.abs_fun (c • E.indicator') = - (‖c‖.toEReal : EReal) • (Real.toEReal ∘ E.indicator') := by - have h_eq : ∀ x, EReal.abs_fun (c • E.indicator') x = - ‖c‖.toEReal * (Real.toEReal ∘ E.indicator') x := by - intro x - simp only [EReal.abs_fun, Pi.smul_apply, smul_eq_mul, Function.comp] - by_cases hx : x ∈ E - · rw [Set.indicator'_of_mem hx, mul_one] - simp - · rw [Set.indicator'_of_notMem hx, mul_zero, norm_zero] - simp - funext x; simp only [Pi.smul_apply, smul_eq_mul]; exact h_eq x - -- Step 2: The integral of EReal.abs_fun (c • E.indicator') < ⊤ - have h_integ_lt : UnsignedLebesgueIntegral (EReal.abs_fun (c • E.indicator')) < ⊤ := hg_ai.2 - -- Step 3: Compute the integral using hom and indicator - have h_indicator_meas : UnsignedMeasurable (Real.toEReal ∘ E.indicator') := - (UnsignedSimpleFunction.indicator hE).unsignedMeasurable - have h_scale : UnsignedLebesgueIntegral ((‖c‖.toEReal : EReal) • (Real.toEReal ∘ E.indicator')) = - ‖c‖.toEReal * UnsignedLebesgueIntegral (Real.toEReal ∘ E.indicator') := by - rw [UnsignedLebesgueIntegral] - exact LowerUnsignedLebesgueIntegral.hom h_indicator_meas (norm_nonneg c) - have h_indicator_integ : UnsignedLebesgueIntegral (Real.toEReal ∘ E.indicator') = Lebesgue_measure E := by - rw [UnsignedLebesgueIntegral, - LowerUnsignedLebesgueIntegral.eq_simpleIntegral (UnsignedSimpleFunction.indicator hE), - UnsignedSimpleFunction.integral_indicator hE] - -- Step 4: Combine to get ‖c‖.toEReal * Lebesgue_measure E < ⊤ - rw [h_abs_eq, h_scale, h_indicator_integ] at h_integ_lt - -- Step 5: Since ‖c‖ > 0, deduce Lebesgue_measure E < ⊤ - have hc_pos : ‖c‖ > 0 := norm_pos_iff.mpr hc - have h_ne_top : ‖c‖.toEReal * Lebesgue_measure E ≠ ⊤ := ne_of_lt h_integ_lt - rw [EReal.mul_ne_top] at h_ne_top - have h_meas_ne_top : Lebesgue_measure E ≠ ⊤ := by - -- 4th conjunct of EReal.mul_ne_top: a ≤ 0 ∨ b ≠ ⊤ - rcases h_ne_top.2.2.2 with h | h - · exact absurd (not_le.mpr (EReal.coe_pos.mpr hc_pos)) (not_not.mpr h) - · exact h - exact lt_of_le_of_ne le_top h_meas_ne_top + (c : ℝ) (hfin : c ≠ 0 → Lebesgue_measure E < ⊤) : + RealAbsolutelyIntegrable (c • E.indicator') := by + by_cases hc : c = 0 + · simp only [hc, zero_smul]; exact RealAbsolutelyIntegrable.zero_fun + · have h_simple : RealSimpleFunction (c • E.indicator') := + ⟨1, fun _ => c, fun _ => E, fun _ => hE, by + ext x; simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Fin.sum_univ_one]⟩ + exact h_simple.absolutelyIntegrable_iff'.mp (h_simple.absolutelyIntegrable_iff.mpr (by + calc Lebesgue_measure (Support (c • E.indicator')) + ≤ Lebesgue_outer_measure E := Lebesgue_outer_measure.mono (fun x hx => by + rw [Support, Set.mem_setOf_eq, Pi.smul_apply, smul_eq_mul] at hx + by_contra h_not + exact hx (by rw [Set.indicator'_of_notMem h_not, mul_zero])) + _ < ⊤ := hfin hc)) -- Helper: PreL1.norm of scalar * indicator of symmDiff private lemma PreL1.norm_smul_indicator_symmDiff_le {d:ℕ} - {E F : Set (EuclideanSpace' d)} (c : ℝ) : + {E F : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hF : LebesgueMeasurable F) + (c : ℝ) : PreL1.norm (c • E.indicator' - c • F.indicator') ≤ ↑(|c|) * Lebesgue_outer_measure (symmDiff E F) := by - sorry + have hSD : LebesgueMeasurable (symmDiff E F) := + (hE.inter hF.complement).union (hF.inter hE.complement) + have hSD_simple := UnsignedSimpleFunction.indicator hSD + have hc_nn : (Real.toEReal |c|) ≥ 0 := by exact_mod_cast abs_nonneg c + have h_simple := hSD_simple.smul hc_nn + -- Pointwise: |c * indicator'_E(x) - c * indicator'_F(x)| = |c| * indicator'_{E△F}(x) + have h_pw : EReal.abs_fun (c • E.indicator' - c • F.indicator') = + (Real.toEReal |c|) • (Real.toEReal ∘ (symmDiff E F).indicator') := by + funext x + simp only [EReal.abs_fun, Pi.smul_apply, Pi.sub_apply, smul_eq_mul, Function.comp] + by_cases hxE : x ∈ E <;> by_cases hxF : x ∈ F <;> + simp [symmDiff_def, hxE, hxF] + -- Compute: ∫|f| = |c| • ∫indicator(E△F) = |c| * μ(E△F) + unfold PreL1.norm UnsignedLebesgueIntegral + rw [h_pw, LowerUnsignedLebesgueIntegral.eq_simpleIntegral h_simple, + UnsignedSimpleFunction.integral_smul hSD_simple hc_nn, + UnsignedSimpleFunction.integral_indicator hSD] + unfold Lebesgue_measure; exact le_refl _ --- Helper: triangle inequality for PreL1.norm (needs measurability) +-- Helper: triangle inequality for PreL1.norm private lemma PreL1.norm_sub_le_add {d:ℕ} {f g h : EuclideanSpace' d → ℝ} + (hfg_ai : RealAbsolutelyIntegrable (f - g)) + (hgh_ai : RealAbsolutelyIntegrable (g - h)) (hfg : PreL1.norm (f - g) ≤ a) (hgh : PreL1.norm (g - h) ≤ b) : PreL1.norm (f - h) ≤ a + b := by - sorry + -- Key: f - h = (f - g) + (g - h), so |f-h| ≤ |f-g| + |g-h| pointwise + have h_eq : f - h = (f - g) + (g - h) := by ext x; simp [Pi.sub_apply] + have hfh_ai : RealAbsolutelyIntegrable (f - h) := h_eq ▸ hfg_ai.add hgh_ai + have h_le : ∀ x, EReal.abs_fun (f - h) x ≤ + (EReal.abs_fun (f - g) + EReal.abs_fun (g - h)) x := fun x => by + rw [h_eq] + simp only [EReal.abs_fun, Pi.add_apply] + rw [← EReal.coe_add] + exact EReal.coe_le_coe_iff.mpr (norm_add_le ((f - g) x) ((g - h) x)) + have hfg_abs := RealAbsolutelyIntegrable.abs _ hfg_ai + have hgh_abs := RealAbsolutelyIntegrable.abs _ hgh_ai + have hfh_abs := RealAbsolutelyIntegrable.abs _ hfh_ai + -- Monotonicity: ∫|f-h| ≤ ∫(|f-g| + |g-h|) + have h_mono : UnsignedLebesgueIntegral (EReal.abs_fun (f - h)) ≤ + UnsignedLebesgueIntegral (EReal.abs_fun (f - g) + EReal.abs_fun (g - h)) := + LowerUnsignedLebesgueIntegral.mono hfh_abs.1 (hfg_abs.1.add hgh_abs.1) + (AlmostAlways.ofAlways h_le) + -- Additivity: ∫(|f-g| + |g-h|) = ∫|f-g| + ∫|g-h| + have h_add : UnsignedLebesgueIntegral (EReal.abs_fun (f - g) + EReal.abs_fun (g - h)) = + UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) + UnsignedLebesgueIntegral (EReal.abs_fun (g - h)) := + LowerUnsignedLebesgueIntegral.add hfg_abs.1 hgh_abs.1 (hfg_abs.1.add hgh_abs.1) + -- Combine + unfold PreL1.norm at hfg hgh ⊢ + calc UnsignedLebesgueIntegral (EReal.abs_fun (f - h)) + ≤ UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) + + UnsignedLebesgueIntegral (EReal.abs_fun (g - h)) := by rw [← h_add]; exact h_mono + _ ≤ a + b := add_le_add hfg hgh -- Main helper: every absolutely integrable simple function can be approximated by a step function private lemma RealSimpleFunction.approx_by_step_aux {d:ℕ} {g : EuclideanSpace' d → ℝ} @@ -583,36 +707,201 @@ private lemma RealSimpleFunction.approx_by_step_aux {d:ℕ} {g : EuclideanSpace' obtain ⟨k, c, E, hE_meas, hg_eq⟩ := hg_simple by_cases hk : k = 0 · subst hk - refine ⟨0, ?_, ?_, ?_⟩ + have hg_zero : g = 0 := by rw [hg_eq]; funext x; simp [Finset.univ_eq_empty] + refine ⟨0, ?_, RealAbsolutelyIntegrable.zero_fun, ?_⟩ · exact ⟨∅, fun x => (Finset.notMem_empty x.1 x.2).elim, by simp⟩ - · constructor - · exact ⟨fun _ => 0, fun _ => ⟨0, fun i => Fin.elim0 i, fun i => Fin.elim0 i, - fun i => Fin.elim0 i, by funext x; simp [Finset.univ_eq_empty]⟩, - fun _ => tendsto_const_nhds⟩ - · have h_zero : EReal.abs_fun (0 : EuclideanSpace' d → ℝ) = 0 := by - funext x; simp only [EReal.abs_fun, Pi.zero_apply, norm_zero]; rfl - rw [h_zero, UnsignedLebesgueIntegral] - have h_simple : UnsignedSimpleFunction (0 : EuclideanSpace' d → EReal) := by - use 0, fun i => Fin.elim0 i, fun i => Fin.elim0 i - exact ⟨fun i => Fin.elim0 i, by funext x; simp [Finset.univ_eq_empty]⟩ - rw [LowerUnsignedLebesgueIntegral.eq_simpleIntegral h_simple] - calc h_simple.integ = 0 := UnsignedSimpleFunction.integ_zero - _ < ⊤ := EReal.zero_lt_top - · have hg_zero : g = 0 := by - rw [hg_eq]; funext x; simp [Finset.univ_eq_empty] - rw [hg_zero, sub_zero] - show UnsignedLebesgueIntegral (EReal.abs_fun (0 : EuclideanSpace' d → ℝ)) ≤ (δ : EReal) - have h_zero : EReal.abs_fun (0 : EuclideanSpace' d → ℝ) = 0 := by - funext x; simp only [EReal.abs_fun, Pi.zero_apply, norm_zero]; rfl - rw [h_zero, UnsignedLebesgueIntegral] - have h_simple : UnsignedSimpleFunction (0 : EuclideanSpace' d → EReal) := by - use 0, fun i => Fin.elim0 i, fun i => Fin.elim0 i - exact ⟨fun i => Fin.elim0 i, by funext x; simp [Finset.univ_eq_empty]⟩ - rw [LowerUnsignedLebesgueIntegral.eq_simpleIntegral h_simple] - calc h_simple.integ = 0 := UnsignedSimpleFunction.integ_zero - _ = (0 : ℝ).toEReal := by simp - _ ≤ (δ : EReal) := EReal.coe_le_coe_iff.mpr (le_of_lt hδ) - · sorry + · rw [hg_zero, sub_zero] + exact PreL1.norm_zero_le (EReal.coe_nonneg.mpr (le_of_lt hδ)) + · -- Case k ≠ 0: use disjoint representation and approximate each atom + -- Step 1: Get disjoint representation of g + have hg_simple' : RealSimpleFunction g := ⟨k, c, E, hE_meas, hg_eq⟩ + obtain ⟨n, v, A, hA_meas, hA_disj, hg_eq'⟩ := hg_simple'.disjoint_representation + -- Step 2: Show Lebesgue_measure (Support g) < ⊤ + have hg_abs_int : hg_simple'.AbsolutelyIntegrable := + hg_simple'.absolutelyIntegrable_iff'.mpr hg_ai + have hg_support_fin : Lebesgue_measure (Support g) < ⊤ := + hg_simple'.absolutelyIntegrable_iff.mp hg_abs_int + -- Step 3: For each j with v j ≠ 0, A j ⊆ Support g, hence finite measure + have hA_sub_support : ∀ j, v j ≠ 0 → A j ⊆ Support g := by + intro j hvj x hx + rw [Support, Set.mem_setOf_eq, hg_eq'] + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [Finset.sum_eq_single j] + · exact mul_ne_zero hvj (Set.indicator'_of_mem hx ▸ one_ne_zero) + · intro i _ hij + rw [Set.indicator'_of_notMem] + · ring + · intro hxi + exact absurd hxi (Set.disjoint_left.mp + (hA_disj (Set.mem_univ j) (Set.mem_univ i) (Ne.symm hij)) hx) + · intro h; exact absurd (Finset.mem_univ j) h + have hA_fin : ∀ j, v j ≠ 0 → Lebesgue_measure (A j) < ⊤ := by + intro j hvj + calc Lebesgue_measure (A j) + ≤ Lebesgue_outer_measure (Support g) := Lebesgue_outer_measure.mono (hA_sub_support j hvj) + _ < ⊤ := hg_support_fin + -- Handle n = 0 separately (g = 0 in this case) + by_cases hn : n = 0 + · -- If n = 0, g = 0, so h = 0 works + have hg_zero : g = 0 := by + rw [hg_eq']; subst hn; funext x; simp [Finset.univ_eq_empty] + refine ⟨0, ?_, RealAbsolutelyIntegrable.zero_fun, ?_⟩ + · exact ⟨∅, fun x => (Finset.notMem_empty x.1 x.2).elim, by simp⟩ + · rw [hg_zero, sub_zero] + exact PreL1.norm_zero_le (EReal.coe_nonneg.mpr (le_of_lt hδ)) + -- Step 4: n ≠ 0, choose elementary approximations for each A j + · have hn_pos : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn) + -- For each j with v j ≠ 0, use TFAE to get elementary F j with small symmDiff + have hε_j : ∀ j : Fin n, 0 < δ / (↑n * (|v j| + 1)) := by + intro j; apply div_pos hδ + exact mul_pos hn_pos (by linarith [abs_nonneg (v j)]) + have hF_exists : ∀ j : Fin n, ∃ F : Set (EuclideanSpace' d), + IsElementary F ∧ + (v j ≠ 0 → Lebesgue_outer_measure (symmDiff F (A j)) ≤ + ↑(δ / (↑n * (|v j| + 1)))) := by + intro j + by_cases hvj : v j = 0 + · exact ⟨∅, IsElementary.empty d, fun h => absurd hvj h⟩ + · have h_tfae := (LebesgueMeasurable.finite_TFAE (A j)).out 0 7 + have h_approx := h_tfae.mp ⟨hA_meas j, hA_fin j hvj⟩ + obtain ⟨F, hF_elem, hF_bound⟩ := + h_approx (↑(δ / (↑n * (|v j| + 1)))) + (EReal.coe_pos.mpr (hε_j j)) + exact ⟨F, hF_elem, fun _ => hF_bound⟩ + choose F hF_elem hF_bound using hF_exists + -- Step 5: Define h = ∑ j : Fin n, v j • (F j).indicator' + set h : EuclideanSpace' d → ℝ := ∑ j : Fin n, v j • (F j).indicator' with hh_def + -- Each F j is elementary, so Lebesgue_outer_measure (F j) < ⊤ + have hF_fin : ∀ j : Fin n, Lebesgue_outer_measure (F j) < ⊤ := by + intro j + rw [Lebesgue_outer_measure.elementary (F j) (hF_elem j)] + exact EReal.coe_lt_top _ + refine ⟨h, ?_, ?_, ?_⟩ + -- Step 6: h is a step function (by Finset induction) + · rw [hh_def]; exact Finset.sum_induction _ + (fun f => RealStepFunction f) + (fun f g hf hg => RealStepFunction.add' hf hg) + ⟨∅, fun x => (Finset.notMem_empty x.1 x.2).elim, by simp⟩ + (fun j _ => RealStepFunction.smul' + (elementary_indicator_is_step (hF_elem j)) (v j)) + -- Step 7: h is absolutely integrable + · have hh_simple : RealSimpleFunction h := + ⟨n, v, fun j => F j, + fun j => Jordan_measurable.lebesgue + (IsElementary.jordanMeasurable (hF_elem j)), + by rw [hh_def]⟩ + exact hh_simple.absolutelyIntegrable_iff'.mp + ((hh_simple.absolutelyIntegrable_iff).mpr (by + have h_support_sub : Support h ⊆ ⋃ j : Fin n, F j := by + intro x hx + rw [Support, Set.mem_setOf_eq] at hx + rw [Set.mem_iUnion] + by_contra h_not; push_neg at h_not; apply hx + rw [hh_def]; simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + exact Finset.sum_eq_zero fun j _ => + by rw [Set.indicator'_of_notMem (h_not j)]; ring + calc Lebesgue_measure (Support h) + ≤ Lebesgue_outer_measure (⋃ j : Fin n, F j) := + Lebesgue_outer_measure.mono h_support_sub + _ ≤ ∑ j : Fin n, Lebesgue_outer_measure (F j) := + Lebesgue_outer_measure.finite_union_le F + _ < ⊤ := by + have : ∀ j : Fin n, Lebesgue_outer_measure (F j) = + ↑((hF_elem j).measure) := + fun j => Lebesgue_outer_measure.elementary (F j) (hF_elem j) + simp_rw [this] + rw [← EReal.coe_finset_sum + (fun j _ => IsElementary.measure_nonneg (hF_elem j))] + exact EReal.coe_lt_top _)) + -- Step 8: Bound PreL1.norm (g - h) ≤ δ via induction on Finset + · have hgh_eq : g - h = ∑ j : Fin n, (v j • (A j).indicator' - v j • (F j).indicator') := by + rw [hg_eq', hh_def, ← Finset.sum_sub_distrib] + suffices h_bound : ∀ (S : Finset (Fin n)), + RealAbsolutelyIntegrable (∑ j ∈ S, (v j • (A j).indicator' - v j • (F j).indicator')) ∧ + PreL1.norm (∑ j ∈ S, (v j • (A j).indicator' - v j • (F j).indicator')) + ≤ ∑ j ∈ S, (↑(|v j|) * Lebesgue_outer_measure (symmDiff (A j) (F j))) by + rw [hgh_eq] + have h1 := (h_bound Finset.univ).2 + calc PreL1.norm (∑ j : Fin n, (v j • (A j).indicator' - v j • (F j).indicator')) + ≤ ∑ j : Fin n, (↑(|v j|) * Lebesgue_outer_measure (symmDiff (A j) (F j))) := h1 + _ ≤ ∑ j : Fin n, (↑(δ / ↑n) : EReal) := by + apply Finset.sum_le_sum + intro j _ + by_cases hvj : v j = 0 + · simp [hvj] + exact le_of_lt (div_pos hδ hn_pos) + · have h_symmDiff := hF_bound j hvj + rw [symmDiff_comm] at h_symmDiff + calc ↑(|v j|) * Lebesgue_outer_measure (symmDiff (A j) (F j)) + ≤ ↑(|v j|) * ↑(δ / (↑n * (|v j| + 1))) := + mul_le_mul_of_nonneg_left h_symmDiff + (EReal.coe_nonneg.mpr (abs_nonneg _)) + _ = ↑(|v j| * (δ / (↑n * (|v j| + 1)))) := by + rw [← EReal.coe_mul] + _ ≤ ↑(δ / ↑n) := by + rw [EReal.coe_le_coe_iff] + have hab : 0 < |v j| + 1 := by linarith [abs_nonneg (v j)] + calc |v j| * (δ / (↑n * (|v j| + 1))) + = |v j| * δ / (↑n * (|v j| + 1)) := by ring + _ ≤ (|v j| + 1) * δ / (↑n * (|v j| + 1)) := by + apply div_le_div_of_nonneg_right + · exact mul_le_mul_of_nonneg_right (by linarith) hδ.le + · exact (mul_pos hn_pos hab).le + _ = δ / ↑n := by + rw [mul_comm (|v j| + 1) δ, mul_div_mul_right _ _ + (ne_of_gt hab)] + _ = ↑δ := by + rw [← EReal.coe_finset_sum (fun _ _ => le_of_lt (div_pos hδ hn_pos))] + congr 1 + rw [Finset.sum_const, Finset.card_fin, nsmul_eq_mul, + mul_div_cancel₀ δ (Nat.cast_ne_zero.mpr hn)] + -- Each term v j • (A j).indicator' - v j • (F j).indicator' is absolutely integrable + have hterm_ai : ∀ j : Fin n, RealAbsolutelyIntegrable + (v j • (A j).indicator' - v j • (F j).indicator') := fun j => + (RealAbsolutelyIntegrable.smul_indicator (hA_meas j) (v j) (hA_fin j)).sub + (RealAbsolutelyIntegrable.smul_indicator + (Jordan_measurable.lebesgue (IsElementary.jordanMeasurable (hF_elem j))) + (v j) (fun _ => hF_fin j)) + -- Prove the suffices: induction on S + intro S + induction S using Finset.induction with + | empty => + simp only [Finset.sum_empty] + exact ⟨RealAbsolutelyIntegrable.zero_fun, PreL1.norm_zero_le le_rfl⟩ + | @insert a S haS ih => + rw [Finset.sum_insert haS, Finset.sum_insert haS] + have h_single := PreL1.norm_smul_indicator_symmDiff_le (hA_meas a) + (Jordan_measurable.lebesgue (IsElementary.jordanMeasurable (hF_elem a))) (v a) + set f_a := v a • (A a).indicator' - v a • (F a).indicator' + set sum_S := ∑ j ∈ S, (v j • (A j).indicator' - v j • (F j).indicator') + have hfa_ai : RealAbsolutelyIntegrable f_a := hterm_ai a + have hsum_ai : RealAbsolutelyIntegrable sum_S := ih.1 + -- Triangle inequality via PreL1.norm_sub_le_add + have h_eq1 : f_a + sum_S - sum_S = f_a := by + ext x; simp [f_a, sum_S, Pi.add_apply, Pi.sub_apply] + have h_eq2 : sum_S - 0 = sum_S := by ext x; simp + have h_eq3 : f_a + sum_S - 0 = f_a + sum_S := by ext x; simp + have h_triangle : PreL1.norm (f_a + sum_S) ≤ + PreL1.norm f_a + PreL1.norm sum_S := by + have hfg : PreL1.norm ((f_a + sum_S) - sum_S) ≤ PreL1.norm f_a := by + rw [show (f_a + sum_S) - sum_S = f_a from h_eq1] + have hgh : PreL1.norm (sum_S - 0) ≤ PreL1.norm sum_S := by + rw [show sum_S - 0 = sum_S from h_eq2] + have hfg_ai' : RealAbsolutelyIntegrable ((f_a + sum_S) - sum_S) := by + rw [show (f_a + sum_S) - sum_S = f_a from h_eq1]; exact hfa_ai + have hgh_ai' : RealAbsolutelyIntegrable (sum_S - 0) := by + rw [show sum_S - 0 = sum_S from h_eq2]; exact hsum_ai + calc PreL1.norm (f_a + sum_S) + = PreL1.norm ((f_a + sum_S) - 0) := by congr 1; exact h_eq3.symm + _ ≤ PreL1.norm f_a + PreL1.norm sum_S := + PreL1.norm_sub_le_add hfg_ai' hgh_ai' hfg hgh + constructor + · exact hfa_ai.add hsum_ai + · calc PreL1.norm (f_a + sum_S) + ≤ PreL1.norm f_a + PreL1.norm sum_S := h_triangle + _ ≤ (↑(|v a|) * Lebesgue_outer_measure (symmDiff (A a) (F a))) + + (∑ j ∈ S, (↑(|v j|) * Lebesgue_outer_measure (symmDiff (A j) (F j)))) := + add_le_add h_single ih.2 theorem RealAbsolutelyIntegrable.approx_by_step {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : @@ -623,28 +912,573 @@ theorem RealAbsolutelyIntegrable.approx_by_step {d:ℕ} {f: EuclideanSpace' d obtain ⟨g₂, hg₂_step, hg₂_ai, hg₂_norm⟩ := RealSimpleFunction.approx_by_step_aux hg₁_simple hg₁_ai (ε / 2) hε2 refine ⟨g₂, hg₂_step, hg₂_ai, ?_⟩ - have h_combined := PreL1.norm_sub_le_add hg₁_norm hg₂_norm + have h_combined := PreL1.norm_sub_le_add (hf.sub hg₁_ai) (hg₁_ai.sub hg₂_ai) hg₁_norm hg₂_norm calc PreL1.norm (f - g₂) ≤ ↑(ε / 2) + ↑(ε / 2) := h_combined _ = (ε : EReal) := by rw [← EReal.coe_add]; congr 1; linarith theorem ComplexAbsolutelyIntegrable.approx_by_step {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℂ), ComplexStepFunction g ∧ ComplexAbsolutelyIntegrable g ∧ - PreL1.norm (f - g) ≤ ε := by sorry + PreL1.norm (f - g) ≤ ε := by + -- Approximate real and imaginary parts within ε/2 + have hε2 : 0 < ε / 2 := half_pos hε + obtain ⟨g_re, hg_re_step, hg_re_ai, hg_re_norm⟩ := + (ComplexAbsolutelyIntegrable.re f hf).approx_by_step (ε / 2) hε2 + obtain ⟨g_im, hg_im_step, hg_im_ai, hg_im_norm⟩ := + (ComplexAbsolutelyIntegrable.im f hf).approx_by_step (ε / 2) hε2 + -- Construct complex approximation g = ↑g_re + I • ↑g_im + set g : EuclideanSpace' d → ℂ := + Real.complex_fun g_re + Complex.I • Real.complex_fun g_im with hg_def + have hg_re_eq : Complex.re_fun g = g_re := by + ext x; simp only [Complex.re_fun, hg_def, Pi.add_apply, Pi.smul_apply, smul_eq_mul, + Real.complex_fun, Complex.add_re, Complex.ofReal_re, Complex.mul_re, + Complex.I_re, Complex.I_im, Complex.ofReal_im]; ring + have hg_im_eq : Complex.im_fun g = g_im := by + ext x; simp only [Complex.im_fun, hg_def, Pi.add_apply, Pi.smul_apply, smul_eq_mul, + Real.complex_fun, Complex.add_im, Complex.ofReal_im, Complex.mul_im, + Complex.I_re, Complex.I_im, Complex.ofReal_re]; ring + -- g is a complex step function + have hg_step : ComplexStepFunction g := + ComplexStepFunction.add + (RealStepFunction.toComplexStep hg_re_step) + (ComplexStepFunction.smul (RealStepFunction.toComplexStep hg_im_step) Complex.I) + -- g is absolutely integrable + have hg_ai : ComplexAbsolutelyIntegrable g := by + apply (ComplexAbsolutelyIntegrable.iff g).mpr + exact ⟨hg_re_eq ▸ hg_re_ai, hg_im_eq ▸ hg_im_ai⟩ + refine ⟨g, hg_step, hg_ai, ?_⟩ + -- Norm bound: PreL1.norm (f - g) ≤ ε + show UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) ≤ (ε : EReal) + have hfg_re : Complex.re_fun (f - g) = Complex.re_fun f - g_re := by + ext x; simp only [Complex.re_fun, hg_def, Pi.sub_apply, Pi.add_apply, Pi.smul_apply, + smul_eq_mul, Real.complex_fun, Complex.sub_re, Complex.add_re, Complex.ofReal_re, + Complex.mul_re, Complex.I_re, Complex.I_im, Complex.ofReal_im]; ring + have hfg_im : Complex.im_fun (f - g) = Complex.im_fun f - g_im := by + ext x; simp only [Complex.im_fun, hg_def, Pi.sub_apply, Pi.add_apply, Pi.smul_apply, + smul_eq_mul, Real.complex_fun, Complex.sub_im, Complex.add_im, Complex.ofReal_im, + Complex.mul_im, Complex.I_re, Complex.I_im, Complex.ofReal_re]; ring + have h_bound : ∀ x, EReal.abs_fun (f - g) x ≤ + (EReal.abs_fun (Complex.re_fun (f - g)) + EReal.abs_fun (Complex.im_fun (f - g))) x := + fun x => by + simp only [EReal.abs_fun, Complex.re_fun, Complex.im_fun, Pi.add_apply] + rw [← EReal.coe_add] + exact EReal.coe_le_coe_iff.mpr (by + calc ‖(f - g) x‖ ≤ |((f - g) x).re| + |((f - g) x).im| := + Complex.norm_le_abs_re_add_abs_im _ + _ = ‖((f - g) x).re‖ + ‖((f - g) x).im‖ := by rw [Real.norm_eq_abs, Real.norm_eq_abs]) + have hfg_ai := hf.sub hg_ai + have hfg_re_ai := ComplexAbsolutelyIntegrable.re (f - g) hfg_ai + have hfg_im_ai := ComplexAbsolutelyIntegrable.im (f - g) hfg_ai + have h_mono : UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) ≤ + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun (f - g)) + + EReal.abs_fun (Complex.im_fun (f - g))) := + LowerUnsignedLebesgueIntegral.mono hfg_ai.abs.1 + (hfg_re_ai.abs.1.add hfg_im_ai.abs.1) (AlmostAlways.ofAlways h_bound) + have h_add : UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun (f - g)) + + EReal.abs_fun (Complex.im_fun (f - g))) = + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun (f - g))) + + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun (f - g))) := + LowerUnsignedLebesgueIntegral.add hfg_re_ai.abs.1 hfg_im_ai.abs.1 + (hfg_re_ai.abs.1.add hfg_im_ai.abs.1) + rw [h_add] at h_mono + rw [show EReal.abs_fun (Complex.re_fun (f - g)) = + EReal.abs_fun (Complex.re_fun f - g_re) from by rw [hfg_re], + show EReal.abs_fun (Complex.im_fun (f - g)) = + EReal.abs_fun (Complex.im_fun f - g_im) from by rw [hfg_im]] at h_mono + calc UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) + ≤ UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f - g_re)) + + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun f - g_im)) := h_mono + _ ≤ (↑(ε / 2) : EReal) + (↑(ε / 2) : EReal) := add_le_add hg_re_norm hg_im_norm + _ = (ε : EReal) := by rw [← EReal.coe_add]; congr 1; linarith def CompactlySupported {X Y:Type*} [TopologicalSpace X] [Zero Y] (f: X → Y) : Prop := ∃ (K: Set X), IsCompact K ∧ ∀ x, x ∉ K → f x = 0 -/-- Theorem 1.3.20(iii) Approximation of $L^1$ functions by continuous compactly supported functions -/ -theorem ComplexAbsolutelyIntegrable.approx_by_continuous_compact {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) - (ε : ℝ) (hε : 0 < ε) : - ∃ (g : EuclideanSpace' d → ℂ), Continuous g ∧ CompactlySupported g ∧ - PreL1.norm (f - g) ≤ ε := by sorry +-- Helper: approximate a scaled box indicator by a continuous compactly supported function +private lemma Box.scaled_indicator_approx_continuous {d:ℕ} (B : Box d) (c : ℝ) (δ : ℝ) (hδ : 0 < δ) : + ∃ (g : EuclideanSpace' d → ℝ), Continuous g ∧ CompactlySupported g ∧ + RealAbsolutelyIntegrable g ∧ PreL1.norm (c • B.toSet.indicator' - g) ≤ δ := by + -- Case 1: c = 0, then g = 0 works + by_cases hc : c = 0 + · refine ⟨0, continuous_const, ⟨∅, isCompact_empty, fun x _ => rfl⟩, + RealAbsolutelyIntegrable.zero_fun, ?_⟩ + have : c • B.toSet.indicator' - (0 : EuclideanSpace' d → ℝ) = 0 := by + ext x; simp [hc] + rw [this] + exact PreL1.norm_zero_le (EReal.coe_nonneg.mpr (le_of_lt hδ)) + -- Case 2: c ≠ 0 + · -- B.toSet is elementary, hence Lebesgue measurable with finite measure + have hB_elem : IsElementary B.toSet := IsElementary.box B + have hB_meas : LebesgueMeasurable B.toSet := + Jordan_measurable.lebesgue (IsElementary.jordanMeasurable hB_elem) + have hB_fin : Lebesgue_measure B.toSet < ⊤ := by + unfold Lebesgue_measure + rw [Lebesgue_outer_measure.elementary B.toSet hB_elem] + exact EReal.coe_lt_top _ + -- Choose ε₀ = δ / (2 * |c|) > 0 + have hc_abs_pos : 0 < |c| := abs_pos.mpr hc + set ε₀ : ℝ := δ / (2 * |c|) with hε₀_def + have hε₀ : 0 < ε₀ := div_pos hδ (mul_pos two_pos hc_abs_pos) + -- Get compact K ⊆ B.toSet with measure(B.toSet \ K) ≤ ε₀ + have h_tfae_03 := (LebesgueMeasurable.finite_TFAE B.toSet).out 0 3 + obtain ⟨K, hK_compact, hK_sub, hK_bound⟩ := + h_tfae_03.mp ⟨hB_meas, hB_fin⟩ (↑ε₀) (EReal.coe_pos.mpr hε₀) + -- Get open U ⊇ B.toSet with measure(U \ B.toSet) ≤ ε₀ and finite measure + have h_tfae_01 := (LebesgueMeasurable.finite_TFAE B.toSet).out 0 1 + obtain ⟨U, hU_open, hB_sub_U, hU_fin, hU_diff_bound⟩ := + h_tfae_01.mp ⟨hB_meas, hB_fin⟩ (↑ε₀) (EReal.coe_pos.mpr hε₀) + -- K ⊆ U (since K ⊆ B.toSet ⊆ U) + have hKU : K ⊆ U := hK_sub.trans hB_sub_U + -- K and Uᶜ are disjoint + have hKU_disj : Disjoint K Uᶜ := + Set.disjoint_compl_right_iff_subset.mpr hKU + -- Apply Urysohn: get continuous φ with HasCompactSupport, φ=1 on K, φ=0 outside U + obtain ⟨φ, hφ_one, hφ_zero, hφ_cs, hφ_range⟩ := + exists_continuous_one_zero_of_isCompact hK_compact hU_open.isClosed_compl hKU_disj + -- Define g = c • φ + set g : EuclideanSpace' d → ℝ := fun x => c * φ x with hg_def + -- Set up notation for the difference + set diff : EuclideanSpace' d → ℝ := c • B.toSet.indicator' - g with hdiff_def + -- Key properties of φ + have hφ_zero' : ∀ x, x ∉ U → φ x = 0 := by + intro x hxU + have := hφ_zero (show x ∈ Uᶜ from hxU) + simp at this; exact this + -- Pointwise bound: |diff(x)| ≤ |c| and diff = 0 outside U + have hdiff_bound : ∀ x, ‖diff x‖ ≤ |c| := by + intro x + simp only [diff, hdiff_def, hg_def, Pi.sub_apply, Pi.smul_apply, smul_eq_mul] + have hφ_bdd := hφ_range x + rw [show c * B.toSet.indicator' x - c * φ x = c * (B.toSet.indicator' x - φ x) by ring] + rw [norm_mul, Real.norm_eq_abs] + apply mul_le_of_le_one_right (abs_nonneg c) + rw [Real.norm_eq_abs, abs_le] + constructor + · by_cases hxB : x ∈ B.toSet + · rw [Set.indicator'_of_mem hxB]; linarith [hφ_bdd.2] + · rw [Set.indicator'_of_notMem hxB]; linarith [hφ_bdd.2] + · by_cases hxB : x ∈ B.toSet + · rw [Set.indicator'_of_mem hxB]; linarith [hφ_bdd.1] + · rw [Set.indicator'_of_notMem hxB]; linarith [hφ_bdd.1] + have hdiff_support : ∀ x, x ∉ U → diff x = 0 := by + intro x hxU + simp only [diff, hdiff_def, hg_def, Pi.sub_apply, Pi.smul_apply, smul_eq_mul] + rw [Set.indicator'_of_notMem (fun h => hxU (hB_sub_U h)), mul_zero, + hφ_zero' x hxU, mul_zero, sub_self] + -- Measurability + have hg_meas : RealMeasurable g := + (continuous_const.mul φ.continuous).RealMeasurable + have hcB_ai : RealAbsolutelyIntegrable (c • B.toSet.indicator') := + RealAbsolutelyIntegrable.smul_indicator hB_meas c (fun _ => hB_fin) + have hdiff_meas : RealMeasurable diff := RealMeasurable.sub hcB_ai.1 hg_meas + -- Measurability of sets involved + have hBK_meas : LebesgueMeasurable (B.toSet \ K) := + hB_meas.inter (hK_compact.isClosed.measurable).complement + have hUB_meas : LebesgueMeasurable (U \ B.toSet) := + (IsOpen.measurable hU_open).inter hB_meas.complement + -- Key pointwise bound: |diff(x)| ≤ |c| * (1_{B\K}(x) + 1_{U\B}(x)) + -- Also: simpler bound |diff(x)| ≤ |c| * 1_U(x) for AI proof + have h_pw_U : ∀ x, EReal.abs_fun diff x ≤ + ((Real.toEReal |c|) • (Real.toEReal ∘ U.indicator')) x := by + intro x + simp only [EReal.abs_fun, Pi.smul_apply, smul_eq_mul, Function.comp] + by_cases hxU : x ∈ U + · rw [Set.indicator'_of_mem hxU] + have : Real.toEReal 1 = (1 : EReal) := rfl + rw [this, mul_one] + exact EReal.coe_le_coe_iff.mpr (hdiff_bound x) + · rw [hdiff_support x hxU, norm_zero, Set.indicator'_of_notMem hxU] + have : Real.toEReal 0 = (0 : EReal) := rfl + rw [this, mul_zero] + -- Tighter pointwise bound (for the norm bound) + have h_pw_tight : ∀ x, EReal.abs_fun diff x ≤ + ((Real.toEReal |c|) • ((Real.toEReal ∘ (B.toSet \ K).indicator') + + (Real.toEReal ∘ (U \ B.toSet).indicator'))) x := by + intro x + simp only [EReal.abs_fun, Pi.smul_apply, smul_eq_mul, Function.comp, Pi.add_apply] + by_cases hxK : x ∈ K + · -- On K: diff = 0 + have hdx : diff x = 0 := by + simp only [diff, hdiff_def, hg_def, Pi.sub_apply, Pi.smul_apply, smul_eq_mul] + have h1 := hφ_one hxK; simp only [Pi.one_apply] at h1 + rw [Set.indicator'_of_mem (hK_sub hxK), mul_one, h1, mul_one, sub_self] + rw [hdx, norm_zero] + apply mul_nonneg (EReal.coe_nonneg.mpr (abs_nonneg c)) + apply add_nonneg <;> exact EReal.coe_nonneg.mpr ((Set.indicator_nonneg (fun _ _ => zero_le_one) x)) + · by_cases hxB : x ∈ B.toSet + · -- On B \ K: |diff| ≤ |c|, bound by |c| * 1 + rw [Set.indicator'_of_mem (show x ∈ B.toSet \ K from ⟨hxB, hxK⟩), + Set.indicator'_of_notMem (show x ∉ U \ B.toSet from fun h => h.2 hxB)] + have h0 : Real.toEReal 0 = (0 : EReal) := rfl + have h1 : Real.toEReal 1 = (1 : EReal) := rfl + rw [h1, h0, add_zero, mul_one] + exact EReal.coe_le_coe_iff.mpr (hdiff_bound x) + · by_cases hxU : x ∈ U + · -- On U \ B: |diff| ≤ |c|, bound by |c| * 1 + rw [Set.indicator'_of_notMem (show x ∉ B.toSet \ K from fun h => hxB h.1), + Set.indicator'_of_mem (show x ∈ U \ B.toSet from ⟨hxU, hxB⟩)] + have h0 : Real.toEReal 0 = (0 : EReal) := rfl + have h1 : Real.toEReal 1 = (1 : EReal) := rfl + rw [h0, h1, zero_add, mul_one] + exact EReal.coe_le_coe_iff.mpr (hdiff_bound x) + · -- Outside U: diff = 0 + rw [hdiff_support x hxU, norm_zero] + apply mul_nonneg (EReal.coe_nonneg.mpr (abs_nonneg c)) + apply add_nonneg <;> exact EReal.coe_nonneg.mpr ((Set.indicator_nonneg (fun _ _ => zero_le_one) x)) + -- Derive AI for diff (using the U bound) + have hU_meas : LebesgueMeasurable U := IsOpen.measurable hU_open + have hU_simple := UnsignedSimpleFunction.indicator hU_meas + have hc_nn : (Real.toEReal |c|) ≥ 0 := by exact_mod_cast abs_nonneg c + have hdiff_abs_meas : UnsignedMeasurable (EReal.abs_fun diff) := by + constructor + · intro x; simp only [EReal.abs_fun]; exact EReal.coe_nonneg.mpr (norm_nonneg _) + · obtain ⟨g, hg_simple, hg_conv⟩ := hdiff_meas + exact ⟨fun n => EReal.abs_fun (g n), fun n => (hg_simple n).abs, fun x => by + simp only [EReal.abs_fun] + exact (continuous_coe_real_ereal.comp continuous_norm).continuousAt.tendsto.comp (hg_conv x)⟩ + have hdiff_ai : RealAbsolutelyIntegrable diff := by + constructor + · exact hdiff_meas + · have hbound_simple := hU_simple.smul hc_nn + have hbound_meas := UnsignedSimpleFunction.unsignedMeasurable hbound_simple + have h_mono := LowerUnsignedLebesgueIntegral.mono + hdiff_abs_meas hbound_meas + (AlmostAlways.ofAlways h_pw_U) + have h_integ : LowerUnsignedLebesgueIntegral + ((Real.toEReal |c|) • (Real.toEReal ∘ U.indicator')) = + (Real.toEReal |c|) * Lebesgue_measure U := by + rw [LowerUnsignedLebesgueIntegral.eq_simpleIntegral hbound_simple, + UnsignedSimpleFunction.integral_smul hU_simple hc_nn, + UnsignedSimpleFunction.integral_indicator hU_meas] + rw [UnsignedLebesgueIntegral] + calc LowerUnsignedLebesgueIntegral (EReal.abs_fun diff) + ≤ LowerUnsignedLebesgueIntegral + ((Real.toEReal |c|) • (Real.toEReal ∘ U.indicator')) := h_mono + _ = (Real.toEReal |c|) * Lebesgue_measure U := h_integ + _ < ⊤ := by + apply Ne.lt_top + rw [EReal.mul_ne_top] + exact ⟨Or.inl (EReal.coe_ne_bot _), + Or.inl (le_of_lt (EReal.coe_pos.mpr hc_abs_pos)), + Or.inl (EReal.coe_ne_top _), + Or.inr (ne_of_lt hU_fin)⟩ + -- g = (c • B.toSet.indicator') - diff, so g is AI + have hg_ai : RealAbsolutelyIntegrable g := by + have : g = c • B.toSet.indicator' - diff := by + ext x; simp [diff, hdiff_def, hg_def, Pi.sub_apply, Pi.smul_apply, smul_eq_mul] + rw [this] + exact hcB_ai.sub hdiff_ai + refine ⟨g, ?_, ?_, hg_ai, ?_⟩ + -- g is continuous + · exact continuous_const.mul φ.continuous + -- g is compactly supported + · refine ⟨tsupport φ, hφ_cs, fun x hx => ?_⟩ + simp only [hg_def] + have : φ x = 0 := by + by_contra h + exact hx (subset_tsupport φ (Function.mem_support.mpr h)) + rw [this, mul_zero] + -- PreL1.norm bound: PreL1.norm diff ≤ δ + · -- Use the tight pointwise bound + have hBK_simple := UnsignedSimpleFunction.indicator hBK_meas + have hUB_simple := UnsignedSimpleFunction.indicator hUB_meas + have hsum_simple : UnsignedSimpleFunction + ((Real.toEReal ∘ (B.toSet \ K).indicator') + + (Real.toEReal ∘ (U \ B.toSet).indicator')) := + UnsignedSimpleFunction.add hBK_simple hUB_simple + have hbound_simple := hsum_simple.smul hc_nn + have hbound_meas2 := UnsignedSimpleFunction.unsignedMeasurable hbound_simple + have h_mono := LowerUnsignedLebesgueIntegral.mono + hdiff_abs_meas hbound_meas2 + (AlmostAlways.ofAlways h_pw_tight) + have h_integ_bound : LowerUnsignedLebesgueIntegral + ((Real.toEReal |c|) • ((Real.toEReal ∘ (B.toSet \ K).indicator') + + (Real.toEReal ∘ (U \ B.toSet).indicator'))) = + (Real.toEReal |c|) * (Lebesgue_measure (B.toSet \ K) + + Lebesgue_measure (U \ B.toSet)) := by + rw [LowerUnsignedLebesgueIntegral.eq_simpleIntegral hbound_simple, + UnsignedSimpleFunction.integral_smul hsum_simple hc_nn] + congr 1 + rw [← LowerUnsignedLebesgueIntegral.eq_simpleIntegral hsum_simple, + LowerUnsignedLebesgueIntegral.add + (UnsignedSimpleFunction.unsignedMeasurable hBK_simple) + (UnsignedSimpleFunction.unsignedMeasurable hUB_simple) + (UnsignedSimpleFunction.unsignedMeasurable hsum_simple), + LowerUnsignedLebesgueIntegral.eq_simpleIntegral hBK_simple, + LowerUnsignedLebesgueIntegral.eq_simpleIntegral hUB_simple, + UnsignedSimpleFunction.integral_indicator hBK_meas, + UnsignedSimpleFunction.integral_indicator hUB_meas] + unfold PreL1.norm UnsignedLebesgueIntegral + calc LowerUnsignedLebesgueIntegral (EReal.abs_fun diff) + ≤ LowerUnsignedLebesgueIntegral + ((Real.toEReal |c|) • ((Real.toEReal ∘ (B.toSet \ K).indicator') + + (Real.toEReal ∘ (U \ B.toSet).indicator'))) := h_mono + _ = (Real.toEReal |c|) * (Lebesgue_measure (B.toSet \ K) + + Lebesgue_measure (U \ B.toSet)) := h_integ_bound + _ ≤ (Real.toEReal |c|) * (↑ε₀ + ↑ε₀) := by + apply mul_le_mul_of_nonneg_left _ hc_nn.le + unfold Lebesgue_measure + exact add_le_add hK_bound hU_diff_bound + _ = ↑δ := by + rw [← EReal.coe_add, ← EReal.coe_mul] + congr 1 + rw [hε₀_def] + field_simp + ring + +-- Helper: a step function can be approximated by a continuous compactly supported function +private lemma RealStepFunction.approx_by_continuous_compact_aux {d:ℕ} + {h : EuclideanSpace' d → ℝ} (hh : RealStepFunction h) (hh_ai : RealAbsolutelyIntegrable h) + (δ : ℝ) (hδ : 0 < δ) : + ∃ (g : EuclideanSpace' d → ℝ), Continuous g ∧ CompactlySupported g ∧ + RealAbsolutelyIntegrable g ∧ PreL1.norm (h - g) ≤ δ := by + obtain ⟨S, c, hh_eq⟩ := hh + -- Handle empty finset + by_cases hS : S = ∅ + · have hh_zero : h = 0 := by + subst hS; rw [hh_eq]; simp [Finset.univ_eq_empty] + refine ⟨0, continuous_const, ⟨∅, isCompact_empty, fun x _ => rfl⟩, + RealAbsolutelyIntegrable.zero_fun, ?_⟩ + rw [hh_zero, sub_zero] + exact PreL1.norm_zero_le (EReal.coe_nonneg.mpr (le_of_lt hδ)) + -- S is nonempty + · have hS_nonempty : S.Nonempty := Finset.nonempty_of_ne_empty hS + have hS_card_pos : 0 < S.card := Finset.Nonempty.card_pos hS_nonempty + have hS_card_pos_real : 0 < (S.card : ℝ) := Nat.cast_pos.mpr hS_card_pos + -- Budget per box + have hδ_per : 0 < δ / S.card := div_pos hδ hS_card_pos_real + -- For each box B ∈ S, approximate c B • B.val.toSet.indicator' by continuous g_B + have h_approx : ∀ B : S, ∃ (g_B : EuclideanSpace' d → ℝ), + Continuous g_B ∧ CompactlySupported g_B ∧ + RealAbsolutelyIntegrable g_B ∧ + PreL1.norm (c B • B.val.toSet.indicator' - g_B) ≤ δ / S.card := + fun B => Box.scaled_indicator_approx_continuous B.val (c B) (δ / S.card) hδ_per + choose g_B hg_cont hg_cs hg_ai hg_norm using h_approx + -- Define g = ∑ B ∈ S, g_B + set g : EuclideanSpace' d → ℝ := fun x => ∑ B : S, g_B B x with hg_def + -- h - g = ∑ B ∈ S, (c B • B.val.toSet.indicator' - g_B B) + have hfg_eq : h - g = fun x => ∑ B : S, (c B • B.val.toSet.indicator' - g_B B) x := by + ext x + simp only [Pi.sub_apply, hg_def, hh_eq, Finset.sum_apply, Pi.smul_apply] + rw [Finset.sum_sub_distrib] + -- Each term is AI + have hterm_ai : ∀ B : S, + RealAbsolutelyIntegrable (c B • B.val.toSet.indicator' - g_B B) := + fun B => by + have hB_meas : LebesgueMeasurable B.val.toSet := + Jordan_measurable.lebesgue (IsElementary.jordanMeasurable (IsElementary.box B.val)) + have hB_fin : Lebesgue_measure B.val.toSet < ⊤ := by + unfold Lebesgue_measure + rw [Lebesgue_outer_measure.elementary B.val.toSet (IsElementary.box B.val)] + exact EReal.coe_lt_top _ + exact (RealAbsolutelyIntegrable.smul_indicator hB_meas (c B) (fun _ => hB_fin)).sub + (hg_ai B) + refine ⟨g, ?_, ?_, ?_, ?_⟩ + -- g is continuous + · show Continuous g + apply continuous_finset_sum + intro B _ + exact hg_cont B + -- g is compactly supported + · obtain ⟨B₀, hB₀⟩ := hS_nonempty + -- Each g_B has compact support K_B + choose K hK_compact hK_support using fun B => (hg_cs B) + refine ⟨⋃ B : S, K B, ?_, ?_⟩ + · exact isCompact_iUnion (fun B => (hK_compact B)) + · intro x hx + rw [Set.mem_iUnion] at hx + push_neg at hx + simp only [hg_def] + exact Finset.sum_eq_zero (fun B _ => hK_support B x (hx B)) + -- g is AI (sum of AI functions) + · show RealAbsolutelyIntegrable g + have hg_eq_sum : g = ∑ B : S, g_B B := by + ext x; simp [hg_def] + rw [hg_eq_sum] + exact Finset.sum_induction _ RealAbsolutelyIntegrable + (fun f g hf hg => hf.add hg) RealAbsolutelyIntegrable.zero_fun + (fun B _ => hg_ai B) + -- PreL1.norm (h - g) ≤ δ + · -- Set up difference terms + set diff_term : S → (EuclideanSpace' d → ℝ) := + fun B => c B • B.val.toSet.indicator' - g_B B with hdiff_term_def + -- h - g = ∑ diff_term + have hfg_eq' : h - g = ∑ B : S, diff_term B := by + ext x + simp only [Pi.sub_apply, hh_eq, hg_def, hdiff_term_def, Finset.sum_apply, + Pi.smul_apply, Pi.sub_apply] + rw [Finset.sum_sub_distrib] + -- Prove by finset induction: AI of partial sum and norm bound + suffices h_bound : ∀ (T : Finset S), + RealAbsolutelyIntegrable (∑ B ∈ T, diff_term B) ∧ + PreL1.norm (∑ B ∈ T, diff_term B) ≤ + ∑ B ∈ T, PreL1.norm (diff_term B) by + rw [hfg_eq'] + have h1 := (h_bound Finset.univ).2 + calc PreL1.norm (∑ B : S, diff_term B) + ≤ ∑ B : S, PreL1.norm (diff_term B) := h1 + _ ≤ ∑ _B : S, (↑(δ / ↑S.card) : EReal) := + Finset.sum_le_sum (fun B _ => hg_norm B) + _ = ↑δ := by + rw [← EReal.coe_finset_sum (fun _ _ => le_of_lt hδ_per)] + congr 1 + rw [Finset.sum_const, Finset.card_univ, Fintype.card_coe, + nsmul_eq_mul, mul_div_cancel₀ δ + (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hS_card_pos))] + -- Prove the suffices by induction + intro T + induction T using Finset.induction with + | empty => + simp only [Finset.sum_empty] + exact ⟨RealAbsolutelyIntegrable.zero_fun, PreL1.norm_zero_le le_rfl⟩ + | @insert a T' haT ih => + rw [Finset.sum_insert haT, Finset.sum_insert haT] + set f_a := diff_term a + set sum_T := ∑ B ∈ T', diff_term B + have hfa_ai : RealAbsolutelyIntegrable f_a := hterm_ai a + have hsum_ai : RealAbsolutelyIntegrable sum_T := ih.1 + constructor + · exact hfa_ai.add hsum_ai + · -- Triangle inequality + have h_eq1 : (f_a + sum_T) - sum_T = f_a := by + ext x; simp [f_a, sum_T, Pi.add_apply, Pi.sub_apply] + have h_eq2 : sum_T - 0 = sum_T := by ext x; simp + have h_eq3 : (f_a + sum_T) - 0 = f_a + sum_T := by ext x; simp + have hfg_ai' : RealAbsolutelyIntegrable ((f_a + sum_T) - sum_T) := by + rw [h_eq1]; exact hfa_ai + have hgh_ai' : RealAbsolutelyIntegrable (sum_T - 0) := by + rw [h_eq2]; exact hsum_ai + have hfg : PreL1.norm ((f_a + sum_T) - sum_T) ≤ PreL1.norm f_a := by rw [h_eq1] + have hgh : PreL1.norm (sum_T - 0) ≤ PreL1.norm sum_T := by rw [h_eq2] + calc PreL1.norm (f_a + sum_T) + = PreL1.norm ((f_a + sum_T) - 0) := by congr 1; exact h_eq3.symm + _ ≤ PreL1.norm f_a + PreL1.norm sum_T := + PreL1.norm_sub_le_add hfg_ai' hgh_ai' hfg hgh + _ ≤ PreL1.norm f_a + + ∑ B ∈ T', PreL1.norm (diff_term B) := + add_le_add le_rfl ih.2 + +/-- Theorem 1.3.20(iii) Approximation of $L^1$ functions by continuous compactly supported functions -/ theorem RealAbsolutelyIntegrable.approx_by_continuous_compact {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℝ), Continuous g ∧ CompactlySupported g ∧ - PreL1.norm (f - g) ≤ ε := by sorry + PreL1.norm (f - g) ≤ ε := by + -- Step 1: approximate f by step function h + have hε2 : 0 < ε / 2 := half_pos hε + obtain ⟨h, hh_step, hh_ai, hh_norm⟩ := hf.approx_by_step (ε / 2) hε2 + -- Step 4: approximate step function h by continuous compactly supported g + obtain ⟨g, hg_cont, hg_cs, hg_ai, hg_norm⟩ := + RealStepFunction.approx_by_continuous_compact_aux hh_step hh_ai (ε / 2) hε2 + -- Step 5: combine via triangle inequality + refine ⟨g, hg_cont, hg_cs, ?_⟩ + have h_combined := PreL1.norm_sub_le_add (hf.sub hh_ai) (hh_ai.sub hg_ai) hh_norm hg_norm + calc PreL1.norm (f - g) ≤ ↑(ε / 2) + ↑(ε / 2) := h_combined + _ = (ε : EReal) := by rw [← EReal.coe_add]; congr 1; linarith + +theorem ComplexAbsolutelyIntegrable.approx_by_continuous_compact {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) + (ε : ℝ) (hε : 0 < ε) : + ∃ (g : EuclideanSpace' d → ℂ), Continuous g ∧ CompactlySupported g ∧ + PreL1.norm (f - g) ≤ ε := by + -- Approximate real and imaginary parts within ε/2 + -- Use internal aux helpers to also get RealAbsolutelyIntegrable + have hε2 : 0 < ε / 2 := half_pos hε + have hε4 : 0 < ε / 2 / 2 := half_pos hε2 + -- Real part: step function approximation then continuous approximation + obtain ⟨h_re, hh_re_step, hh_re_ai, hh_re_norm⟩ := + (ComplexAbsolutelyIntegrable.re f hf).approx_by_step (ε / 2 / 2) hε4 + obtain ⟨g_re, hg_re_cont, hg_re_cs, hg_re_ai, hg_re_norm'⟩ := + RealStepFunction.approx_by_continuous_compact_aux hh_re_step hh_re_ai (ε / 2 / 2) hε4 + have hg_re_norm : PreL1.norm (Complex.re_fun f - g_re) ≤ ↑(ε / 2) := by + have := PreL1.norm_sub_le_add ((ComplexAbsolutelyIntegrable.re f hf).sub hh_re_ai) + (hh_re_ai.sub hg_re_ai) hh_re_norm hg_re_norm' + calc PreL1.norm (Complex.re_fun f - g_re) + ≤ ↑(ε / 2 / 2) + ↑(ε / 2 / 2) := this + _ = ↑(ε / 2) := by rw [← EReal.coe_add]; congr 1; linarith + -- Imaginary part: step function approximation then continuous approximation + obtain ⟨h_im, hh_im_step, hh_im_ai, hh_im_norm⟩ := + (ComplexAbsolutelyIntegrable.im f hf).approx_by_step (ε / 2 / 2) hε4 + obtain ⟨g_im, hg_im_cont, hg_im_cs, hg_im_ai, hg_im_norm'⟩ := + RealStepFunction.approx_by_continuous_compact_aux hh_im_step hh_im_ai (ε / 2 / 2) hε4 + have hg_im_norm : PreL1.norm (Complex.im_fun f - g_im) ≤ ↑(ε / 2) := by + have := PreL1.norm_sub_le_add ((ComplexAbsolutelyIntegrable.im f hf).sub hh_im_ai) + (hh_im_ai.sub hg_im_ai) hh_im_norm hg_im_norm' + calc PreL1.norm (Complex.im_fun f - g_im) + ≤ ↑(ε / 2 / 2) + ↑(ε / 2 / 2) := this + _ = ↑(ε / 2) := by rw [← EReal.coe_add]; congr 1; linarith + -- Construct complex approximation g = ↑g_re + I • ↑g_im + set g : EuclideanSpace' d → ℂ := + Real.complex_fun g_re + Complex.I • Real.complex_fun g_im with hg_def + have hg_re_eq : Complex.re_fun g = g_re := by + ext x; simp only [Complex.re_fun, hg_def, Pi.add_apply, Pi.smul_apply, smul_eq_mul, + Real.complex_fun, Complex.add_re, Complex.ofReal_re, Complex.mul_re, + Complex.I_re, Complex.I_im, Complex.ofReal_im]; ring + have hg_im_eq : Complex.im_fun g = g_im := by + ext x; simp only [Complex.im_fun, hg_def, Pi.add_apply, Pi.smul_apply, smul_eq_mul, + Real.complex_fun, Complex.add_im, Complex.ofReal_im, Complex.mul_im, + Complex.I_re, Complex.I_im, Complex.ofReal_re]; ring + -- g is continuous + have hg_cont : Continuous g := by + apply Continuous.add + · exact Complex.continuous_ofReal.comp hg_re_cont + · exact continuous_const.mul (Complex.continuous_ofReal.comp hg_im_cont) + -- g is compactly supported + have hg_cs : CompactlySupported g := by + obtain ⟨K_re, hK_re_compact, hK_re_supp⟩ := hg_re_cs + obtain ⟨K_im, hK_im_compact, hK_im_supp⟩ := hg_im_cs + refine ⟨K_re ∪ K_im, hK_re_compact.union hK_im_compact, fun x hx => ?_⟩ + rw [Set.mem_union] at hx; push_neg at hx + simp only [hg_def, Pi.add_apply, Pi.smul_apply, smul_eq_mul, Real.complex_fun] + rw [hK_re_supp x hx.1, hK_im_supp x hx.2] + simp + -- g is absolutely integrable + have hg_ai : ComplexAbsolutelyIntegrable g := by + apply (ComplexAbsolutelyIntegrable.iff g).mpr + exact ⟨hg_re_eq ▸ hg_re_ai, hg_im_eq ▸ hg_im_ai⟩ + refine ⟨g, hg_cont, hg_cs, ?_⟩ + -- Norm bound: PreL1.norm (f - g) ≤ ε + show UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) ≤ (ε : EReal) + have hfg_re : Complex.re_fun (f - g) = Complex.re_fun f - g_re := by + ext x; simp only [Complex.re_fun, hg_def, Pi.sub_apply, Pi.add_apply, Pi.smul_apply, + smul_eq_mul, Real.complex_fun, Complex.sub_re, Complex.add_re, Complex.ofReal_re, + Complex.mul_re, Complex.I_re, Complex.I_im, Complex.ofReal_im]; ring + have hfg_im : Complex.im_fun (f - g) = Complex.im_fun f - g_im := by + ext x; simp only [Complex.im_fun, hg_def, Pi.sub_apply, Pi.add_apply, Pi.smul_apply, + smul_eq_mul, Real.complex_fun, Complex.sub_im, Complex.add_im, Complex.ofReal_im, + Complex.mul_im, Complex.I_re, Complex.I_im, Complex.ofReal_re]; ring + have h_bound : ∀ x, EReal.abs_fun (f - g) x ≤ + (EReal.abs_fun (Complex.re_fun (f - g)) + EReal.abs_fun (Complex.im_fun (f - g))) x := + fun x => by + simp only [EReal.abs_fun, Complex.re_fun, Complex.im_fun, Pi.add_apply] + rw [← EReal.coe_add] + exact EReal.coe_le_coe_iff.mpr (by + calc ‖(f - g) x‖ ≤ |((f - g) x).re| + |((f - g) x).im| := + Complex.norm_le_abs_re_add_abs_im _ + _ = ‖((f - g) x).re‖ + ‖((f - g) x).im‖ := by rw [Real.norm_eq_abs, Real.norm_eq_abs]) + have hfg_ai := hf.sub hg_ai + have hfg_re_ai := ComplexAbsolutelyIntegrable.re (f - g) hfg_ai + have hfg_im_ai := ComplexAbsolutelyIntegrable.im (f - g) hfg_ai + have h_mono : UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) ≤ + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun (f - g)) + + EReal.abs_fun (Complex.im_fun (f - g))) := + LowerUnsignedLebesgueIntegral.mono hfg_ai.abs.1 + (hfg_re_ai.abs.1.add hfg_im_ai.abs.1) (AlmostAlways.ofAlways h_bound) + have h_add : UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun (f - g)) + + EReal.abs_fun (Complex.im_fun (f - g))) = + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun (f - g))) + + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun (f - g))) := + LowerUnsignedLebesgueIntegral.add hfg_re_ai.abs.1 hfg_im_ai.abs.1 + (hfg_re_ai.abs.1.add hfg_im_ai.abs.1) + rw [h_add] at h_mono + rw [show EReal.abs_fun (Complex.re_fun (f - g)) = + EReal.abs_fun (Complex.re_fun f - g_re) from by rw [hfg_re], + show EReal.abs_fun (Complex.im_fun (f - g)) = + EReal.abs_fun (Complex.im_fun f - g_im) from by rw [hfg_im]] at h_mono + calc UnsignedLebesgueIntegral (EReal.abs_fun (f - g)) + ≤ UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f - g_re)) + + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun f - g_im)) := h_mono + _ ≤ (↑(ε / 2) : EReal) + (↑(ε / 2) : EReal) := add_le_add hg_re_norm hg_im_norm + _ = (ε : EReal) := by rw [← EReal.coe_add]; congr 1; linarith def UniformlyConvergesTo {X Y:Type*} [PseudoMetricSpace Y] (f: ℕ → X → Y) (g: X → Y) : Prop := ∀ ε>0, ∃ N, ∀ n ≥ N, ∀ x, dist (f n x) (g x) ≤ ε