cfc_id'
theorem cfc_id' :
∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
[inst_2 : MetricSpace R] [inst_3 : TopologicalSemiring R] [inst_4 : ContinuousStar R]
[inst_5 : TopologicalSpace A] [inst_6 : Ring A] [inst_7 : StarRing A] [inst_8 : Algebra R A]
[inst_9 : ContinuousFunctionalCalculus R p] (a : A), autoParam (p a) _auto✝ → cfc (fun x => x) a = a
This theorem, named `cfc_id'`, states that for any type `R` and another type `A` with a property `p`, given multiple conditions - `R` being a Commutative Semiring, a Star Ring, a Metric Space, a Topological Semiring, and having Continuous Star; `A` being a Topological Space, a Ring, and a Star Ring; and `R` and `A` together forming an Algebra with Continuous Functional Calculus for property `p` - for any element `a` of type `A` that satisfies property `p`, the continuous functional calculus of the identity function applied to `a` is `a` itself. This basically means that under these conditions, the continuous functional calculus acts like the identity on elements which satisfy the property `p`. The `autoParam (p a) _auto✝` argument is used for automatic parameter support and does not affect the statement of the theorem in a mathematical sense.
More concisely: If `R` is a Commutative Semiring, a Star Ring, a Metric Space, a Topological Semiring with Continuous Star, `A` is a Topological Space, a Ring, a Star Ring, and `R` and `A` form an Algebra with Continuous Functional Calculus for property `p`, then for any `a` in `A` satisfying property `p`, the continuous functional calculus of the identity function on `a` equals `a`.
|
cfc_comp'
theorem cfc_comp' :
∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
[inst_2 : MetricSpace R] [inst_3 : TopologicalSemiring R] [inst_4 : ContinuousStar R]
[inst_5 : TopologicalSpace A] [inst_6 : Ring A] [inst_7 : StarRing A] [inst_8 : Algebra R A]
[inst_9 : ContinuousFunctionalCalculus R p] [inst_10 : UniqueContinuousFunctionalCalculus R A] (g f : R → R)
(a : A),
autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝ →
autoParam (ContinuousOn f (spectrum R a)) _auto✝¹ →
autoParam (p a) _auto✝² → cfc (fun x => g (f x)) a = cfc g (cfc f a)
This theorem states that for any given commutative semiring `R`, any `A` that is a `R`-algebra, and a predicate `p` on `A`, under certain conditions, the continuous functional calculus of the composition of two functions `g` and `f` at a point `a` is equal to the continuous functional calculus of `g` at the continuous functional calculus of `f` at `a`. The conditions required are that the function `g` is continuous on the image of the spectrum of `a` under `f`, the function `f` is continuous on the spectrum of `a`, and the predicate `p` holds true for `a`. This theorem encapsulates a property of the continuous functional calculus in the context of topological semirings and star rings.
More concisely: For any commutative semiring `R`, `R-algebra `A`, function `f: A -> A` and `g: A -> A` with `g` continuous on the image of the spectrum of `a` under `f`, `f` continuous on the spectrum of `a`, and `p(a)` true, the functional calculus of `g(f(x))` is equal to `g(functional calculus of f(x) at a)` for all `x` satisfying `p(x)`.
|