noncomputable def NonnegSimpleFunction.add {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) : NonnegSimpleFunction Ω

Pointwise sum of two non-negative simple functions on Ω.

Equations

• f.add g = ⟨fun (x : ↑Ω) => ↑f x + ↑g x, ⋯⟩

theorem lebesgueIntegralNonnegSimple_add {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) : lebesgueIntegralNonnegSimple (f.add g) = lebesgueIntegralNonnegSimple f + lebesgueIntegralNonnegSimple g

Proposition 8.1.2: for non-negative simple functions f, g : Ω → ℝ, the integral is additive: ∫_Ω (f + g) dm = ∫_Ω f dm + ∫_Ω g dm.

noncomputable def NonnegSimpleFunction.constMul {n : ℕ} {Ω : Set (Fin n → ℝ)} (c : ℝ) (hc : 0 ≤ c) (f : NonnegSimpleFunction Ω) : NonnegSimpleFunction Ω

Pointwise scalar multiplication of a non-negative simple function by a nonnegative real.

Equations

• NonnegSimpleFunction.constMul c hc f = ⟨fun (x : ↑Ω) => c * ↑f x, ⋯⟩

theorem lebesgueIntegralNonnegSimple_constMul {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : NonnegSimpleFunction Ω) {c : ℝ} (hc : 0 < c) : lebesgueIntegralNonnegSimple (NonnegSimpleFunction.constMul c ⋯ f) = ENNReal.ofReal c * lebesgueIntegralNonnegSimple f

Proposition 8.1.3: if f : Ω → ℝ is a non-negative simple function and c > 0, then the integral scales linearly: ∫_Ω (c f) dm = c ∫_Ω f dm.

theorem helperForProposition_8_1_4_difference_isSimple {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) : IsSimpleFunction Ω fun (x : ↑Ω) => ↑g x - ↑f x

Helper for Proposition 8.1.4: the pointwise difference of two non-negative simple functions is simple.

theorem helperForProposition_8_1_4_difference_nonneg {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) (hfg : ∀ (x : ↑Ω), ↑f x ≤ ↑g x) (x : ↑Ω) : 0 ≤ ↑g x - ↑f x

Helper for Proposition 8.1.4: if f ≤ g pointwise then g - f is pointwise nonnegative.

noncomputable def helperForProposition_8_1_4_difference {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) (hfg : ∀ (x : ↑Ω), ↑f x ≤ ↑g x) : NonnegSimpleFunction Ω

Helper for Proposition 8.1.4: the non-negative simple remainder g - f.

Equations

• helperForProposition_8_1_4_difference f g hfg = ⟨fun (x : ↑Ω) => ↑g x - ↑f x, ⋯⟩

theorem helperForProposition_8_1_4_add_difference_eq {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) (hfg : ∀ (x : ↑Ω), ↑f x ≤ ↑g x) : f.add (helperForProposition_8_1_4_difference f g hfg) = g

Helper for Proposition 8.1.4: f + (g - f) = g as non-negative simple functions.

theorem lebesgueIntegralNonnegSimple_mono {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : NonnegSimpleFunction Ω) (hfg : ∀ (x : ↑Ω), ↑f x ≤ ↑g x) : lebesgueIntegralNonnegSimple f ≤ lebesgueIntegralNonnegSimple g

Proposition 8.1.4: if f, g : Ω → ℝ are non-negative simple functions and f(x) ≤ g(x) for every x ∈ Ω, then ∫_Ω f dm ≤ ∫_Ω g dm.

def HoldsForAlmostEverywhereOn {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (Ω : Set α) (P : α → Prop) : Prop

Definition 8.4: A property P holds for almost every x ∈ Ω (with respect to μ) if there is a measurable null set N ⊆ Ω such that P x holds for all x ∈ Ω \ N.

Equations

• HoldsForAlmostEverywhereOn μ Ω P = ∃ N ⊆ Ω, MeasurableSet N ∧ μ N = 0 ∧ ∀ ⦃x : α⦄, x ∈ Ω \ N → P x

theorem helperForProposition_8_2_nonzeroSetNull_of_aeEqZero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hAe : f =ᵐ[μ] 0) : μ {x : α | f x ≠ 0} = 0

Helper for Proposition 8.2: almost-everywhere vanishing gives a null nonzero set.

theorem helperForProposition_8_2_holdsOnUniv_of_aeEqZero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : f =ᵐ[μ] 0 → HoldsForAlmostEverywhereOn μ Set.univ fun (x : α) => f x = 0

Helper for Proposition 8.2: convert f = 0 almost everywhere to Definition 8.4 on univ.

theorem helperForProposition_8_2_aeEqZero_of_holdsOnUniv {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} : (HoldsForAlmostEverywhereOn μ Set.univ fun (x : α) => f x = 0) → f =ᵐ[μ] 0

Helper for Proposition 8.2: convert Definition 8.4 on univ to f = 0 almost everywhere.

theorem helperForProposition_8_2_holdsOnUniv_iff_aeEqZero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : (HoldsForAlmostEverywhereOn μ Set.univ fun (x : α) => f x = 0) ↔ f =ᵐ[μ] 0

Helper for Proposition 8.2: Definition 8.4 on univ is equivalent to f = 0 almost everywhere.

theorem proposition_8_2_lintegral_eq_zero_iff_holdsForAlmostEverywhereOn {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0

Proposition 8.2: if f : α → [0, ∞] is measurable, then its integral is zero iff f x = 0 for μ-almost every x.