Introduction to Measure Theory, Section 1.3.4: Absolute integrability

A companion to (the introduction to) Section 1.3.4 of the book "An introduction to Measure Theory".

def UnsignedAbsolutelyIntegrable {d : ℕ} (f : EuclideanSpace' d → EReal) : Prop

Definition 1.3.17

Equations

• UnsignedAbsolutelyIntegrable f = (UnsignedMeasurable f ∧ UnsignedLebesgueIntegral f < ⊤)

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

Equations

• ComplexAbsolutelyIntegrable f = (ComplexMeasurable f ∧ UnsignedLebesgueIntegral (EReal.abs_fun f) < ⊤)

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

Equations

• RealAbsolutelyIntegrable f = (RealMeasurable f ∧ UnsignedLebesgueIntegral (EReal.abs_fun f) < ⊤)

theorem ComplexAbsolutelyIntegrable.abs {d : ℕ} (f : EuclideanSpace' d → ℂ) (hf : ComplexAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.abs_fun f)

theorem RealAbsolutelyIntegrable.abs {d : ℕ} (f : EuclideanSpace' d → ℝ) (hf : RealAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.abs_fun f)

theorem RealAbsolutelyIntegrable.iff {d : ℕ} (f : EuclideanSpace' d → ℝ) : RealAbsolutelyIntegrable f ↔ ComplexAbsolutelyIntegrable fun (x : EuclideanSpace' d) => ↑(f x)

theorem ComplexAbsolutelyIntegrable.re {d : ℕ} (f : EuclideanSpace' d → ℂ) (hf : ComplexAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (Complex.re_fun f)

theorem ComplexAbsolutelyIntegrable.im {d : ℕ} (f : EuclideanSpace' d → ℂ) (hf : ComplexAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (Complex.im_fun f)

theorem ComplexAbsolutelyIntegrable.iff {d : ℕ} (f : EuclideanSpace' d → ℂ) : ComplexAbsolutelyIntegrable f ↔ RealAbsolutelyIntegrable (Complex.re_fun f) ∧ RealAbsolutelyIntegrable (Complex.im_fun f)

noncomputable def UnsignedAbsolutelyIntegrable.integ {d : ℕ} (f : EuclideanSpace' d → EReal) : UnsignedAbsolutelyIntegrable f → ℝ

Equations

• UnsignedAbsolutelyIntegrable.integ f x✝ = (UnsignedLebesgueIntegral f).toReal

noncomputable def ComplexAbsolutelyIntegrable.norm {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : ℝ

Equations

• hf.norm = UnsignedAbsolutelyIntegrable.integ (EReal.abs_fun f) ⋯

noncomputable def RealAbsolutelyIntegrable.norm {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) : ℝ

Equations

• hf.norm = UnsignedAbsolutelyIntegrable.integ (EReal.abs_fun f) ⋯

def RealMeasurable.measurable_pos {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) : UnsignedMeasurable (EReal.pos_fun f)

Equations

• ⋯ = ⋯

def RealMeasurable.measurable_neg {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) : UnsignedMeasurable (EReal.neg_fun f)

Equations

• ⋯ = ⋯

def RealAbsolutelyIntegrable.pos {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.pos_fun f)

Equations

• ⋯ = ⋯

def RealAbsolutelyIntegrable.neg {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.neg_fun f)

Equations

• ⋯ = ⋯

noncomputable def RealAbsolutelyIntegrable.integ {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) : ℝ

Equations

• hf.integ = UnsignedAbsolutelyIntegrable.integ (EReal.pos_fun f) ⋯ - UnsignedAbsolutelyIntegrable.integ (EReal.neg_fun f) ⋯

noncomputable def ComplexAbsolutelyIntegrable.integ {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : ℂ

Equations

• hf.integ = ↑⋯.integ + Complex.I * ↑⋯.integ

noncomputable def RealLebesgueIntegral {d : ℕ} (f : EuclideanSpace' d → ℝ) : ℝ

Equations

• RealLebesgueIntegral f = if hf : RealAbsolutelyIntegrable f then hf.integ else 0

noncomputable def ComplexLebesgueIntegral {d : ℕ} (f : EuclideanSpace' d → ℂ) : ℂ

Equations

• ComplexLebesgueIntegral f = if hf : ComplexAbsolutelyIntegrable f then hf.integ else 0

def RealSimpleFunction.absolutelyIntegrable_iff' {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : hf.AbsolutelyIntegrable ↔ RealAbsolutelyIntegrable f

Equations

• ⋯ = ⋯

def ComplexSimpleFunction.absolutelyIntegrable_iff' {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : hf.AbsolutelyIntegrable ↔ ComplexAbsolutelyIntegrable f

Equations

• ⋯ = ⋯

def RealSimpleFunction.AbsolutelyIntegrable.integ_eq {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) (hfi : hf.AbsolutelyIntegrable) : hf.integ = ⋯.integ

Equations

• ⋯ = ⋯

def ComplexSimpleFunction.AbsolutelyIntegrable.integ_eq {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) (hfi : hf.AbsolutelyIntegrable) : hf.integ = ⋯.integ

Equations

• ⋯ = ⋯

theorem RealAbsolutelyIntegrable.add {d : ℕ} {f g : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (hg : RealAbsolutelyIntegrable g) : RealAbsolutelyIntegrable (f + g)

theorem ComplexAbsolutelyIntegrable.add {d : ℕ} {f g : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (hg : ComplexAbsolutelyIntegrable g) : ComplexAbsolutelyIntegrable (f + g)

theorem RealAbsolutelyIntegrable.sub {d : ℕ} {f g : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (hg : RealAbsolutelyIntegrable g) : RealAbsolutelyIntegrable (f - g)

theorem ComplexAbsolutelyIntegrable.sub {d : ℕ} {f g : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (hg : ComplexAbsolutelyIntegrable g) : ComplexAbsolutelyIntegrable (f - g)

theorem RealAbsolutelyIntegrable.smul {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (c : ℝ) : RealAbsolutelyIntegrable (c • f)

theorem ComplexAbsolutelyIntegrable.smul {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (c : ℂ) : ComplexAbsolutelyIntegrable (c • f)

theorem RealAbsolutelyIntegrable.of_neg {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (-f)

theorem ComplexAbsolutelyIntegrable.of_neg {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : ComplexAbsolutelyIntegrable (-f)

theorem ComplexAbsolutelyIntegrable.conj {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : ComplexAbsolutelyIntegrable (Complex.conj_fun f)

structure PreL1 (d : ℕ) : Type

• f : EuclideanSpace' d → ℂ
• integrable : ComplexAbsolutelyIntegrable self.f

theorem PreL1.ext_iff {d : ℕ} {x y : PreL1 d} : x = y ↔ x.f = y.f

theorem PreL1.ext {d : ℕ} {x y : PreL1 d} (f : x.f = y.f) : x = y

noncomputable def PreL1.norm {d : ℕ} {X : Type u_1} [RCLike X] (f : EuclideanSpace' d → X) : EReal

Equations

• PreL1.norm f = UnsignedLebesgueIntegral (EReal.abs_fun f)

def ComplexAbsolutelyIntegrable.to_PreL1 {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : PreL1 d

Equations

• hf.to_PreL1 = { f := f, integrable := hf }

def PreL1.conj {d : ℕ} (F : PreL1 d) : PreL1 d

Equations

• F.conj = { f := Complex.conj_fun F.f, integrable := ⋯ }

instance PreL1.inst_AddZeroClass {d : ℕ} : AddZeroClass (PreL1 d)

Equations

• PreL1.inst_AddZeroClass = { zero := { f := 0, integrable := ⋯ }, add := fun (F G : PreL1 d) => { f := F.f + G.f, integrable := ⋯ }, zero_add := ⋯, add_zero := ⋯ }

instance PreL1.inst_addCommMonoid {d : ℕ} : AddCommMonoid (PreL1 d)

Equations

• One or more equations did not get rendered due to their size.

instance PreL1.inst_Neg {d : ℕ} : Neg (PreL1 d)

Equations

• PreL1.inst_Neg = { neg := fun (F : PreL1 d) => { f := -F.f, integrable := ⋯ } }

instance PreL1.inst_module {d : ℕ} : Module ℂ (PreL1 d)

Equations

• PreL1.inst_module = { smul := fun (c : ℂ) (F : PreL1 d) => { f := c • F.f, integrable := ⋯ }, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable instance PreL1.inst_seminormedAddCommGroup {d : ℕ} : SeminormedAddCommGroup (PreL1 d)

Equations

• One or more equations did not get rendered due to their size.

instance PreL1.inst_normedSpace {d : ℕ} : NormedSpace ℂ (PreL1 d)

Equations

• PreL1.inst_normedSpace = { toModule := PreL1.inst_module, norm_smul_le := ⋯ }

theorem PreL1.dist_eq {d : ℕ} (F G : PreL1 d) : dist F G = ‖F - G‖

@[reducible, inline]

noncomputable abbrev L1 (d : ℕ) : Type

Equations

• L1 d = SeparationQuotient (PreL1 d)

def PreL1.toL1 {d : ℕ} (F : PreL1 d) : L1 d

Equations

• ↑F = SeparationQuotient.mk F

instance PreL1.inst_coeL1 {d : ℕ} : Coe (PreL1 d) (L1 d)

Equations

• PreL1.inst_coeL1 = { coe := PreL1.toL1 }

def ComplexAbsolutelyIntegrable.toL1 {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : L1 d

Equations

• hf.toL1 = SeparationQuotient.mk hf.to_PreL1

theorem L1.dist_eq {d : ℕ} (f g : EuclideanSpace' d → ℂ) (hf : ComplexAbsolutelyIntegrable f) (hg : ComplexAbsolutelyIntegrable g) : dist hf.toL1 hg.toL1 = ⋯.norm

theorem L1.dist_eq_zero {d : ℕ} (f g : EuclideanSpace' d → ℂ) (hf : ComplexAbsolutelyIntegrable f) (hg : ComplexAbsolutelyIntegrable g) : dist hf.toL1 hg.toL1 = 0 ↔ AlmostEverywhereEqual f g

noncomputable def L1.integ {d : ℕ} : L1 d →ₗ[ℂ] ℂ

Exercise 1.3.19 (Integration is linear)

Equations

• L1.integ = { toFun := Quotient.lift (fun (F : PreL1 d) => ⋯.integ) ⋯, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def L1.conj {d : ℕ} : L1 d → L1 d

Equations

• L1.conj = Quotient.lift (fun (F : PreL1 d) => ↑F.conj) ⋯

theorem L1.integ_conj {d : ℕ} (F : L1 d) : integ F.conj = (starRingEnd ℂ) (integ F)

theorem RealAbsolutelyIntegrable.trans {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (a : EuclideanSpace' d) : RealAbsolutelyIntegrable fun (x : EuclideanSpace' d) => f (x + a)

Exercise 1.3.20 (Translation invariance)

theorem RealAbsolutelyIntegrable.integ_trans {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) (a : EuclideanSpace' d) : ⋯.integ = hf.integ

theorem ComplexAbsolutelyIntegrable.trans {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (a : EuclideanSpace' d) : ComplexAbsolutelyIntegrable fun (x : EuclideanSpace' d) => f (x + a)

theorem ComplexAbsolutelyIntegrable.integ_trans {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) (a : EuclideanSpace' d) : ⋯.integ = hf.integ

theorem RealAbsolutelyIntegrable.comp_linear {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) {A : EuclideanSpace' d →ₗ[ℝ] EuclideanSpace' d} (hA : LinearMap.det A ≠ 0) : RealAbsolutelyIntegrable fun (x : EuclideanSpace' d) => f (A x)

Exercise 1.3.20 (Linear change of variables)

theorem RealAbsolutelyIntegrable.integ_comp_linear {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealAbsolutelyIntegrable f) {A : EuclideanSpace' d →ₗ[ℝ] EuclideanSpace' d} (hA : LinearMap.det A ≠ 0) : ⋯.integ = |LinearMap.det A|⁻¹ * hf.integ

theorem ComplexAbsolutelyIntegrable.comp_linear {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) {A : EuclideanSpace' d →ₗ[ℝ] EuclideanSpace' d} (hA : LinearMap.det A ≠ 0) : ComplexAbsolutelyIntegrable fun (x : EuclideanSpace' d) => f (A x)

theorem ComplexAbsolutelyIntegrable.integ_comp_linear {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) {A : EuclideanSpace' d →ₗ[ℝ] EuclideanSpace' d} (hA : LinearMap.det A ≠ 0) : ⋯.integ = ↑|LinearMap.det A|⁻¹ * hf.integ

theorem RiemannIntegrableOn.realAbsolutelyIntegrable {I : BoundedInterval} {f : ℝ → ℝ} (hf : RiemannIntegrableOn f I) : RealAbsolutelyIntegrable ((fun (x : ℝ) => f x * (↑I).indicator' x) ∘ ⇑EuclideanSpace'.equiv_Real)

Exercise 1.3.20 (Compatibility with the Riemann integral)

theorem RiemannIntegral.eq_integ {I : BoundedInterval} {f : ℝ → ℝ} (hf : RiemannIntegrableOn f I) : riemannIntegral f I = ⋯.integ

theorem AbsolutelySummable.realAbsolutelyIntegrable_iff {a : ℤ → ℝ} : ∑' (n : ℤ), ↑|a n| < ⊤ ↔ RealAbsolutelyIntegrable fun (x : EuclideanSpace' 1) => a ⌊EuclideanSpace'.equiv_Real x⌋

Exercise 1.3.21 (Absolute summability is a special case of absolute integrability)

theorem AbsolutelySummable.complexAbsolutelyIntegrable_iff {a : ℤ → ℂ} : ∑' (n : ℤ), ↑‖a n‖ < ⊤ ↔ ComplexAbsolutelyIntegrable fun (x : EuclideanSpace' 1) => a ⌊EuclideanSpace'.equiv_Real x⌋

def ComplexAbsolutelyIntegrableOn {d : ℕ} (f : EuclideanSpace' d → ℂ) (E : Set (EuclideanSpace' d)) : Prop

Equations

• ComplexAbsolutelyIntegrableOn f E = ComplexAbsolutelyIntegrable (f * Complex.indicator E)

noncomputable def ComplexAbsolutelyIntegrableOn.integ {d : ℕ} {f : EuclideanSpace' d → ℂ} {E : Set (EuclideanSpace' d)} (hf : ComplexAbsolutelyIntegrableOn f E) : ℂ

Equations

• hf.integ = ComplexAbsolutelyIntegrable.integ hf

theorem ComplexAbsolutelyIntegrableOn.glue {d : ℕ} {f : EuclideanSpace' d → ℂ} {E F : Set (EuclideanSpace' d)} (hdisj : Disjoint E F) (hf : ComplexAbsolutelyIntegrableOn f (E ∪ F)) : ∃ (hE : ComplexAbsolutelyIntegrableOn f E) (hF : ComplexAbsolutelyIntegrableOn f F), hf.integ = hE.integ + hF.integ

Exercise 1.3.22

def ComplexAbsolutelyIntegrableOn.restrict {d : ℕ} {f : EuclideanSpace' d → ℂ} {E F : Set (EuclideanSpace' d)} (hf : ComplexAbsolutelyIntegrableOn f E) (hF : LebesgueMeasurable F) : ComplexAbsolutelyIntegrableOn (f * Complex.indicator F) E

Equations

• ⋯ = ⋯

def ComplexAbsolutelyIntegrableOn.mono {d : ℕ} {f : EuclideanSpace' d → ℂ} {E F : Set (EuclideanSpace' d)} (hf : ComplexAbsolutelyIntegrableOn f E) (hE : LebesgueMeasurable E) (hF : LebesgueMeasurable F) (hsub : F ⊆ E) : ComplexAbsolutelyIntegrableOn f F

Equations

• ⋯ = ⋯

theorem ComplexAbsolutelyIntegrableOn.integ_restrict {d : ℕ} {f : EuclideanSpace' d → ℂ} {E F : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hF : LebesgueMeasurable F) (hsub : F ⊆ E) (hf : ComplexAbsolutelyIntegrableOn f E) : ⋯.integ = ⋯.integ

theorem ComplexAbsolutelyIntegrable.abs_le {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexAbsolutelyIntegrable f) : ‖hf.integ‖ ≤ UnsignedAbsolutelyIntegrable.integ (EReal.abs_fun f) ⋯

Lemma 1.3.19 (Triangle inequality)