![]() |
Metamath
Proof Explorer Theorem List (p. 465 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 | sge0seq 46401 | A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) & ⊢ 𝐺 = seq𝑀( + , 𝐹) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran 𝐺, ℝ*, < )) | ||
Theorem | sge0reuz 46402* | Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, < )) | ||
Theorem | sge0reuzb 46403* | Value of the generalized sum of uniformly bounded nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 Σ𝑘 ∈ (𝑀...𝑛)𝐵 ≤ 𝑥) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ, < )) | ||
Proofs for most of the theorems in section 112 of [Fremlin1] | ||
Syntax | cmea 46404 | Extend class notation with the class of measures. |
class Meas | ||
Definition | df-mea 46405* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))} | ||
Theorem | ismea 46406* | Express the predicate "𝑀 is a measure." Definition 112A of [Fremlin1] p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = (Σ^‘(𝑀 ↾ 𝑥))))) | ||
Theorem | dmmeasal 46407 | The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | meaf 46408 | A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 ⇒ ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) | ||
Theorem | mea0 46409 | The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) ⇒ ⊢ (𝜑 → (𝑀‘∅) = 0) | ||
Theorem | nnfoctbdjlem 46410* | There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) | ||
Theorem | nnfoctbdj 46411* | There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) | ||
Theorem | meadjuni 46412* | The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝑥) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑋) = (Σ^‘(𝑀 ↾ 𝑋))) | ||
Theorem | meacl 46413 | The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | iundjiunlem 46414* | The sets in the sequence 𝐹 are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) & ⊢ (𝜑 → 𝐽 ∈ 𝑍) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) & ⊢ (𝜑 → 𝐽 < 𝐾) ⇒ ⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅) | ||
Theorem | iundjiun 46415* | Given a sequence 𝐸 of sets, a sequence 𝐹 of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑉) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) | ||
Theorem | meaxrcl 46416 | The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ*) | ||
Theorem | meadjun 46417 | The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | ||
Theorem | meassle 46418 | The measure of a set is greater than or equal to the measure of a subset, Property 112C (b) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵)) | ||
Theorem | meaunle 46419 | The measure of the union of two sets is less than or equal to the sum of the measures, Property 112C (c) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | ||
Theorem | meadjiunlem 46420* | The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐺:𝑋⟶𝑆) & ⊢ 𝑌 = {𝑖 ∈ 𝑋 ∣ (𝐺‘𝑖) ≠ ∅} & ⊢ (𝜑 → Disj 𝑖 ∈ 𝑋 (𝐺‘𝑖)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑀 ∘ 𝐺))) | ||
Theorem | meadjiun 46421* | The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑘 ∈ 𝐴 𝐵) = (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)))) | ||
Theorem | ismeannd 46422* | Sufficient condition to prove that 𝑀 is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑛 ∈ ℕ (𝑒‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛))))) ⇒ ⊢ (𝜑 → 𝑀 ∈ Meas) | ||
Theorem | meaiunlelem 46423* | The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))) | ||
Theorem | meaiunle 46424* | The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))) | ||
Theorem | psmeasurelem 46425* | 𝑀 applied to a disjoint union of subsets of its domain is the sum of 𝑀 applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞)) & ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥))) & ⊢ (𝜑 → 𝑀:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑌 𝑦) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑌) = (Σ^‘(𝑀 ↾ 𝑌))) | ||
Theorem | psmeasure 46426* | Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞)) & ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥))) ⇒ ⊢ (𝜑 → 𝑀 ∈ Meas) | ||
Theorem | voliunsge0lem 46427* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝑆 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))) & ⊢ (𝜑 → 𝐸:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) | ||
Theorem | voliunsge0 46428* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐸:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) | ||
Theorem | volmea 46429 | The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → vol ∈ Meas) | ||
Theorem | meage0 46430 | If the measure of a measurable set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) ⇒ ⊢ (𝜑 → 0 ≤ (𝑀‘𝐴)) | ||
Theorem | meadjunre 46431 | The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) + (𝑀‘𝐵))) | ||
Theorem | meassre 46432 | If the measure of a measurable set is real, then the measure of any of its measurable subsets is real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ) | ||
Theorem | meale0eq0 46433 | A measure that is less than or equal to 0 is 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) & ⊢ (𝜑 → (𝑀‘𝐴) ≤ 0) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = 0) | ||
Theorem | meadif 46434 | The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∖ 𝐵)) = ((𝑀‘𝐴) − (𝑀‘𝐵))) | ||
Theorem | meaiuninclem 46435* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc 46436* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc2 46437* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝐵) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiunincf 46438* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc3v 46439* | Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 46436 and meaiuninc2 46437 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc3 46440* | Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 46436 and meaiuninc2 46437 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiininclem 46441* | Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁)) & ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) & ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiininc 46442* | Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁)) & ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiininc2 46443* | Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) & ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝑀‘(𝐸‘𝑘)) ∈ ℝ) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Proofs for most of the theorems in section 113 of [Fremlin1] | ||
Syntax | come 46444 | Extend class notation with the class of outer measures. |
class OutMeas | ||
Definition | df-ome 46445* | Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))} | ||
Syntax | ccaragen 46446 | Extend class notation with a function that takes an outer measure and generates a sigma-algebra and a measure. |
class CaraGen | ||
Definition | df-caragen 46447* | Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}) | ||
Theorem | caragenval 46448* | The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑂 ∈ OutMeas → (CaraGen‘𝑂) = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)}) | ||
Theorem | isome 46449* | Express the predicate "𝑂 is an outer measure." Definition 113A of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^‘(𝑂 ↾ 𝑦)))))) | ||
Theorem | caragenel 46450* | Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)))) | ||
Theorem | omef 46451 | An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 ⇒ ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) | ||
Theorem | ome0 46452 | The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) ⇒ ⊢ (𝜑 → (𝑂‘∅) = 0) | ||
Theorem | omessle 46453 | The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐵 ⊆ 𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ≤ (𝑂‘𝐵)) | ||
Theorem | omedm 46454 | The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑂 ∈ OutMeas → dom 𝑂 = 𝒫 ∪ dom 𝑂) | ||
Theorem | caragensplit 46455 | If 𝐸 is in the set generated by the Caratheodory's method, then it splits any set 𝐴 in two parts such that the sum of the outer measures of the two parts is equal to the outer measure of the whole set 𝐴. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸))) = (𝑂‘𝐴)) | ||
Theorem | caragenelss 46456 | An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ 𝑋 = ∪ dom 𝑂 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑋) | ||
Theorem | carageneld 46457* | Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Theorem | omecl 46458 | The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | caragenss 46459 | The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the domain of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) | ||
Theorem | omeunile 46460 | The outer measure of the union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ (𝜑 → 𝑌 ≼ ω) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌))) | ||
Theorem | caragen0 46461 | The empty set belongs to any Caratheodory's construction. First part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑆) | ||
Theorem | omexrcl 46462 | The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ*) | ||
Theorem | caragenunidm 46463 | The base set of an outer measure belongs to the sigma-algebra generated by the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑆) | ||
Theorem | caragensspw 46464 | The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the power set of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝒫 𝑋) | ||
Theorem | omessre 46465 | If the outer measure of a set is real, then the outer measure of any of its subset is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑂‘𝐵) ∈ ℝ) | ||
Theorem | caragenuni 46466 | The base set of the sigma-algebra generated by the Caratheodory's construction is the whole base set of the original outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → ∪ 𝑆 = ∪ dom 𝑂) | ||
Theorem | caragenuncllem 46467 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) +𝑒 (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹)))) = (𝑂‘𝐴)) | ||
Theorem | caragenuncl 46468 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | caragendifcl 46469 | The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | caragenfiiuncl 46470* | The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | omeunle 46471 | The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝐵 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘(𝐴 ∪ 𝐵)) ≤ ((𝑂‘𝐴) +𝑒 (𝑂‘𝐵))) | ||
Theorem | omeiunle 46472* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | omelesplit 46473 | The outer measure of a set 𝐴 is less than or equal to the extended addition of the outer measures of the decomposition induced on 𝐴 by any 𝐸. Step (a) in the proof of Caratheodory's Method, Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸)))) | ||
Theorem | omeiunltfirp 46474* | If the outer measure of a countable union is not +∞, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) & ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐸‘𝑛)) + 𝑌)) | ||
Theorem | omeiunlempt 46475* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐸 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 𝐸) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘𝐸)))) | ||
Theorem | carageniuncllem1 46476* | The outer measure of 𝐴 ∩ (𝐺‘𝑛) is the sum of the outer measures of 𝐴 ∩ (𝐹‘𝑚). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾)))) | ||
Theorem | carageniuncllem2 46477* | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)) | ||
Theorem | carageniuncl 46478* | The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆) | ||
Theorem | caragenunicl 46479 | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝑋 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑋 ∈ 𝑆) | ||
Theorem | caragensal 46480 | Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | caratheodorylem1 46481* | Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛)) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | caratheodorylem2 46482* | Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸:ℕ⟶𝑆) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) & ⊢ 𝐺 = (𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | caratheodory 46483 | Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → (𝑂 ↾ 𝑆) ∈ Meas) | ||
Theorem | 0ome 46484* | The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0) ⇒ ⊢ (𝜑 → 𝑂 ∈ OutMeas) | ||
Theorem | isomenndlem 46485* | 𝑂 is sub-additive w.r.t. countable indexed union, implies that 𝑂 is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑂‘∅) = 0) & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) & ⊢ (𝜑 → 𝐵 ⊆ ℕ) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌) & ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌))) | ||
Theorem | isomennd 46486* | Sufficient condition to prove that 𝑂 is an outer measure. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑂‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) & ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ⇒ ⊢ (𝜑 → 𝑂 ∈ OutMeas) | ||
Theorem | caragenel2d 46487* | Membership in the Caratheodory's construction. Similar to carageneld 46457, but here "less then or equal to" is used, instead of equality. This is Remark 113D of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) ≤ (𝑂‘𝑎)) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Theorem | omege0 46488 | If the outer measure of a set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 0 ≤ (𝑂‘𝐴)) | ||
Theorem | omess0 46489 | If the outer measure of a set is 0, then the outer measure of its subsets is 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) = 0) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑂‘𝐵) = 0) | ||
Theorem | caragencmpl 46490 | A measure built with the Caratheodory's construction is complete. See Definition 112Df of [Fremlin1] p. 19. This is Exercise 113Xa of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐸 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐸) = 0) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Proofs for most of the theorems in section 115 of [Fremlin1] | ||
Syntax | covoln 46491 | Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers. |
class voln* | ||
Definition | df-ovoln 46492* | Define the outer measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))) | ||
Syntax | cvoln 46493 | Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers. |
class voln | ||
Definition | df-voln 46494 | Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))) | ||
Theorem | vonval 46495 | Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln‘𝑋) = ((voln*‘𝑋) ↾ (CaraGen‘(voln*‘𝑋)))) | ||
Theorem | ovnval 46496* | Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln*‘𝑋) = (𝑦 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))) | ||
Theorem | elhoi 46497* | Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑌 ∈ ((𝐴[,)𝐵) ↑m 𝑋) ↔ (𝑌:𝑋⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 (𝑌‘𝑥) ∈ (𝐴[,)𝐵)))) | ||
Theorem | icoresmbl 46498 | A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ran ([,) ↾ (ℝ × ℝ)) ⊆ dom vol | ||
Theorem | hoissre 46499* | The projection of a half-open interval onto a single dimension is a subset of ℝ. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ 𝐼)‘𝑘) ⊆ ℝ) | ||
Theorem | ovnval2 46500* | Value of the Lebesgue outer measure of a subset 𝐴 of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |