![]() |
Metamath
Proof Explorer Theorem List (p. 258 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mbfposb 25701* | A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn))) | ||
Theorem | ismbf3d 25702* | Simplified form of ismbfd 25687. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfimaopnlem 25703* | Lemma for mbfimaopn 25704. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐵 = ((,) “ (ℚ × ℚ)) & ⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | mbfimaopn 25704 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25706, which explains why 𝐴 ∈ dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | mbfimaopn2 25705 | The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐵) ⇒ ⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ ℂ) ∧ 𝐶 ∈ 𝐾) → (◡𝐹 “ 𝐶) ∈ dom vol) | ||
Theorem | cncombf 25706 | The composition of a continuous function with a measurable function is measurable. (More generally, 𝐺 can be a Borel-measurable function, but notably the condition that 𝐺 be only measurable is too weak, the usual counterexample taking 𝐺 to be the Cantor function and 𝐹 the indicator function of the 𝐺-image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ MblFn) | ||
Theorem | cnmbf 25707 | A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 26-Mar-2015.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) → 𝐹 ∈ MblFn) | ||
Theorem | mbfaddlem 25708 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) | ||
Theorem | mbfadd 25709 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) | ||
Theorem | mbfsub 25710 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ MblFn) | ||
Theorem | mbfmulc2 25711* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) | ||
Theorem | mbfsup 25712* | The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, 𝐵(𝑛, 𝑥) is a function of both 𝑛 and 𝑥, since it is an 𝑛-indexed sequence of functions on 𝑥. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
Theorem | mbfinf 25713* | The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 13-Sep-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
Theorem | mbflimsup 25714* | The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵))) & ⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*), ℝ*, < )) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
Theorem | mbflimlem 25715* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | ||
Theorem | mbflim 25716* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | ||
Syntax | c0p 25717 | Extend class notation to include the zero polynomial. |
class 0𝑝 | ||
Definition | df-0p 25718 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ 0𝑝 = (ℂ × {0}) | ||
Theorem | 0pval 25719 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (0𝑝‘𝐴) = 0) | ||
Theorem | 0plef 25720 | Two ways to say that the function 𝐹 on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹)) | ||
Theorem | 0pledm 25721 | Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹 Fn 𝐴) ⇒ ⊢ (𝜑 → (0𝑝 ∘r ≤ 𝐹 ↔ (𝐴 × {0}) ∘r ≤ 𝐹)) | ||
Theorem | isi1f 25722 | The predicate "𝐹 is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom 𝐹 ∈ dom ∫1 to represent this concept because ∫1 is the first preparation function for our final definition ∫ (see df-itg 25671); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))) | ||
Theorem | i1fmbf 25723 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn) | ||
Theorem | i1ff 25724 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ) | ||
Theorem | i1frn 25725 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin) | ||
Theorem | i1fima 25726 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | i1fima2 25727 | Any preimage of a simple function not containing zero has finite measure. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴) → (vol‘(◡𝐹 “ 𝐴)) ∈ ℝ) | ||
Theorem | i1fima2sn 25728 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ (𝐵 ∖ {0})) → (vol‘(◡𝐹 “ {𝐴})) ∈ ℝ) | ||
Theorem | i1fd 25729* | A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ran 𝐹 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ∫1) | ||
Theorem | i1f0rn 25730 | Any simple function takes the value zero on a set of unbounded measure, so in particular this set is not empty. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹) | ||
Theorem | itg1val 25731* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) | ||
Theorem | itg1val2 25732* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ (𝐴 ∈ Fin ∧ (ran 𝐹 ∖ {0}) ⊆ 𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) → (∫1‘𝐹) = Σ𝑥 ∈ 𝐴 (𝑥 · (vol‘(◡𝐹 “ {𝑥})))) | ||
Theorem | itg1cl 25733 | Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) ∈ ℝ) | ||
Theorem | itg1ge0 25734 | Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹) → 0 ≤ (∫1‘𝐹)) | ||
Theorem | i1f0 25735 | The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (ℝ × {0}) ∈ dom ∫1 | ||
Theorem | itg10 25736 | The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (∫1‘(ℝ × {0})) = 0 | ||
Theorem | i1f1lem 25737* | Lemma for i1f1 25738 and itg11 25739. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) ⇒ ⊢ (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (◡𝐹 “ {1}) = 𝐴)) | ||
Theorem | i1f1 25738* | Base case simple functions are indicator functions of measurable sets. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) ⇒ ⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → 𝐹 ∈ dom ∫1) | ||
Theorem | itg11 25739* | The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) ⇒ ⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (∫1‘𝐹) = (vol‘𝐴)) | ||
Theorem | itg1addlem1 25740* | Decompose a preimage, which is always a disjoint union. (Contributed by Mario Carneiro, 25-Jun-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ (◡𝐹 “ {𝑘})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (vol‘𝐵)) | ||
Theorem | i1faddlem 25741* | Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | ||
Theorem | i1fmullem 25742* | Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | ||
Theorem | i1fadd 25743 | The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom ∫1) | ||
Theorem | i1fmul 25744 | The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ dom ∫1) | ||
Theorem | itg1addlem2 25745* | Lemma for itg1add 25750. The function 𝐼 represents the pieces into which we will break up the domain of the sum. Since it is infinite only when both 𝑖 and 𝑗 are zero, we arbitrarily define it to be zero there to simplify the sums that are manipulated in itg1addlem4 25747 and itg1addlem5 25749. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) ⇒ ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ) | ||
Theorem | itg1addlem3 25746* | Lemma for itg1add 25750. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴𝐼𝐵) = (vol‘((◡𝐹 “ {𝐴}) ∩ (◡𝐺 “ {𝐵})))) | ||
Theorem | itg1addlem4 25747* | Lemma for itg1add 25750. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof shortened by SN, 3-Oct-2024.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) & ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) | ||
Theorem | itg1addlem4OLD 25748* | Obsolete version of itg1addlem4 25747 as of 6-Oct-2024. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) & ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) | ||
Theorem | itg1addlem5 25749* | Lemma for itg1add 25750. (Contributed by Mario Carneiro, 27-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) & ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺))) | ||
Theorem | itg1add 25750 | The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺))) | ||
Theorem | i1fmulclem 25751 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)})) | ||
Theorem | i1fmulc 25752 | A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℝ × {𝐴}) ∘f · 𝐹) ∈ dom ∫1) | ||
Theorem | itg1mulc 25753 | The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫1‘𝐹))) | ||
Theorem | i1fres 25754* | The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside 𝐴.) (Contributed by Mario Carneiro, 29-Jun-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0)) ⇒ ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol) → 𝐺 ∈ dom ∫1) | ||
Theorem | i1fpos 25755* | The positive part of a simple function is simple. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ⇒ ⊢ (𝐹 ∈ dom ∫1 → 𝐺 ∈ dom ∫1) | ||
Theorem | i1fposd 25756* | Deduction form of i1fposd 25756. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(0 ≤ 𝐴, 𝐴, 0)) ∈ dom ∫1) | ||
Theorem | i1fsub 25757 | The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘f − 𝐺) ∈ dom ∫1) | ||
Theorem | itg1sub 25758 | The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (∫1‘(𝐹 ∘f − 𝐺)) = ((∫1‘𝐹) − (∫1‘𝐺))) | ||
Theorem | itg10a 25759* | The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) = 0) ⇒ ⊢ (𝜑 → (∫1‘𝐹) = 0) | ||
Theorem | itg1ge0a 25760* | The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → 0 ≤ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → 0 ≤ (∫1‘𝐹)) | ||
Theorem | itg1lea 25761* | Approximate version of itg1le 25762. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫1𝐹 ≤ ∫1𝐺. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (∫1‘𝐹) ≤ (∫1‘𝐺)) | ||
Theorem | itg1le 25762 | If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺) → (∫1‘𝐹) ≤ (∫1‘𝐺)) | ||
Theorem | itg1climres 25763* | Restricting the simple function 𝐹 to the increasing sequence 𝐴(𝑛) of measurable sets whose union is ℝ yields a sequence of simple functions whose integrals approach the integral of 𝐹. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐴:ℕ⟶dom vol) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) & ⊢ (𝜑 → ∪ ran 𝐴 = ℝ) & ⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫1‘𝐺)) ⇝ (∫1‘𝐹)) | ||
Theorem | mbfi1fseqlem1 25764* | Lemma for mbfi1fseq 25770. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) ⇒ ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞)) | ||
Theorem | mbfi1fseqlem2 25765* | Lemma for mbfi1fseq 25770. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) | ||
Theorem | mbfi1fseqlem3 25766* | Lemma for mbfi1fseq 25770. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) | ||
Theorem | mbfi1fseqlem4 25767* | Lemma for mbfi1fseq 25770. This lemma is not as interesting as it is long - it is simply checking that 𝐺 is in fact a sequence of simple functions, by verifying that its range is in (0...𝑛2↑𝑛) / (2↑𝑛) (which is to say, the numbers from 0 to 𝑛 in increments of 1 / (2↑𝑛)), and also that the preimage of each point 𝑘 is measurable, because it is equal to (-𝑛[,]𝑛) ∩ (◡𝐹 “ (𝑘[,)𝑘 + 1 / (2↑𝑛))) for 𝑘 < 𝑛 and (-𝑛[,]𝑛) ∩ (◡𝐹 “ (𝑘[,)+∞)) for 𝑘 = 𝑛. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1) | ||
Theorem | mbfi1fseqlem5 25768* | Lemma for mbfi1fseq 25770. Verify that 𝐺 describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0𝑝 ∘r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘r ≤ (𝐺‘(𝐴 + 1)))) | ||
Theorem | mbfi1fseqlem6 25769* | Lemma for mbfi1fseq 25770. Verify that 𝐺 converges pointwise to 𝐹, and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1fseq 25770* | A characterization of measurability in terms of simple functions (this is an if and only if for nonnegative functions, although we don't prove it). Any nonnegative measurable function is the limit of an increasing sequence of nonnegative simple functions. This proof is an example of a poor de Bruijn factor - the formalized proof is much longer than an average hand proof, which usually just describes the function 𝐺 and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1flimlem 25771* | Lemma for mbfi1flim 25772. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1flim 25772* | Any real measurable function has a sequence of simple functions that converges to it. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfmullem2 25773* | Lemma for mbfmul 25775. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | mbfmullem 25774 | Lemma for mbfmul 25775. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | mbfmul 25775 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | itg2lcl 25776* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ 𝐿 ⊆ ℝ* | ||
Theorem | itg2val 25777* | Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < )) | ||
Theorem | itg2l 25778* | Elementhood in the set 𝐿 of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ (𝐴 ∈ 𝐿 ↔ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = (∫1‘𝑔))) | ||
Theorem | itg2lr 25779* | Sufficient condition for elementhood in the set 𝐿. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ∈ 𝐿) | ||
Theorem | xrge0f 25780 | A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 28-Jul-2014.) |
⊢ ((𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹) → 𝐹:ℝ⟶(0[,]+∞)) | ||
Theorem | itg2cl 25781 | The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*) | ||
Theorem | itg2ub 25782 | The integral of a nonnegative real function 𝐹 is an upper bound on the integrals of all simple functions 𝐺 dominated by 𝐹. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ≤ (∫2‘𝐹)) | ||
Theorem | itg2leub 25783* | Any upper bound on the integrals of all simple functions 𝐺 dominated by 𝐹 is greater than (∫2‘𝐹), the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ*) → ((∫2‘𝐹) ≤ 𝐴 ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 → (∫1‘𝑔) ≤ 𝐴))) | ||
Theorem | itg2ge0 25784 | The integral of a nonnegative real function is greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2‘𝐹)) | ||
Theorem | itg2itg1 25785 | The integral of a nonnegative simple function using ∫2 is the same as its value under ∫1. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹) → (∫2‘𝐹) = (∫1‘𝐹)) | ||
Theorem | itg20 25786 | The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (∫2‘(ℝ × {0})) = 0 | ||
Theorem | itg2lecl 25787 | If an ∫2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ ∧ (∫2‘𝐹) ≤ 𝐴) → (∫2‘𝐹) ∈ ℝ) | ||
Theorem | itg2le 25788 | If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐺:ℝ⟶(0[,]+∞) ∧ 𝐹 ∘r ≤ 𝐺) → (∫2‘𝐹) ≤ (∫2‘𝐺)) | ||
Theorem | itg2const 25789* | Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ (0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) | ||
Theorem | itg2const2 25790* | When the base set of a constant function has infinite volume, the integral is also infinite and vice-versa. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+) → ((vol‘𝐴) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ)) | ||
Theorem | itg2seq 25791* | Definitional property of the ∫2 integral: for any function 𝐹 there is a countable sequence 𝑔 of simple functions less than 𝐹 whose integrals converge to the integral of 𝐹. (This theorem is for the most part unnecessary in lieu of itg2i1fseq 25804, but unlike that theorem this one doesn't require 𝐹 to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.) |
⊢ (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))) | ||
Theorem | itg2uba 25792* | Approximate version of itg2ub 25782. If 𝐹 approximately dominates 𝐺, then ∫1𝐺 ≤ ∫2𝐹. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (∫1‘𝐺) ≤ (∫2‘𝐹)) | ||
Theorem | itg2lea 25793* | Approximate version of itg2le 25788. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫2𝐹 ≤ ∫2𝐺. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (∫2‘𝐹) ≤ (∫2‘𝐺)) | ||
Theorem | itg2eqa 25794* | Approximate equality of integrals. If 𝐹 = 𝐺 for almost all 𝑥, then ∫2𝐹 = ∫2𝐺. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (∫2‘𝐹) = (∫2‘𝐺)) | ||
Theorem | itg2mulclem 25795 | Lemma for itg2mulc 25796. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹))) | ||
Theorem | itg2mulc 25796 | The integral of a nonnegative constant times a function is the constant times the integral of the original function. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫2‘𝐹))) | ||
Theorem | itg2splitlem 25797* | Lemma for itg2split 25798. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ (𝜑 → 𝐵 ∈ dom vol) & ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ) ⇒ ⊢ (𝜑 → (∫2‘𝐻) ≤ ((∫2‘𝐹) + (∫2‘𝐺))) | ||
Theorem | itg2split 25798* | The ∫2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25808, which requires countable choice. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ (𝜑 → 𝐵 ∈ dom vol) & ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ) ⇒ ⊢ (𝜑 → (∫2‘𝐻) = ((∫2‘𝐹) + (∫2‘𝐺))) | ||
Theorem | itg2monolem1 25799* | Lemma for itg2mono 25802. We show that for any constant 𝑡 less than one, 𝑡 · ∫1𝐻 is less than 𝑆, and so ∫1𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 25802. Consider the sequence 𝐴(𝑛) = {𝑥 ∣ 𝑡 · 𝐻 ≤ 𝐹(𝑛)}. This is an increasing sequence of measurable sets whose union is ℝ, and so 𝐻 ↾ 𝐴(𝑛) has an integral which equals ∫1𝐻 in the limit, by itg1climres 25763. Then by taking the limit in (𝑡 · 𝐻) ↾ 𝐴(𝑛) ≤ 𝐹(𝑛), we get 𝑡 · ∫1𝐻 ≤ 𝑆 as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) & ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) & ⊢ (𝜑 → 𝑇 ∈ (0(,)1)) & ⊢ (𝜑 → 𝐻 ∈ dom ∫1) & ⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺) & ⊢ (𝜑 → 𝑆 ∈ ℝ) & ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)}) ⇒ ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆) | ||
Theorem | itg2monolem2 25800* | Lemma for itg2mono 25802. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) & ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) & ⊢ (𝜑 → 𝑃 ∈ dom ∫1) & ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺) & ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |