Home | Metamath
Proof Explorer Theorem List (p. 324 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pmeasadd 32301* | 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 32302* | Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥) | ||
Syntax | citgm 32303 | Extend class notation with the (measure) Bochner integral. |
class itgm | ||
Syntax | csitm 32304 | Extend class notation with the integral metric for simple functions. |
class sitm | ||
Syntax | csitg 32305 | Extend class notation with the integral of simple functions. |
class sitg | ||
Definition | df-sitg 32306* |
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 32307* | 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 32308* | 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 32309* | 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 32310 | 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 32311 | 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 32312 | 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 32313 | 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 32314 | 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 32315 | 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 32316 | 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 32317* | 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 32318* | Closure of the Bochner integral on simple functions, generic version. See sitgclbn 32319 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 32319 | 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 32320 | 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 32321 | 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 32322 | 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 32323* | 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 32324 | 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 32325* | 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 32326 | 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 32327 | 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 32328 | 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 32329* |
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 24796. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
⊢ itgm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚))) | ||
Theorem | oddpwdc 32330* | Lemma for eulerpart 32358. 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 32331* | Lemma for eulerpart 32358: value of the 𝐹 function. (Contributed by Thierry Arnoux, 9-Sep-2017.) |
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) ⇒ ⊢ (𝑊 ∈ (𝐽 × ℕ0) → (𝐹‘𝑊) = ((2↑(2nd ‘𝑊)) · (1st ‘𝑊))) | ||
Theorem | eulerpartlemsv1 32332* | Lemma for eulerpart 32358. Value of the sum of a partition 𝐴. (Contributed by Thierry Arnoux, 26-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) | ||
Theorem | eulerpartlemelr 32333* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin)) | ||
Theorem | eulerpartlemsv2 32334* | Lemma for eulerpart 32358. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) | ||
Theorem | eulerpartlemsf 32335* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ 𝑆:((ℕ0 ↑m ℕ) ∩ 𝑅)⟶ℕ0 | ||
Theorem | eulerpartlems 32336* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ 𝑡 ∈ (ℤ≥‘((𝑆‘𝐴) + 1))) → (𝐴‘𝑡) = 0) | ||
Theorem | eulerpartlemsv3 32337* | Lemma for eulerpart 32358. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (1...(𝑆‘𝐴))((𝐴‘𝑘) · 𝑘)) | ||
Theorem | eulerpartlemgc 32338* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 9-Aug-2018.) |
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ≤ (𝑆‘𝐴)) | ||
Theorem | eulerpartleme 32339* | Lemma for eulerpart 32358. (Contributed by Mario Carneiro, 26-Jan-2015.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} ⇒ ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘) = 𝑁)) | ||
Theorem | eulerpartlemv 32340* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 19-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} ⇒ ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) | ||
Theorem | eulerpartlemo 32341* | Lemma for eulerpart 32358: 𝑂 is the set of odd partitions of 𝑁. (Contributed by Thierry Arnoux, 10-Aug-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} ⇒ ⊢ (𝐴 ∈ 𝑂 ↔ (𝐴 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛)) | ||
Theorem | eulerpartlemd 32342* | Lemma for eulerpart 32358: 𝐷 is the set of distinct part. of 𝑁. (Contributed by Thierry Arnoux, 11-Aug-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ (𝐴 “ ℕ) ⊆ {0, 1})) | ||
Theorem | eulerpartlem1 32343* | Lemma for eulerpart 32358. (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 32344* | Lemma for eulerpart 32358. 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 32345* | Lemma for eulerpart 32358. (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 32346* | Lemma for eulerpart 32358: 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) | ||
Theorem | eulerpartlemt 32347* | Lemma for eulerpart 32358. (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 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) | ||
Theorem | eulerpartgbij 32348* | Lemma for eulerpart 32358: The 𝐺 function is a bijection. (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} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) ⇒ ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) | ||
Theorem | eulerpartlemgv 32349* | Lemma for eulerpart 32358: value of the function 𝐺. (Contributed by Thierry Arnoux, 13-Nov-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))) | ||
Theorem | eulerpartlemr 32350* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 13-Nov-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) ⇒ ⊢ 𝑂 = ((𝑇 ∩ 𝑅) ∩ 𝑃) | ||
Theorem | eulerpartlemmf 32351* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 30-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻) | ||
Theorem | eulerpartlemgvv 32352* | Lemma for eulerpart 32358: value of the function 𝐺 evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) ⇒ ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0)) | ||
Theorem | eulerpartlemgu 32353* | Lemma for eulerpart 32358: Rewriting the 𝑈 set for an odd partition Note that interestingly, this proof reuses marypha2lem2 9204. (Contributed by Thierry Arnoux, 10-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) & ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))}) | ||
Theorem | eulerpartlemgh 32354* | Lemma for eulerpart 32358: The 𝐹 function is a bijection on the 𝑈 subsets. (Contributed by Thierry Arnoux, 15-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) & ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) | ||
Theorem | eulerpartlemgf 32355* | Lemma for eulerpart 32358: Images under 𝐺 have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈ Fin) | ||
Theorem | eulerpartlemgs2 32356* | Lemma for eulerpart 32358: The 𝐺 function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴)) | ||
Theorem | eulerpartlemn 32357* | Lemma for eulerpart 32358. (Contributed by Thierry Arnoux, 30-Aug-2018.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} & ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥)) & ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} & ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) & ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} & ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) & ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) ⇒ ⊢ (𝐺 ↾ 𝑂):𝑂–1-1-onto→𝐷 | ||
Theorem | eulerpart 32358* | Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let 𝑃 be the set of all partitions of 𝑁, represented as multisets of positive integers, which is to say functions from ℕ to ℕ0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals 𝑁. Then the set 𝑂 of all partitions that only consist of odd numbers and the set 𝐷 of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)} & ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} & ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} ⇒ ⊢ (♯‘𝑂) = (♯‘𝐷) | ||
Syntax | csseq 32359 | Sequences defined by strong recursion. |
class seqstr | ||
Definition | df-sseq 32360* | Define a builder for sequences by strong recursion, i.e., by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
⊢ seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0 × {(𝑚 ++ 〈“(𝑓‘𝑚)”〉)}))))) | ||
Theorem | subiwrd 32361 | Lemma for sseqp1 32371. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word 𝑆) | ||
Theorem | subiwrdlen 32362 | Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁) | ||
Theorem | iwrdsplit 32363 | Lemma for sseqp1 32371. (Contributed by Thierry Arnoux, 25-Apr-2019.) (Proof shortened by AV, 14-Oct-2022.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹 ↾ (0..^(𝑁 + 1))) = ((𝐹 ↾ (0..^𝑁)) ++ 〈“(𝐹‘𝑁)”〉)) | ||
Theorem | sseqval 32364* | Value of the strong sequence builder function. The set 𝑊 represents here the words of length greater than or equal to the lenght of the initial sequence 𝑀. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) ⇒ ⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)}))))) | ||
Theorem | sseqfv1 32365 | Value of the strong sequence builder function at one of its initial values. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑀))) ⇒ ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝑀‘𝑁)) | ||
Theorem | sseqfn 32366 | A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) ⇒ ⊢ (𝜑 → (𝑀seqstr𝐹) Fn ℕ0) | ||
Theorem | sseqmw 32367 | Lemma for sseqf 32368 amd sseqp1 32371. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑊) | ||
Theorem | sseqf 32368 | A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.) (Proof shortened by AV, 7-Mar-2022.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) ⇒ ⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆) | ||
Theorem | sseqfres 32369 | The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) ⇒ ⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) = 𝑀) | ||
Theorem | sseqfv2 32370* | Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(♯‘𝑀))) ⇒ ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)}))‘𝑁))) | ||
Theorem | sseqp1 32371 | Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019.) |
⊢ (𝜑 → 𝑆 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ Word 𝑆) & ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀)))) & ⊢ (𝜑 → 𝐹:𝑊⟶𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(♯‘𝑀))) ⇒ ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) | ||
Syntax | cfib 32372 | The Fibonacci sequence. |
class Fibci | ||
Definition | df-fib 32373 | Define the Fibonacci sequence, where that each element is the sum of the two preceding ones, starting from 0 and 1. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ Fibci = (〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) | ||
Theorem | fiblem 32374 | Lemma for fib0 32375, fib1 32376 and fibp1 32377. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))):(Word ℕ0 ∩ (◡♯ “ (ℤ≥‘(♯‘〈“01”〉))))⟶ℕ0 | ||
Theorem | fib0 32375 | Value of the Fibonacci sequence at index 0. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘0) = 0 | ||
Theorem | fib1 32376 | Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘1) = 1 | ||
Theorem | fibp1 32377 | Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (𝑁 ∈ ℕ → (Fibci‘(𝑁 + 1)) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁))) | ||
Theorem | fib2 32378 | Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘2) = 1 | ||
Theorem | fib3 32379 | Value of the Fibonacci sequence at index 3. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘3) = 2 | ||
Theorem | fib4 32380 | Value of the Fibonacci sequence at index 4. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘4) = 3 | ||
Theorem | fib5 32381 | Value of the Fibonacci sequence at index 5. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘5) = 5 | ||
Theorem | fib6 32382 | Value of the Fibonacci sequence at index 6. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
⊢ (Fibci‘6) = 8 | ||
Syntax | cprb 32383 | Extend class notation to include the class of probability measures. |
class Prob | ||
Definition | df-prob 32384 | Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.) |
⊢ Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1} | ||
Theorem | elprob 32385 | The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
⊢ (𝑃 ∈ Prob ↔ (𝑃 ∈ ∪ ran measures ∧ (𝑃‘∪ dom 𝑃) = 1)) | ||
Theorem | domprobmeas 32386 | A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
⊢ (𝑃 ∈ Prob → 𝑃 ∈ (measures‘dom 𝑃)) | ||
Theorem | domprobsiga 32387 | The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
⊢ (𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra) | ||
Theorem | probtot 32388 | The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) | ||
Theorem | prob01 32389 | A probability is an element of [ 0 , 1 ]. First axiom of Kolmogorov. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘𝐴) ∈ (0[,]1)) | ||
Theorem | probnul 32390 | The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝑃 ∈ Prob → (𝑃‘∅) = 0) | ||
Theorem | unveldomd 32391 | The universe is an element of the domain of the probability, the universe (entire probability space) being ∪ dom 𝑃 in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) | ||
Theorem | unveldom 32392 | The universe is an element of the domain of the probability, the universe (entire probability space) being ∪ dom 𝑃 in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
⊢ (𝑃 ∈ Prob → ∪ dom 𝑃 ∈ dom 𝑃) | ||
Theorem | nuleldmp 32393 | The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
⊢ (𝑃 ∈ Prob → ∅ ∈ dom 𝑃) | ||
Theorem | probcun 32394* | The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the Σ construct cannot be used as it can handle infinite indexing set only if they are subsets of ℤ, which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ 𝒫 dom 𝑃 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑃‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑃‘𝑥)) | ||
Theorem | probun 32395 | The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((𝐴 ∩ 𝐵) = ∅ → (𝑃‘(𝐴 ∪ 𝐵)) = ((𝑃‘𝐴) + (𝑃‘𝐵)))) | ||
Theorem | probdif 32396 | The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (𝑃‘(𝐴 ∖ 𝐵)) = ((𝑃‘𝐴) − (𝑃‘(𝐴 ∩ 𝐵)))) | ||
Theorem | probinc 32397 | A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ 𝐴 ⊆ 𝐵) → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) | ||
Theorem | probdsb 32398 | The probability of the complement of a set. That is, the probability that the event 𝐴 does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘(∪ dom 𝑃 ∖ 𝐴)) = (1 − (𝑃‘𝐴))) | ||
Theorem | probmeasd 32399 | A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → 𝑃 ∈ ∪ ran measures) | ||
Theorem | probvalrnd 32400 | The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑃) ⇒ ⊢ (𝜑 → (𝑃‘𝐴) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |