Home | Metamath
Proof Explorer Theorem List (p. 233 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mbfdm 23201 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol) | ||
Theorem | mbfconstlem 23202 | Lemma for mbfconst 23208. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐶 ∈ ℝ) → (◡(𝐴 × {𝐶}) “ 𝐵) ∈ dom vol) | ||
Theorem | ismbf 23203* | The predicate "𝐹 is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl 23101. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) | ||
Theorem | ismbfcn 23204 | A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))) | ||
Theorem | mbfima 23205 | Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝐵(,)𝐶)) ∈ dom vol) | ||
Theorem | mbfimaicc 23206 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (◡𝐹 “ (𝐵[,]𝐶)) ∈ dom vol) | ||
Theorem | mbfimasn 23207 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ ∧ 𝐵 ∈ ℝ) → (◡𝐹 “ {𝐵}) ∈ dom vol) | ||
Theorem | mbfconst 23208 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ MblFn) | ||
Theorem | mbfid 23209 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn) | ||
Theorem | mbfmptcl 23210* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | ||
Theorem | mbfdm2 23211* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom vol) | ||
Theorem | ismbfcn2 23212* | A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn))) | ||
Theorem | ismbfd 23213* | Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d 23227. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | ismbf2d 23214* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfeqalem 23215* | Lemma for mbfeqa 23216. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ MblFn)) | ||
Theorem | mbfeqa 23216* | If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 2-Sep-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ MblFn)) | ||
Theorem | mbfres 23217 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴) ∈ MblFn) | ||
Theorem | mbfres2 23218 | Measurability of a piecewise function: if 𝐹 is measurable on subsets 𝐵 and 𝐶 of its domain, and these pieces make up all of 𝐴, then 𝐹 is measurable on the whole domain. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ MblFn) & ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ MblFn) & ⊢ (𝜑 → (𝐵 ∪ 𝐶) = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfss 23219* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) | ||
Theorem | mbfmulc2lem 23220 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn) | ||
Theorem | mbfmulc2re 23221 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn) | ||
Theorem | mbfmax 23222* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥))) ⇒ ⊢ (𝜑 → 𝐻 ∈ MblFn) | ||
Theorem | mbfneg 23223* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn) | ||
Theorem | mbfpos 23224* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) | ||
Theorem | mbfposr 23225* | Converse to mbfpos 23224. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | ||
Theorem | mbfposb 23226* | 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 23227* | Simplified form of ismbfd 23213. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfimaopnlem 23228* | Lemma for mbfimaopn 23229. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐵 = ((,) “ (ℚ × ℚ)) & ⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | mbfimaopn 23229 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 23231, 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 23230 | 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 23231 | 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 23232 | 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 23233 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ MblFn) | ||
Theorem | mbfadd 23234 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ MblFn) | ||
Theorem | mbfsub 23235 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) ∈ MblFn) | ||
Theorem | mbfmulc2 23236* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) | ||
Theorem | mbfsup 23237* | 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 23238* | 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 23239* | 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 23240* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | ||
Theorem | mbflim 23241* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | ||
Syntax | c0p 23242 | Extend class notation to include the zero polynomial. |
class 0𝑝 | ||
Definition | df-0p 23243 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ 0𝑝 = (ℂ × {0}) | ||
Theorem | 0pval 23244 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (0𝑝‘𝐴) = 0) | ||
Theorem | 0plef 23245 | Two ways to say that the function 𝐹 on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘𝑟 ≤ 𝐹)) | ||
Theorem | 0pledm 23246 | 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𝑝 ∘𝑟 ≤ 𝐹 ↔ (𝐴 × {0}) ∘𝑟 ≤ 𝐹)) | ||
Theorem | isi1f 23247 | 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 23198); 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 23248 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn) | ||
Theorem | i1ff 23249 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ) | ||
Theorem | i1frn 23250 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin) | ||
Theorem | i1fima 23251 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | i1fima2 23252 | 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 23253 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ (𝐵 ∖ {0})) → (vol‘(◡𝐹 “ {𝐴})) ∈ ℝ) | ||
Theorem | i1fd 23254* | 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 23255 | 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 23256* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) | ||
Theorem | itg1val2 23257* | 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 23258 | Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) ∈ ℝ) | ||
Theorem | itg1ge0 23259 | Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘𝑟 ≤ 𝐹) → 0 ≤ (∫1‘𝐹)) | ||
Theorem | i1f0 23260 | The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (ℝ × {0}) ∈ dom ∫1 | ||
Theorem | itg10 23261 | The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (∫1‘(ℝ × {0})) = 0 | ||
Theorem | i1f1lem 23262* | Lemma for i1f1 23263 and itg11 23264. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) ⇒ ⊢ (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (◡𝐹 “ {1}) = 𝐴)) | ||
Theorem | i1f1 23263* | 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 23264* | 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 23265* | 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 23266* | Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | ||
Theorem | i1fmullem 23267* | Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | ||
Theorem | i1fadd 23268 | The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom ∫1) | ||
Theorem | i1fmul 23269 | The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ dom ∫1) | ||
Theorem | itg1addlem2 23270* | Lemma for itg1add 23274. 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 23272 and itg1addlem5 23273. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) ⇒ ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ) | ||
Theorem | itg1addlem3 23271* | Lemma for itg1add 23274. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴𝐼𝐵) = (vol‘((◡𝐹 “ {𝐴}) ∩ (◡𝐺 “ {𝐵})))) | ||
Theorem | itg1addlem4 23272* | Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) & ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘𝑓 + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) | ||
Theorem | itg1addlem5 23273* | Lemma for itg1add . (Contributed by Mario Carneiro, 27-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) & ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘𝑓 + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺))) | ||
Theorem | itg1add 23274 | 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‘(𝐹 ∘𝑓 + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺))) | ||
Theorem | i1fmulclem 23275 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)})) | ||
Theorem | i1fmulc 23276 | A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1) | ||
Theorem | itg1mulc 23277 | 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‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1‘𝐹))) | ||
Theorem | i1fres 23278* | 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 23279* | 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 23280* | Deduction form of i1fposd 23280. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(0 ≤ 𝐴, 𝐴, 0)) ∈ dom ∫1) | ||
Theorem | i1fsub 23281 | The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 − 𝐺) ∈ dom ∫1) | ||
Theorem | itg1sub 23282 | The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (∫1‘(𝐹 ∘𝑓 − 𝐺)) = ((∫1‘𝐹) − (∫1‘𝐺))) | ||
Theorem | itg10a 23283* | 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 23284* | 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 23285* | Approximate version of itg1le 23286. 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 23286 | 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 ∧ 𝐹 ∘𝑟 ≤ 𝐺) → (∫1‘𝐹) ≤ (∫1‘𝐺)) | ||
Theorem | itg1climres 23287* | 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 23288* | Lemma for mbfi1fseq 23294. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) ⇒ ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞)) | ||
Theorem | mbfi1fseqlem2 23289* | Lemma for mbfi1fseq 23294. (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 23290* | Lemma for mbfi1fseq 23294. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) | ||
Theorem | mbfi1fseqlem4 23291* | Lemma for mbfi1fseq 23294. 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 23292* | Lemma for mbfi1fseq 23294. Verify that 𝐺 describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0𝑝 ∘𝑟 ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘𝑟 ≤ (𝐺‘(𝐴 + 1)))) | ||
Theorem | mbfi1fseqlem6 23293* | Lemma for mbfi1fseq 23294. Verify that 𝐺 converges pointwise to 𝐹, and wrap up the existence 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𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1fseq 23294* | 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𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1flimlem 23295* | Lemma for mbfi1flim 23296. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1flim 23296* | 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 23297* | Lemma for mbfmul 23299. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) | ||
Theorem | mbfmullem 23298 | Lemma for mbfmul 23299. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) | ||
Theorem | mbfmul 23299 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) | ||
Theorem | itg2lcl 23300* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ 𝐿 ⊆ ℝ* |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |