mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ spectrum ℝ≥0 a ⊆ s
⊢ ⇑(algebraMap ℝ≥0 ℝ) '' spectrum ℝ≥0 a ⊆ NNReal.toReal '' s

Tactic:
]

Goal state after:
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ spectrum ℝ≥0 a ⊆ s
⊢ ⇑(algebraMap ℝ≥0 ℝ) '' spectrum ℝ≥0 a ⊆ NNReal.toReal '' s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ star (star ⟪x + y, z⟫) = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ star (star ⟪x + y, z⟫) = ⟪x, z⟫ + ⟪y, z⟫
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ star (↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ star (↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * star (sqrt ↑b⁻¹ * sqrt ↑a)‖ ≤ 1

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * star (sqrt ↑b⁻¹ * sqrt ↑a)‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ star (star ↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ star (star ↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑b⁻¹ * sqrt ↑a * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑b⁻¹ * sqrt ↑a * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive ↑a
hab : ↑a ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive ↑a
hab : ↑a ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a
⊢ ↑a⁻¹ ≤ 1

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a
⊢ ↑a⁻¹ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ ↑⋯.unit⁻¹ ≤ ↑⋯.unit⁻¹

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ ↑⋯.unit⁻¹ ≤ ↑⋯.unit⁻¹
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
hx : x ∈ spectrum ℂ ↑a
⊢ 0 ≤ x

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
hx : x ∈ spectrum ℂ ↑a
⊢ 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul A E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
H : x = 0
⊢ False

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul A E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
H : x = 0
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
hb : 0 ≤ b
⊢ a ≤ b

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
hb : 0 ≤ b
⊢ a ≤ b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ ↑(star a * b * a) ≤ ↑(‖b‖ • (star a * a))

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ ↑(star a * b * a) ≤ ↑(‖b‖ • (star a * a))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed (Unitization.inr '' {a | 0 ≤ a})

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed (Unitization.inr '' {a | 0 ≤ a})
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ ‖⟪x, x⟫_A‖ •> (a * star a) = ‖⟪x, x⟫_A‖ •> (a * star a)

pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤ ‖⟪x, x⟫_A‖

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤ ‖⟪x, x⟫_A‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
this : cfcₙ f = fun x ↦ 0
⊢ ConvexOn ℝ s fun x ↦ 0

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
this : cfcₙ f = fun x ↦ 0
⊢ ConvexOn ℝ s fun x ↦ 0
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ ‖x‖ ^ 2 •> (a * star a) = ‖x‖ ^ 2 •> (a * star a)

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
this✝ : cfcₙ f = fun x ↦ 0
this : Convex ℝ s
⊢ Convex ℝ s

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
this✝ : cfcₙ f = fun x ↦ 0
this : Convex ℝ s
⊢ Convex ℝ s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
x✝ : A
⊢ cfc f ↑x✝ = cfc f ↑x✝

Tactic:
]

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, a n ∈ {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
]

Goal state after:
X : Type u_1
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, a n ∈ {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: case inr
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
h₁ : ⟪x, y⟫_A * ⟪y, x⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
]

Goal state after:
case inr
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
h₁ : ⟪x, y⟫_A * ⟪y, x⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x

Tactic:
]

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖ = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖

Tactic:
]

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfc f (a x)) t x

Tactic:
]

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfc f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
h₃ : ConvexOn ℝ s (cfc f ∘ ⇑inrl)
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x

Tactic:
]

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
h₃ : ConvexOn ℝ s (cfc f ∘ ⇑inrl)
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A

Tactic:
]

Goal state after:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc f)
⊢ ConcaveOn ℝ s (-cfcₙ (-f))

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc f)
⊢ ConcaveOn ℝ s (-cfcₙ (-f))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc f)
⊢ ConvexOn ℝ (inr '' s) (-cfc f)

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc f)
⊢ ConvexOn ℝ (inr '' s) (-cfc f)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ ↑x → (‖↑x‖ ≤ 1 ↔ ↑x ≤ 1)

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ ↑x → (‖↑x‖ ≤ 1 ↔ ↑x ≤ 1)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) = 0

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ cfc (fun x ↦ x ^ n) a

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ cfc (fun x ↦ x ^ n) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m