Home | Metamath
Proof Explorer Theorem List (p. 244 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itg1addlem5 24301* | 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 24302 | 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 24303 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)})) | ||
Theorem | i1fmulc 24304 | 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 24305 | 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 24306* | 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 24307* | 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 24308* | Deduction form of i1fposd 24308. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ dom ∫1) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(0 ≤ 𝐴, 𝐴, 0)) ∈ dom ∫1) | ||
Theorem | i1fsub 24309 | 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 24310 | 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 24311* | 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 24312* | 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 24313* | Approximate version of itg1le 24314. 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 24314 | 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 24315* | 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 24316* | Lemma for mbfi1fseq 24322. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) ⇒ ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞)) | ||
Theorem | mbfi1fseqlem2 24317* | Lemma for mbfi1fseq 24322. (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 24318* | Lemma for mbfi1fseq 24322. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) | ||
Theorem | mbfi1fseqlem4 24319* | Lemma for mbfi1fseq 24322. 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 24320* | Lemma for mbfi1fseq 24322. 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 24321* | Lemma for mbfi1fseq 24322. 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 24322* | 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 24323* | Lemma for mbfi1flim 24324. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | ||
Theorem | mbfi1flim 24324* | 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 24325* | Lemma for mbfmul 24327. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | mbfmullem 24326 | Lemma for mbfmul 24327. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | mbfmul 24327 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) | ||
Theorem | itg2lcl 24328* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ 𝐿 ⊆ ℝ* | ||
Theorem | itg2val 24329* | Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < )) | ||
Theorem | itg2l 24330* | 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 24331* | Sufficient condition for elementhood in the set 𝐿. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ∈ 𝐿) | ||
Theorem | xrge0f 24332 | 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 24333 | The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*) | ||
Theorem | itg2ub 24334 | 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 24335* | 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 24336 | 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 24337 | 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 24338 | The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (∫2‘(ℝ × {0})) = 0 | ||
Theorem | itg2lecl 24339 | If an ∫2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ ∧ (∫2‘𝐹) ≤ 𝐴) → (∫2‘𝐹) ∈ ℝ) | ||
Theorem | itg2le 24340 | 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 24341* | 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 24342* | 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 24343* | 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 24356, 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 24344* | Approximate version of itg2ub 24334. If 𝐹 approximately dominates 𝐺, then ∫1𝐺 ≤ ∫2𝐹. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺 ∈ dom ∫1) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (∫1‘𝐺) ≤ (∫2‘𝐹)) | ||
Theorem | itg2lea 24345* | Approximate version of itg2le 24340. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫2𝐹 ≤ ∫2𝐺. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (∫2‘𝐹) ≤ (∫2‘𝐺)) | ||
Theorem | itg2eqa 24346* | 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 24347 | Lemma for itg2mulc 24348. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹))) | ||
Theorem | itg2mulc 24348 | 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 24349* | Lemma for itg2split 24350. (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 24350* | The ∫2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 24360 which requires CC.) (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 24351* | Lemma for itg2mono 24354. 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 24354. 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 24315. 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 24352* | Lemma for itg2mono 24354. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) & ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) & ⊢ (𝜑 → 𝑃 ∈ dom ∫1) & ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺) & ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ ℝ) | ||
Theorem | itg2monolem3 24353* | Lemma for itg2mono 24354. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) & ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) & ⊢ (𝜑 → 𝑃 ∈ dom ∫1) & ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺) & ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆) ⇒ ⊢ (𝜑 → (∫1‘𝑃) ≤ 𝑆) | ||
Theorem | itg2mono 24354* | The Monotone Convergence Theorem for nonnegative functions. If {(𝐹‘𝑛):𝑛 ∈ ℕ} is a monotone increasing sequence of positive, measurable, real-valued functions, and 𝐺 is the pointwise limit of the sequence, then (∫2‘𝐺) is the limit of the sequence {(∫2‘(𝐹‘𝑛)):𝑛 ∈ ℕ}. (Contributed by Mario Carneiro, 16-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) & ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) ⇒ ⊢ (𝜑 → (∫2‘𝐺) = 𝑆) | ||
Theorem | itg2i1fseqle 24355* | Subject to the conditions coming from mbfi1fseq 24322, the sequence of simple functions are all less than the target function 𝐹. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑃‘𝑀) ∘r ≤ 𝐹) | ||
Theorem | itg2i1fseq 24356* | Subject to the conditions coming from mbfi1fseq 24322, the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚))) ⇒ ⊢ (𝜑 → (∫2‘𝐹) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | itg2i1fseq2 24357* | In an extension to the results of itg2i1fseq 24356, if there is an upper bound on the integrals of the simple functions approaching 𝐹, then ∫2𝐹 is real and the standard limit relation applies. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑃‘𝑘)) ≤ 𝑀) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹)) | ||
Theorem | itg2i1fseq3 24358* | Special case of itg2i1fseq2 24357: if the integral of 𝐹 is a real number, then the standard limit relation holds on the integrals of simple functions approaching 𝐹. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚))) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹)) | ||
Theorem | itg2addlem 24359* | Lemma for itg2add 24360. (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ) & ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘r ≤ (𝑄‘(𝑛 + 1)))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (∫2‘(𝐹 ∘f + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺))) | ||
Theorem | itg2add 24360 | The ∫2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ) ⇒ ⊢ (𝜑 → (∫2‘(𝐹 ∘f + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺))) | ||
Theorem | itg2gt0 24361* | If the function 𝐹 is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ (𝜑 → 0 < (vol‘𝐴)) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 < (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → 0 < (∫2‘𝐹)) | ||
Theorem | itg2cnlem1 24362* | Lemma for itgcn 24443. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) = (∫2‘𝐹)) | ||
Theorem | itg2cnlem2 24363* | Lemma for itgcn 24443. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) | ||
Theorem | itg2cn 24364* | A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 24634 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) | ||
Theorem | ibllem 24365 | Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) | ||
Theorem | isibl 24366* | The predicate "𝐹 is integrable". The "integrable" predicate corresponds roughly to the range of validity of ∫𝐴𝐵 d𝑥, which is to say that the expression ∫𝐴𝐵 d𝑥 doesn't make sense unless (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘)))) & ⊢ (𝜑 → dom 𝐹 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘𝐺) ∈ ℝ))) | ||
Theorem | isibl2 24367* | The predicate "𝐹 is integrable" when 𝐹 is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘𝐺) ∈ ℝ))) | ||
Theorem | iblmbf 24368 | An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.) |
⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn) | ||
Theorem | iblitg 24369* | If a function is integrable, then the ∫2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝐾)))) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → (∫2‘𝐺) ∈ ℝ) | ||
Theorem | dfitg 24370* | Evaluate the class substitution in df-itg 24224. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))) ⇒ ⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))) | ||
Theorem | itgex 24371 | An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ∫𝐴𝐵 d𝑥 ∈ V | ||
Theorem | itgeq1f 24372 | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥) | ||
Theorem | itgeq1 24373* | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥) | ||
Theorem | nfitg1 24374 | Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ Ⅎ𝑥∫𝐴𝐵 d𝑥 | ||
Theorem | nfitg 24375* | Bound-variable hypothesis builder for an integral: if 𝑦 is (effectively) not free in 𝐴 and 𝐵, it is not free in ∫𝐴𝐵 d𝑥. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∫𝐴𝐵 d𝑥 | ||
Theorem | cbvitg 24376* | Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦 | ||
Theorem | cbvitgv 24377* | Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦 | ||
Theorem | itgeq2 24378 | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥) | ||
Theorem | itgresr 24379 | The domain of an integral only matters in its intersection with ℝ. (Contributed by Mario Carneiro, 29-Jun-2014.) |
⊢ ∫𝐴𝐵 d𝑥 = ∫(𝐴 ∩ ℝ)𝐵 d𝑥 | ||
Theorem | itg0 24380 | The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ∫∅𝐴 d𝑥 = 0 | ||
Theorem | itgz 24381 | The integral of zero on any set is zero. (Contributed by Mario Carneiro, 29-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ∫𝐴0 d𝑥 = 0 | ||
Theorem | itgeq2dv 24382* | Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥) | ||
Theorem | itgmpt 24383* | Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) d𝑦) | ||
Theorem | itgcl 24384* | The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ) | ||
Theorem | itgvallem 24385* | Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (i↑𝐾) = 𝑇 ⇒ ⊢ (𝑘 = 𝐾 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 𝑇))), (ℜ‘(𝐵 / 𝑇)), 0)))) | ||
Theorem | itgvallem3 24386* | Lemma for itgposval 24396 and itgreval 24397. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 0) ⇒ ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = 0) | ||
Theorem | ibl0 24387 | The zero function is integrable on any measurable set. (Unlike iblconst 24418, this does not require 𝐴 to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1) | ||
Theorem | iblcnlem1 24388* | Lemma for iblcnlem 24389. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) & ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) & ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) & ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) | ||
Theorem | iblcnlem 24389* | Expand out the forall in isibl2 24367. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) & ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) & ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) & ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) | ||
Theorem | itgcnlem 24390* | Expand out the sum in dfitg 24370. (Contributed by Mario Carneiro, 1-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) & ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) & ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) & ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((𝑅 − 𝑆) + (i · (𝑇 − 𝑈)))) | ||
Theorem | iblrelem 24391* | Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ))) | ||
Theorem | iblposlem 24392* | Lemma for iblpos 24393. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = 0) | ||
Theorem | iblpos 24393* | Integrability of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ))) | ||
Theorem | iblre 24394* | Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1))) | ||
Theorem | itgrevallem1 24395* | Lemma for itgposval 24396 and itgreval 24397. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) − (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))) | ||
Theorem | itgposval 24396* | The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) | ||
Theorem | itgreval 24397* | Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥)) | ||
Theorem | itgrecl 24398* | Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℝ) | ||
Theorem | iblcn 24399* | Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1))) | ||
Theorem | itgcnval 24400* | Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |