mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: ι : Type u_2
C : ι → Type u_3
inst✝¹⁴ : (i : ι) → PartialOrder (C i)
inst✝¹³ : (i : ι) → NonUnitalRing (C i)
inst✝¹² : (i : ι) → TopologicalSpace (C i)
inst✝¹¹ : (i : ι) → StarRing (C i)
inst✝¹⁰ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁹ : StarOrderedRing ((i : ι) → C i)
inst✝⁸ : (i : ι) → Module ℝ (C i)
inst✝⁷ : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)
inst✝⁶ : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)
inst✝⁵ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
x : ℝ≥0
hc : ∀ (i : ι), 0 ≤ c i
⊢ nnrpow c x = fun i ↦ cfcₙ (fun x_1 ↦ x_1.nnrpow x) (c i)

Tactic:
unfold nnrpow

Goal state after:
ι : Type u_2
C : ι → Type u_3
inst✝¹⁴ : (i : ι) → PartialOrder (C i)
inst✝¹³ : (i : ι) → NonUnitalRing (C i)
inst✝¹² : (i : ι) → TopologicalSpace (C i)
inst✝¹¹ : (i : ι) → StarRing (C i)
inst✝¹⁰ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁹ : StarOrderedRing ((i : ι) → C i)
inst✝⁸ : (i : ι) → Module ℝ (C i)
inst✝⁷ : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)
inst✝⁶ : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)
inst✝⁵ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
x : ℝ≥0
hc : ∀ (i : ι), 0 ≤ c i
⊢ cfcₙ (fun x_1 ↦ x_1.nnrpow x) c = fun i ↦ cfcₙ (fun x_1 ↦ x_1.nnrpow x) (c i)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: ι : Type u_2
C : ι → Type u_3
inst✝¹⁴ : (i : ι) → PartialOrder (C i)
inst✝¹³ : (i : ι) → NonUnitalRing (C i)
inst✝¹² : (i : ι) → TopologicalSpace (C i)
inst✝¹¹ : (i : ι) → StarRing (C i)
inst✝¹⁰ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁹ : StarOrderedRing ((i : ι) → C i)
inst✝⁸ : (i : ι) → Module ℝ (C i)
inst✝⁷ : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)
inst✝⁶ : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)
inst✝⁵ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
x : ℝ≥0
hc : ∀ (i : ι), 0 ≤ c i
⊢ nnrpow c x = fun i ↦ c i ^ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ sqrt a = a ^ (1 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
⊢ sqrt 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a ^ 2 = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a * sqrt a = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt (a ^ 2) = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt (a * a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
this : cfcₙ (fun x ↦ √x * √x) a = cfcₙ (fun x ↦ x) a
⊢ sqrt a = cfcₙ Real.sqrt a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a = cfcₙ Real.sqrt a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝²⁵ : PartialOrder A
inst✝²⁴ : NonUnitalRing A
inst✝²³ : TopologicalSpace A
inst✝²² : StarRing A
inst✝²¹ : Module ℝ A
inst✝²⁰ : SMulCommClass ℝ A A
inst✝¹⁹ : IsScalarTower ℝ A A
inst✝¹⁸ : StarOrderedRing A
inst✝¹⁷ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹⁶ : NonnegSpectrumClass ℝ A
inst✝¹⁵ : IsSemitopologicalRing A
inst✝¹⁴ : T2Space A
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : StarOrderedRing B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝³ : IsSemitopologicalRing B
inst✝² : T2Space B
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
ha : 0 ≤ a
hb : 0 ≤ b
⊢ sqrt (a, b) = (sqrt a, sqrt b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: ι : Type u_2
C : ι → Type u_3
inst✝¹⁴ : (i : ι) → PartialOrder (C i)
inst✝¹³ : (i : ι) → NonUnitalRing (C i)
inst✝¹² : (i : ι) → TopologicalSpace (C i)
inst✝¹¹ : (i : ι) → StarRing (C i)
inst✝¹⁰ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁹ : StarOrderedRing ((i : ι) → C i)
inst✝⁸ : (i : ι) → Module ℝ (C i)
inst✝⁷ : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)
inst✝⁶ : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)
inst✝⁵ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
hc : ∀ (i : ι), 0 ≤ c i
⊢ sqrt c = fun i ↦ sqrt (c i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∃ x, (∀ (i : Fin 4), 0 ≤ x i) ∧ (∀ (i : Fin 4), ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i, I ^ ↑i • x i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
⊢ Set.range Subtype.val ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MulOneClass α
m : α
⊢ Tendsto (fun x ↦ m * x) (pure 1) (𝓝 m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MulOneClass α
m : α
⊢ Tendsto (fun x ↦ x * m) (pure 1) (𝓝 m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : SeparatelyContinuousMul α
m : α
⊢ Tendsto (fun x ↦ m * x) (𝓝 1) (𝓝 m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : SeparatelyContinuousMul α
m : α
⊢ Tendsto (fun x ↦ x * m) (𝓝 1) (𝓝 m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : SeparatelyContinuousMul α
l : Filter α
hl : l.IsApproximateUnit
⊢ l ≤ 𝓝 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MulOneClass α
inst✝¹ : SeparatelyContinuousMul α
l : Filter α
inst✝ : l.NeBot
⊢ l.IsApproximateUnit ↔ l ≤ 𝓝 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
⊢ [0 ≤ a, a = sqrt a * sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
ha : 0 ≤ a
⊢ a ^ y = cfc (fun x ↦ x ^ y) a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ ContinuousOn id (f '' spectrum ℝ a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ ∀ x ∈ f '' spectrum ℝ a, id x ≠ 0 ∨ 0 ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
hg : ContinuousOn (fun r ↦ r ^ y) (f '' spectrum ℝ a)
⊢ 0 ≤ cfc f a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ cfc f a ^ y = cfc (fun r ↦ f r ^ y) a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ a ^ 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : ℝ
⊢ 1 ^ x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ a ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
⊢ Set.EqOn (fun a ↦ a ^ 0) (fun x ↦ 1) (Set.Ici 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
⊢ Tendsto (fun x ↦ cfc (F x) a) l (𝓝 (cfc f a))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : ℝ
hx : x ≠ 0
⊢ rpow 0 x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
n : ℕ
ha : 0 ≤ a
⊢ a ^ ↑n = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : ℝ≥0
y : ℝ
⊢ (algebraMap ℝ≥0 A) x ^ y = (algebraMap ℝ≥0 A) (x ^ y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ContinuousOn (fun x ↦ (ofFun {spectrum R a}) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ContinuousOn (fun x ↦ cfc (f x) a) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
⊢ z ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x y : ℝ
ha : IsUnit a
⊢ a ^ (x + y) = a ^ x * a ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
h_cont : Continuous[inst✝, topologicalSpace R R {spectrum R a}] fun x ↦ (ofFun {spectrum R a}) (f x)
hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)
⊢ Continuous[inst✝, inst✝³] fun x ↦ cfc (f x) a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x) ^ x⁻¹ = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x⁻¹) ^ x = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
by

Goal state after: