-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive. -/
lemma nnnorm_apply_le (φ : F) (a : A) : ‖φ a‖₊ ≤ ‖a‖₊

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
⊢ ‖φ a‖₊ ≤ ‖a‖₊

Tactic:
have h (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A) :
    ‖ψ x‖₊ ≤ ‖x‖₊ := by
  suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
    refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
    simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
    exact this <| .star_mul_self x
  intro s hs
  suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
    rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
      at this
  exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
h : ∀ (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A), ‖ψ x‖₊ ≤ ‖x‖₊
⊢ ‖φ a‖₊ ≤ ‖a‖₊

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
⊢ ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊

Tactic:
intro s hs

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ ‖ψ s‖₊ ≤ ‖s‖₊

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
⊢ ‖ψ x‖₊ ≤ ‖x‖₊

Tactic:
suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
  refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
  simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
  exact this <| .star_mul_self x

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
⊢ ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ ≤ ‖x‖₊

Tactic:
refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ * ‖ψ x‖₊ ≤ ‖x‖₊ * ‖x‖₊

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ x‖₊ * ‖ψ x‖₊ ≤ ‖x‖₊ * ‖x‖₊

Tactic:
simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ (x⋆ * x)‖₊ ≤ ‖x⋆ * x‖₊

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s
⊢ ‖ψ s‖₊ ≤ ‖s‖₊

Tactic:
rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
  at this

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ ‖ψ s‖₊ ≤ ‖s‖₊

Tactic:
suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
  rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
    at this

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
h : ∀ (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A), ‖ψ x‖₊ ≤ ‖x‖₊
⊢ ‖φ a‖₊ ≤ ‖a‖₊

Tactic:
simpa [nnnorm_inr] using h (starLift (inrNonUnitalStarAlgHom ℂ B |>.comp (φ : A →⋆ₙₐ[ℂ] B))) a

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x : Unitization ℂ A
this : ∀ {s : Unitization ℂ A}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
⊢ ‖ψ (x⋆ * x)‖₊ ≤ ‖x⋆ * x‖₊

Tactic:
exact this <| .star_mul_self x

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s

Tactic:
exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)

Result:
no goals