Home | Metamath
Proof Explorer Theorem List (p. 246 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mbfimasn 24501 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ ∧ 𝐵 ∈ ℝ) → (◡𝐹 “ {𝐵}) ∈ dom vol) | ||
Theorem | mbfconst 24502 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ MblFn) | ||
Theorem | mbf0 24503 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
⊢ ∅ ∈ MblFn | ||
Theorem | mbfid 24504 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn) | ||
Theorem | mbfmptcl 24505* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | ||
Theorem | mbfdm2 24506* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom vol) | ||
Theorem | ismbfcn2 24507* | 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 24508* | 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 24523. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | ismbf2d 24509* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfeqalem1 24510* | Lemma for mbfeqalem2 24511. (Contributed by Mario Carneiro, 2-Sep-2014.) (Revised by AV, 19-Aug-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐵 ↦ 𝐶) “ 𝑦) ∖ (◡(𝑥 ∈ 𝐵 ↦ 𝐷) “ 𝑦)) ∈ dom vol) | ||
Theorem | mbfeqalem2 24511* | Lemma for mbfeqa 24512. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by AV, 19-Aug-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ MblFn)) | ||
Theorem | mbfeqa 24512* | 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 24513 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴) ∈ MblFn) | ||
Theorem | mbfres2 24514 | 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 24515* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) | ||
Theorem | mbfmulc2lem 24516 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn) | ||
Theorem | mbfmulc2re 24517 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn) | ||
Theorem | mbfmax 24518* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥))) ⇒ ⊢ (𝜑 → 𝐻 ∈ MblFn) | ||
Theorem | mbfneg 24519* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn) | ||
Theorem | mbfpos 24520* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) | ||
Theorem | mbfposr 24521* | Converse to mbfpos 24520. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | ||
Theorem | mbfposb 24522* | 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 24523* | Simplified form of ismbfd 24508. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfimaopnlem 24524* | Lemma for mbfimaopn 24525. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐵 = ((,) “ (ℚ × ℚ)) & ⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | mbfimaopn 24525 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 24527, 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 24526 | 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 24527 | 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 24528 | 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 24529 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) | ||
Theorem | mbfadd 24530 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) | ||
Theorem | mbfsub 24531 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ MblFn) | ||
Theorem | mbfmulc2 24532* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) | ||
Theorem | mbfsup 24533* | 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 24534* | 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 24535* | 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 24536* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | ||
Theorem | mbflim 24537* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | ||
Syntax | c0p 24538 | Extend class notation to include the zero polynomial. |
class 0𝑝 | ||
Definition | df-0p 24539 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ 0𝑝 = (ℂ × {0}) | ||
Theorem | 0pval 24540 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (0𝑝‘𝐴) = 0) | ||
Theorem | 0plef 24541 | Two ways to say that the function 𝐹 on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹)) | ||
Theorem | 0pledm 24542 | 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 24543 | 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 24492); 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 24544 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn) | ||
Theorem | i1ff 24545 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ) | ||
Theorem | i1frn 24546 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin) | ||
Theorem | i1fima 24547 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
Theorem | i1fima2 24548 | 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 24549 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ (𝐵 ∖ {0})) → (vol‘(◡𝐹 “ {𝐴})) ∈ ℝ) | ||
Theorem | i1fd 24550* | 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 24551 | 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 24552* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) | ||
Theorem | itg1val2 24553* | 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 24554 | Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) ∈ ℝ) | ||
Theorem | itg1ge0 24555 | Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹) → 0 ≤ (∫1‘𝐹)) | ||
Theorem | i1f0 24556 | The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (ℝ × {0}) ∈ dom ∫1 | ||
Theorem | itg10 24557 | The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (∫1‘(ℝ × {0})) = 0 | ||
Theorem | i1f1lem 24558* | Lemma for i1f1 24559 and itg11 24560. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) ⇒ ⊢ (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (◡𝐹 “ {1}) = 𝐴)) | ||
Theorem | i1f1 24559* | 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 24560* | 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 24561* | 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 24562* | Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | ||
Theorem | i1fmullem 24563* | Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | ||
Theorem | i1fadd 24564 | 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 24565 | 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 24566* | Lemma for itg1add 24571. 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 24568 and itg1addlem5 24570. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) ⇒ ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ) | ||
Theorem | itg1addlem3 24567* | Lemma for itg1add 24571. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴𝐼𝐵) = (vol‘((◡𝐹 “ {𝐴}) ∩ (◡𝐺 “ {𝐵})))) | ||
Theorem | itg1addlem4 24568* | Lemma for itg1add . (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 24569* | Obsolete version of itg1addlem4 24568. (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 24570* | Lemma for itg1add . (Contributed by Mario Carneiro, 27-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) & ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) ⇒ ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺))) | ||
Theorem | itg1add 24571 | 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 24572 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)})) | ||
Theorem | i1fmulc 24573 | 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 24574 | 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 24575* | 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 24576* | 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 24577* | Deduction form of i1fposd 24577. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(0 ≤ 𝐴, 𝐴, 0)) ∈ dom ∫1) | ||
Theorem | i1fsub 24578 | 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 24579 | 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 24580* | 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 24581* | 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 24582* | Approximate version of itg1le 24583. 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 24583 | 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 24584* | 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 24585* | Lemma for mbfi1fseq 24591. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) ⇒ ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞)) | ||
Theorem | mbfi1fseqlem2 24586* | Lemma for mbfi1fseq 24591. (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 24587* | Lemma for mbfi1fseq 24591. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) | ||
Theorem | mbfi1fseqlem4 24588* | Lemma for mbfi1fseq 24591. 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 24589* | Lemma for mbfi1fseq 24591. 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 24590* | Lemma for mbfi1fseq 24591. 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 24591* | 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 24592* | Lemma for mbfi1flim 24593. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1flim 24593* | 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 24594* | Lemma for mbfmul 24596. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | mbfmullem 24595 | Lemma for mbfmul 24596. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | mbfmul 24596 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | itg2lcl 24597* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ 𝐿 ⊆ ℝ* | ||
Theorem | itg2val 24598* | Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < )) | ||
Theorem | itg2l 24599* | 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 24600* | Sufficient condition for elementhood in the set 𝐿. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ∈ 𝐿) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |