![]() |
Metamath
Proof Explorer Theorem List (p. 332 of 475) | < 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-30034) |
![]() (30035-31557) |
![]() (31558-47500) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sxbrsigalem0 33101* | The closed half-spaces of (ℝ × ℝ) cover (ℝ × ℝ). (Contributed by Thierry Arnoux, 11-Oct-2017.) |
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) = (ℝ × ℝ) | ||
Theorem | sxbrsigalem3 33102* | The sigma-algebra generated by the closed half-spaces of (ℝ × ℝ) is a subset of the sigma-algebra generated by the closed sets of (ℝ × ℝ). (Contributed by Thierry Arnoux, 11-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ⊆ (sigaGen‘(Clsd‘(𝐽 ×t 𝐽))) | ||
Theorem | dya2iocival 33103* | The function 𝐼 returns closed-below open-above dyadic rational intervals covering the real line. This is the same construction as in dyadmbl 25046. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ⇒ ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) = ((𝑋 / (2↑𝑁))[,)((𝑋 + 1) / (2↑𝑁)))) | ||
Theorem | dya2iocress 33104* | Dyadic intervals are subsets of ℝ. (Contributed by Thierry Arnoux, 18-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ⇒ ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) ⊆ ℝ) | ||
Theorem | dya2iocbrsiga 33105* | Dyadic intervals are Borel sets of ℝ. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ⇒ ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) ∈ 𝔅ℝ) | ||
Theorem | dya2icobrsiga 33106* | Dyadic intervals are Borel sets of ℝ. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 13-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ⇒ ⊢ ran 𝐼 ⊆ 𝔅ℝ | ||
Theorem | dya2icoseg 33107* | For any point and any closed-below, open-above interval of ℝ centered on that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑁 = (⌊‘(1 − (2 logb 𝐷))) ⇒ ⊢ ((𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝐷)(,)(𝑋 + 𝐷)))) | ||
Theorem | dya2icoseg2 33108* | For any point and any open interval of ℝ containing that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 12-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ⇒ ⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) | ||
Theorem | dya2iocrfn 33109* | The function returning dyadic square covering for a given size has domain (ran 𝐼 × ran 𝐼). (Contributed by Thierry Arnoux, 19-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ 𝑅 Fn (ran 𝐼 × ran 𝐼) | ||
Theorem | dya2iocct 33110* | The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017.) (Revised by Thierry Arnoux, 11-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ ran 𝑅 ≼ ω | ||
Theorem | dya2iocnrect 33111* | For any point of an open rectangle in (ℝ × ℝ), there is a closed-below open-above dyadic rational square which contains that point and is included in the rectangle. (Contributed by Thierry Arnoux, 12-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) & ⊢ 𝐵 = ran (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓)) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) | ||
Theorem | dya2iocnei 33112* | For any point of an open set of the usual topology on (ℝ × ℝ) there is a closed-below open-above dyadic rational square which contains that point and is entirely in the open set. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) | ||
Theorem | dya2iocuni 33113* | Every open set of (ℝ × ℝ) is a union of closed-below open-above dyadic rational rectangular subsets of (ℝ × ℝ). This union must be a countable union by dya2iocct 33110. (Contributed by Thierry Arnoux, 18-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ (𝐴 ∈ (𝐽 ×t 𝐽) → ∃𝑐 ∈ 𝒫 ran 𝑅∪ 𝑐 = 𝐴) | ||
Theorem | dya2iocucvr 33114* | The dyadic rectangular set collection covers (ℝ × ℝ). (Contributed by Thierry Arnoux, 18-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ ∪ ran 𝑅 = (ℝ × ℝ) | ||
Theorem | sxbrsigalem1 33115* | The Borel algebra on (ℝ × ℝ) is a subset of the sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ). This is a step of the proof of Proposition 1.1.5 of [Cohn] p. 4. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (sigaGen‘ran 𝑅) | ||
Theorem | sxbrsigalem2 33116* | The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ) is a subset of the sigma-algebra generated by the closed half-spaces of (ℝ × ℝ). The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ (sigaGen‘ran 𝑅) ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) | ||
Theorem | sxbrsigalem4 33117* | The Borel algebra on (ℝ × ℝ) is generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ). Proposition 1.1.5 of [Cohn] p. 4 . Note that the interval used in this formalization are closed-below, open-above instead of open-below, closed-above in the proof as they are ultimately generated by the floor function. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ (sigaGen‘(𝐽 ×t 𝐽)) = (sigaGen‘ran 𝑅) | ||
Theorem | sxbrsigalem5 33118* | First direction for sxbrsiga 33120. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 11-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) & ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) ⇒ ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (𝔅ℝ ×s 𝔅ℝ) | ||
Theorem | sxbrsigalem6 33119 | First direction for sxbrsiga 33120, same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (𝔅ℝ ×s 𝔅ℝ) | ||
Theorem | sxbrsiga 33120 | The product sigma-algebra (𝔅ℝ ×s 𝔅ℝ) is the Borel algebra on (ℝ × ℝ) See example 5.1.1 of [Cohn] p. 143 . (Contributed by Thierry Arnoux, 10-Oct-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝔅ℝ ×s 𝔅ℝ) = (sigaGen‘(𝐽 ×t 𝐽)) | ||
In this section, we define a function toOMeas which constructs an outer measure, from a pre-measure 𝑅. An explicit generic definition of an outer measure is not given. It consists of the three following statements: - the outer measure of an empty set is zero (oms0 33127) - it is monotone (omsmon 33128) - it is countably sub-additive (omssubadd 33130) See Definition 1.11.1 of [Bogachev] p. 41. | ||
Syntax | coms 33121 | Class declaration for the outer measure construction function. |
class toOMeas | ||
Definition | df-oms 33122* | Define a function constructing an outer measure. See omsval 33123 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < ))) | ||
Theorem | omsval 33123* | Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝑅 ∈ V → (toOMeas‘𝑅) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ))) | ||
Theorem | omsfval 33124* | Value of the outer measure evaluated for a given set 𝐴. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )) | ||
Theorem | omscl 33125* | A closure lemma for the constructed outer measure. (Contributed by Thierry Arnoux, 17-Sep-2019.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ⊆ (0[,]+∞)) | ||
Theorem | omsf 33126 | A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 ∪ dom 𝑅⟶(0[,]+∞)) | ||
Theorem | oms0 33127 | A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ 𝑀 = (toOMeas‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) & ⊢ (𝜑 → ∅ ∈ dom 𝑅) & ⊢ (𝜑 → (𝑅‘∅) = 0) ⇒ ⊢ (𝜑 → (𝑀‘∅) = 0) | ||
Theorem | omsmon 33128 | A constructed outer measure is monotone. Note in Example 1.5.2 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ 𝑀 = (toOMeas‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑄) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵)) | ||
Theorem | omssubaddlem 33129* | For any small margin 𝐸, we can find a covering approaching the outer measure of a set 𝐴 by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ 𝑀 = (toOMeas‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑄) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸)) | ||
Theorem | omssubadd 33130* | A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ 𝑀 = (toOMeas‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄) & ⊢ (𝜑 → 𝑋 ≼ ω) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) | ||
Syntax | ccarsg 33131 | Class declaration for the Caratheodory sigma-Algebra construction. |
class toCaraSiga | ||
Definition | df-carsg 33132* | Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 33133 for its value. Definition 1.11.2 of [Bogachev] p. 41. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)}) | ||
Theorem | carsgval 33133* | Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) | ||
Theorem | carsgcl 33134 | Closure of the Caratheodory measurable sets. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (toCaraSiga‘𝑀) ⊆ 𝒫 𝑂) | ||
Theorem | elcarsg 33135* | Property of being a Caratheodory measurable set. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (toCaraSiga‘𝑀) ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)))) | ||
Theorem | baselcarsg 33136 | The universe set, 𝑂, is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) ⇒ ⊢ (𝜑 → 𝑂 ∈ (toCaraSiga‘𝑀)) | ||
Theorem | 0elcarsg 33137 | The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) ⇒ ⊢ (𝜑 → ∅ ∈ (toCaraSiga‘𝑀)) | ||
Theorem | carsguni 33138 | The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) ⇒ ⊢ (𝜑 → ∪ (toCaraSiga‘𝑀) = 𝑂) | ||
Theorem | elcarsgss 33139 | Caratheodory measurable sets are subsets of the universe. (Contributed by Thierry Arnoux, 21-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑂) | ||
Theorem | difelcarsg 33140 | The Caratheodory measurable sets are closed under complement. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → (𝑂 ∖ 𝐴) ∈ (toCaraSiga‘𝑀)) | ||
Theorem | inelcarsg 33141* | The Caratheodory measurable sets are closed under intersection. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀)) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂) → (𝑀‘(𝑎 ∪ 𝑏)) ≤ ((𝑀‘𝑎) +𝑒 (𝑀‘𝑏))) & ⊢ (𝜑 → 𝐵 ∈ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ (toCaraSiga‘𝑀)) | ||
Theorem | unelcarsg 33142* | The Caratheodory-measurable sets are closed under pairwise unions. (Contributed by Thierry Arnoux, 21-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀)) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂) → (𝑀‘(𝑎 ∪ 𝑏)) ≤ ((𝑀‘𝑎) +𝑒 (𝑀‘𝑏))) & ⊢ (𝜑 → 𝐵 ∈ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ (toCaraSiga‘𝑀)) | ||
Theorem | difelcarsg2 33143* | The Caratheodory-measurable sets are closed under class difference. (Contributed by Thierry Arnoux, 30-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀)) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂) → (𝑀‘(𝑎 ∪ 𝑏)) ≤ ((𝑀‘𝑎) +𝑒 (𝑀‘𝑏))) & ⊢ (𝜑 → 𝐵 ∈ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ (toCaraSiga‘𝑀)) | ||
Theorem | carsgmon 33144* | Utility lemma: Apply monotony. (Contributed by Thierry Arnoux, 29-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝑂) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵)) | ||
Theorem | carsgsigalem 33145* | Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) ⇒ ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∪ 𝑓)) ≤ ((𝑀‘𝑒) +𝑒 (𝑀‘𝑓))) | ||
Theorem | fiunelcarsg 33146* | The Caratheodory measurable sets are closed under finite union. (Contributed by Thierry Arnoux, 23-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ (toCaraSiga‘𝑀)) | ||
Theorem | carsgclctunlem1 33147* | Lemma for carsgclctun 33151. (Contributed by Thierry Arnoux, 23-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂) ⇒ ⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦))) | ||
Theorem | carsggect 33148* | The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ (𝜑 → ¬ ∅ ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) ⇒ ⊢ (𝜑 → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ (𝑀‘∪ 𝐴)) | ||
Theorem | carsgclctunlem2 33149* | Lemma for carsgclctun 33151. (Contributed by Thierry Arnoux, 25-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) & ⊢ (𝜑 → Disj 𝑘 ∈ ℕ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (toCaraSiga‘𝑀)) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂) & ⊢ (𝜑 → (𝑀‘𝐸) ≠ +∞) ⇒ ⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴))) ≤ (𝑀‘𝐸)) | ||
Theorem | carsgclctunlem3 33150* | Lemma for carsgclctun 33151. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) & ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂) ⇒ ⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) | ||
Theorem | carsgclctun 33151* | The Caratheodory measurable sets are closed under countable union. (Contributed by Thierry Arnoux, 21-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) & ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ (toCaraSiga‘𝑀)) | ||
Theorem | carsgsiga 33152* | The Caratheodory measurable sets constructed from outer measures form a Sigma-algebra. Statement (iii) of Theorem 1.11.4 of [Bogachev] p. 42. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) ⇒ ⊢ (𝜑 → (toCaraSiga‘𝑀) ∈ (sigAlgebra‘𝑂)) | ||
Theorem | omsmeas 33153 | The restriction of a constructed outer measure to Caratheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020.) |
⊢ 𝑀 = (toOMeas‘𝑅) & ⊢ 𝑆 = (toCaraSiga‘𝑀) & ⊢ (𝜑 → 𝑄 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) & ⊢ (𝜑 → ∅ ∈ dom 𝑅) & ⊢ (𝜑 → (𝑅‘∅) = 0) ⇒ ⊢ (𝜑 → (𝑀 ↾ 𝑆) ∈ (measures‘𝑆)) | ||
Theorem | pmeasmono 33154* | This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑃‘∅) = 0) & ⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦)) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝑅) & ⊢ (𝜑 → (𝐵 ∖ 𝐴) ∈ 𝑅) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) | ||
Theorem | pmeasadd 33155* | A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑃‘∅) = 0) & ⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦)) & ⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} & ⊢ (𝜑 → 𝑅 ∈ 𝑄) & ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑅) & ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (𝑃‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ*𝑘 ∈ 𝐴(𝑃‘𝐵)) | ||
Theorem | itgeq12dv 33156* | Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥) | ||
Syntax | citgm 33157 | Extend class notation with the (measure) Bochner integral. |
class itgm | ||
Syntax | csitm 33158 | Extend class notation with the integral metric for simple functions. |
class sitm | ||
Syntax | csitg 33159 | Extend class notation with the integral of simple functions. |
class sitg | ||
Definition | df-sitg 33160* |
Define the integral of simple functions from a measurable space
dom 𝑚 to a generic space 𝑤
equipped with the right scalar
product. 𝑤 will later be required to be a Banach
space.
These simple functions are required to take finitely many different values: this is expressed by ran 𝑔 ∈ Fin in the definition. Moreover, for each 𝑥, the pre-image (◡𝑔 “ {𝑥}) is requested to be measurable, of finite measure. In this definition, (sigaGen‘(TopOpen‘𝑤)) is the Borel sigma-algebra on 𝑤, and the functions 𝑔 range over the measurable functions over that Borel algebra. Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.) |
⊢ sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))))) | ||
Definition | df-sitm 33161* | Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in ℝ*, the range structure for this integral is (ℝ*𝑠 ↾s (0[,]+∞)). See definition 2.3.1 of [Bogachev] p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ sitm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))) | ||
Theorem | sitgval 33162* | Value of the simple function integral builder for a given space 𝑊 and measure 𝑀. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) ⇒ ⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) | ||
Theorem | issibf 33163* | The predicate "𝐹 is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) | ||
Theorem | sibf0 33164 | The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → 𝑊 ∈ Mnd) ⇒ ⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀)) | ||
Theorem | sibfmbl 33165 | A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) | ||
Theorem | sibff 33166 | A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝐽) | ||
Theorem | sibfrn 33167 | A simple function has finite range. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ Fin) | ||
Theorem | sibfima 33168 | Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝐴})) ∈ (0[,)+∞)) | ||
Theorem | sibfinima 33169 | The measure of the intersection of any two preimages by simple functions is a real number. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → 𝐽 ∈ Fre) ⇒ ⊢ (((𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺) ∧ (𝑋 ≠ 0 ∨ 𝑌 ≠ 0 )) → (𝑀‘((◡𝐹 “ {𝑋}) ∩ (◡𝐺 “ {𝑌}))) ∈ (0[,)+∞)) | ||
Theorem | sibfof 33170 | Applying function operations on simple functions results in simple functions with regard to the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ 𝐶 = (Base‘𝐾) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝐾 ∈ TopSp) & ⊢ (𝜑 → 𝐽 ∈ Fre) & ⊢ (𝜑 → ( 0 + 0 ) = (0g‘𝐾)) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀)) | ||
Theorem | sitgfval 33171* | Value of the Bochner integral for a simple function 𝐹. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) | ||
Theorem | sitgclg 33172* | Closure of the Bochner integral on simple functions, generic version. See sitgclbn 33173 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.) (Proof shortened by AV, 12-Dec-2019.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ 𝐺 = (Scalar‘𝑊) & ⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt ) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) | ||
Theorem | sitgclbn 33173 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝑊 ∈ Ban) & ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt ) ⇒ ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) | ||
Theorem | sitgclcn 33174 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝑊 ∈ Ban) & ⊢ (𝜑 → (Scalar‘𝑊) = ℂfld) ⇒ ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) | ||
Theorem | sitgclre 33175 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝑊 ∈ Ban) & ⊢ (𝜑 → (Scalar‘𝑊) = ℝfld) ⇒ ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) | ||
Theorem | sitg0 33176 | The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → 𝑊 ∈ Mnd) ⇒ ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = 0 ) | ||
Theorem | sitgf 33177* | The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ ((𝜑 ∧ 𝑓 ∈ dom (𝑊sitg𝑀)) → ((𝑊sitg𝑀)‘𝑓) ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊sitg𝑀):dom (𝑊sitg𝑀)⟶𝐵) | ||
Theorem | sitgaddlemb 33178 | Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑆 = (sigaGen‘𝐽) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈ SLMod) & ⊢ (𝜑 → 𝐽 ∈ Fre) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt ) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd ‘𝑝)) ∈ 𝐵) | ||
Theorem | sitmval 33179* | Value of the simple function integral metric for a given space 𝑊 and measure 𝑀. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ 𝐷 = (dist‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) ⇒ ⊢ (𝜑 → (𝑊sitm𝑀) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔)))) | ||
Theorem | sitmfval 33180 | Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ 𝐷 = (dist‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) = (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺))) | ||
Theorem | sitmcl 33181 | Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
⊢ (𝜑 → 𝑊 ∈ Mnd) & ⊢ (𝜑 → 𝑊 ∈ ∞MetSp) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) & ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) & ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) ⇒ ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞)) | ||
Theorem | sitmf 33182 | The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
⊢ (𝜑 → 𝑊 ∈ Mnd) & ⊢ (𝜑 → 𝑊 ∈ ∞MetSp) & ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) ⇒ ⊢ (𝜑 → (𝑊sitm𝑀):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞)) | ||
Definition | df-itgm 33183* |
Define the Bochner integral as the extension by continuity of the
Bochnel integral for simple functions.
Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric (𝑤sitm𝑚). He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 25069. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
⊢ itgm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚))) | ||
Theorem | oddpwdc 33184* | Lemma for eulerpart 33212. The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) |
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) ⇒ ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ | ||
Theorem | oddpwdcv 33185* | Lemma for eulerpart 33212: value of the 𝐹 function. (Contributed by Thierry Arnoux, 9-Sep-2017.) |
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) ⇒ ⊢ (𝑊 ∈ (𝐽 × ℕ0) → (𝐹‘𝑊) = ((2↑(2nd ‘𝑊)) · (1st ‘𝑊))) | ||
Theorem | eulerpartlemsv1 33186* | Lemma for eulerpart 33212. Value of the sum of a partition 𝐴. (Contributed by Thierry Arnoux, 26-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) | ||
Theorem | eulerpartlemelr 33187* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin)) | ||
Theorem | eulerpartlemsv2 33188* | Lemma for eulerpart 33212. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) | ||
Theorem | eulerpartlemsf 33189* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ 𝑆:((ℕ0 ↑m ℕ) ∩ 𝑅)⟶ℕ0 | ||
Theorem | eulerpartlems 33190* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ 𝑡 ∈ (ℤ≥‘((𝑆‘𝐴) + 1))) → (𝐴‘𝑡) = 0) | ||
Theorem | eulerpartlemsv3 33191* | Lemma for eulerpart 33212. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (1...(𝑆‘𝐴))((𝐴‘𝑘) · 𝑘)) | ||
Theorem | eulerpartlemgc 33192* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 9-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ≤ (𝑆‘𝐴)) | ||
Theorem | eulerpartleme 33193* | Lemma for eulerpart 33212. (Contributed by Mario Carneiro, 26-Jan-2015.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} ⇒ ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘) = 𝑁)) | ||
Theorem | eulerpartlemv 33194* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 19-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} ⇒ ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) | ||
Theorem | eulerpartlemo 33195* | Lemma for eulerpart 33212: 𝑂 is the set of odd partitions of 𝑁. (Contributed by Thierry Arnoux, 10-Aug-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} ⇒ ⊢ (𝐴 ∈ 𝑂 ↔ (𝐴 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛)) | ||
Theorem | eulerpartlemd 33196* | Lemma for eulerpart 33212: 𝐷 is the set of distinct part. of 𝑁. (Contributed by Thierry Arnoux, 11-Aug-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ (𝐴 “ ℕ) ⊆ {0, 1})) | ||
Theorem | eulerpartlem1 33197* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ⇒ ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) | ||
Theorem | eulerpartlemb 33198* | Lemma for eulerpart 33212. The set of all partitions of 𝑁 is finite. (Contributed by Mario Carneiro, 26-Jan-2015.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ⇒ ⊢ 𝑃 ∈ Fin | ||
Theorem | eulerpartlemt0 33199* | Lemma for eulerpart 33212. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) | ||
Theorem | eulerpartlemf 33200* | Lemma for eulerpart 33212: Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} ⇒ ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |