theorem RealAbsolutelyIntegrable.approx_by_simple {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℝ), RealSimpleFunction g ∧ RealAbsolutelyIntegrable g ∧ PreL1.norm (f - g) ≤ ↑ε

Theorem 1.3.20(i) Approximation of $L^1$ functions by simple functions (real case)

theorem ComplexAbsolutelyIntegrable.approx_by_simple {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℂ), ComplexSimpleFunction g ∧ ComplexAbsolutelyIntegrable g ∧ PreL1.norm (f - g) ≤ ↑ε

Theorem 1.3.20(i) Approximation of $L^1$ functions by simple functions (complex case)

def ComplexStepFunction {d : ℕ} (f : EuclideanSpace' d → ℂ) : Prop

Equations

• ComplexStepFunction f = ∃ (S : Finset (Box d)) (c : ↥S → ℂ), f = ∑ B : ↥S, c B • Complex.indicator ↑↑B

def RealStepFunction {d : ℕ} (f : EuclideanSpace' d → ℝ) : Prop

Equations

• RealStepFunction f = ∃ (S : Finset (Box d)) (c : ↥S → ℝ), f = ∑ B : ↥S, c B • (↑↑B).indicator'

theorem RealAbsolutelyIntegrable.approx_by_step {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℝ), RealStepFunction g ∧ RealAbsolutelyIntegrable g ∧ PreL1.norm (f - g) ≤ ↑ε

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) ≤ ↑ε

def CompactlySupported {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] (f : X → Y) : Prop

Equations

• CompactlySupported f = ∃ (K : Set X), IsCompact K ∧ ∀ x ∉ K, f x = 0

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) ≤ ↑ε

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) ≤ ↑ε

def UniformlyConvergesTo {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] (f : ℕ → X → Y) (g : X → Y) : Prop

Equations

• UniformlyConvergesTo f g = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (x : X), dist (f n x) (g x) ≤ ε

def UniformlyConvergesToOn {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] (f : ℕ → X → Y) (g : X → Y) (S : Set X) : Prop

Equations

• UniformlyConvergesToOn f g S = UniformlyConvergesTo (fun (n : ℕ) (x : ↑S) => f n ↑x) fun (x : ↑S) => g ↑x

def LocallyUniformlyConvergesTo {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (f : ℕ → X → Y) (g : X → Y) : Prop

Definition 1.3.21 (Locally uniform convergence)

Equations

• LocallyUniformlyConvergesTo f g = ∀ (K : Set X), Bornology.IsBounded K → UniformlyConvergesToOn f g K

theorem LocallyUniformlyConvergesTo.iff {d : ℕ} {Y : Type u_1} [PseudoMetricSpace Y] (f : ℕ → EuclideanSpace' d → Y) (g : EuclideanSpace' d → Y) : LocallyUniformlyConvergesTo f g ↔ ∀ (x₀ : EuclideanSpace' d), ∃ (U : Set (EuclideanSpace' d)), x₀ ∈ U ∧ IsOpen U ∧ UniformlyConvergesToOn f g U

Remark 1.3.22

def LocallyUniformlyConvergesToOn {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (f : ℕ → X → Y) (g : X → Y) (S : Set X) : Prop

Equations

• LocallyUniformlyConvergesToOn f g S = LocallyUniformlyConvergesTo (fun (n : ℕ) (x : ↑S) => f n ↑x) fun (x : ↑S) => g ↑x

theorem PointwiseAeConvergesTo.locallyUniformlyConverges_outside_small {d : ℕ} {f : ℕ → EuclideanSpace' d → ℂ} {g : EuclideanSpace' d → ℂ} (hf : ∀ (n : ℕ), ComplexMeasurable (f n)) (hfg : PointwiseAeConvergesTo f g) (ε : ℝ) (hε : 0 < ε) : ∃ (E : Set (EuclideanSpace' d)), LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ LocallyUniformlyConvergesToOn f g Eᶜ

Theorem 1.3.26 (Egorov's theorem).

theorem PointwiseAeConvergesTo.uniformlyConverges_outside_small {d : ℕ} {f : ℕ → EuclideanSpace' d → ℂ} {g : EuclideanSpace' d → ℂ} (hf : ∀ (n : ℕ), ComplexMeasurable (f n)) (hfg : PointwiseAeConvergesTo f g) (S : Set (EuclideanSpace' d)) (hSm : LebesgueMeasurable S) (hS : Lebesgue_measure S < ⊤) (ε : ℝ) (hε : 0 < ε) : ∃ (E : Set (EuclideanSpace' d)), LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ UniformlyConvergesToOn f g (S ∩ Eᶜ)

But uniform convergence can be recovered on a fixed set of finite measure

theorem ComplexAbsolutelyIntegrable.approx_by_continuous_outside_small {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℂ) (E : Set (EuclideanSpace' d)), ContinuousOn g Eᶜ ∧ LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ ∀ x ∉ E, g x = f x

Theorem 1.3.28 (Lusin's theorem)

def LocallyComplexAbsolutelyIntegrable {d : ℕ} (f : EuclideanSpace' d → ℂ) : Prop

Equations

• LocallyComplexAbsolutelyIntegrable f = ∀ (S : Set (EuclideanSpace' d)), LebesgueMeasurable S ∧ Bornology.IsBounded S → ComplexAbsolutelyIntegrableOn f S

theorem LocallyComplexAbsolutelyIntegrable.approx_by_continuous_outside_small {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : LocallyComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℂ) (E : Set (EuclideanSpace' d)), ContinuousOn g Eᶜ ∧ LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ ∀ x ∉ E, g x = f x

Exercise 1.3.23 (Lusin's theorem only requires local absolute integrability).

theorem ComplexMeasurable.approx_by_continuous_outside_small {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexMeasurable f) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℂ) (E : Set (EuclideanSpace' d)), ContinuousOn g Eᶜ ∧ LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ ∀ x ∉ E, g x = f x

theorem ComplexMeasurable.iff_pointwiseae_of_continuous {d : ℕ} {f : EuclideanSpace' d → ℂ} : ComplexMeasurable f ↔ ∃ (g : ℕ → EuclideanSpace' d → ℂ), (∀ (n : ℕ), Continuous (g n)) ∧ PointwiseAeConvergesTo g f

Exercise 1.3.24

theorem UnsignedMeasurable.approx_by_continuous_outside_small {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) (hfin : AlmostAlways fun (x : EuclideanSpace' d) => f x < ⊤) (ε : ℝ) (hε : 0 < ε) : ∃ (g : EuclideanSpace' d → ℝ) (E : Set (EuclideanSpace' d)), ContinuousOn g Eᶜ ∧ LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ ∀ x ∉ E, ↑(g x) = f x

Remark 1.3.29

theorem ComplexAbsolutelyIntegrable.almost_bounded_support {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (R : ℝ), PreL1.norm (f * Complex.indicator (Metric.ball 0 R)ᶜ) ≤ ↑ε

Exercise 1.3.25 (a) (Littlewood-like principle)

def BoundedOn {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] (f : X → Y) (S : Set X) : Prop

Equations

• BoundedOn f S = Bornology.IsBounded (f '' S)

theorem ComplexAbsolutelyIntegrable.almost_bounded {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : ∃ (E : Set (EuclideanSpace' d)), LebesgueMeasurable E ∧ Lebesgue_measure E ≤ ↑ε ∧ BoundedOn f Eᶜ

Exercise 1.3.25 (b) (Littlewood-like principle)