awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
obtain :
  ∀ (x : ℝ) (hx : IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) x),
    IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖

Tactic:
obtain ⟨x, hx⟩ := NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum a
      |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
      (quasispectrum.nonempty 𝕜 a).image _

Premises used: quasispectrum.nonempty, Set.Nonempty.image, IsCompact.image_of_continuousOn, NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum, ContinuousOn.norm, IsCompact.exists_isGreatest
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : ℝ
hx : IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) x
obtain :
  ∀ (x : 𝕜) (hx' : x ∈ σₙ 𝕜 a) (hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)),
    IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖

Tactic:
obtain ⟨x, hx', rfl⟩ := hx.1

Premises used: And.left, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
⊢ IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)

Tactic:
hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h : ‖cfcₙ (p := p) f a‖ = (fun (x : 𝕜) ↦ ‖f x‖) x
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖

Tactic:
convert! hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h :
  norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
      { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
        C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } =
    (fun (x : 𝕜) ↦ ‖f x‖) x
⊢ ‖cfcₙ (p := p) f a‖ = (fun (x : 𝕜) ↦ ‖f x‖) x

Tactic:
rw [cfcₙ_apply f a, norm_cfcₙHom a _]

Premises used: norm_cfcₙHom, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h :
  norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
      { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
        C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } ≤
    (fun (x : 𝕜) ↦ ‖f x‖) x
h₁ :
  (fun (x : 𝕜) ↦ ‖f x‖) x ≤
    norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
      { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
        C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ }
⊢ norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
      { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
        C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } =
    (fun (x : 𝕜) ↦ ‖f x‖) x

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h :
  ∀ (x_1 : (↑(σₙ 𝕜 a) : Type u_1)),
    norm (E := 𝕜)
        (((↑{ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
                    C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } :
                C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) :
              (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
            x_1 :
          𝕜) ≤
      ‖f x‖
⊢ norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
      { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
        C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } ≤
    (fun (x : 𝕜) ↦ ‖f x‖) x

Tactic:
apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr

Premises used: Iff.mpr, ContinuousMap.norm_le, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
y : 𝕜
hy : y ∈ σₙ 𝕜 a
⊢ norm (E := 𝕜)
      (((↑{ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
                  C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) :
            (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) y hy) :
        𝕜) ≤
    ‖f x‖

Tactic:
hx.2 ⟨y, hy, rfl⟩

Premises used: And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
y : 𝕜
hy : y ∈ σₙ 𝕜 a
⊢ norm (E := 𝕜)
      (((↑{ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
                  C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) :
            (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) y hy) :
        𝕜) ≤
    ‖f x‖

Tactic:
exact hx.2 ⟨y, hy, rfl⟩

Premises used: And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤
    norm (E := 𝕜)
      (((↑{ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
                  C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) :
            (a : { x : 𝕜 // x ∈ σₙ 𝕜 a }) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) x hx') :
        𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤
    norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
      { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := ⋯ :
        C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ }

Tactic:
exact le_trans (by simp) <| ContinuousMap.norm_coe_le_norm _ (⟨x, hx'⟩ : σₙ 𝕜 a)

Premises used: ContinuousMap.norm_coe_le_norm, Subtype.mk, le_trans
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ IsGreatest (Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖.toNNReal

Tactic:
Real.toNNReal_monotone.map_isGreatest (.norm_cfcₙ f a)

Premises used: IsGreatest.norm_cfcₙ, Real.toNNReal_monotone, Monotone.map_isGreatest
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
h : (fun (x : 𝕜) ↦ ‖f x‖₊) '' σₙ 𝕜 a = Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a
h₁ : ‖cfcₙ (p := p) f a‖₊ = ‖cfcₙ (p := p) f a‖.toNNReal
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖₊) '' σₙ 𝕜 a) ‖cfcₙ (p := p) f a‖₊

Tactic:
convert! Real.toNNReal_monotone.map_isGreatest (.norm_cfcₙ f a)

Premises used: IsGreatest.norm_cfcₙ, Real.toNNReal_monotone, Monotone.map_isGreatest
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ (fun (x : 𝕜) ↦ ‖f x‖₊) '' σₙ 𝕜 a = Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a

Tactic:
simp [Set.image_image, norm_toNNReal]

Premises used: Set.image_image, norm_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖cfcₙ (p := p) f a‖₊ = ‖cfcₙ (p := p) f a‖.toNNReal

Tactic:
simp [Set.image_image, norm_toNNReal]

Premises used: Set.image_image, norm_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖f x‖ ≤ ‖cfcₙ (p := p) f a‖

Tactic:
IsGreatest.norm_cfcₙ f a hf hf₀ ha |>.2 ⟨x, hx, rfl⟩

Premises used: IsGreatest.norm_cfcₙ, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖f x‖₊ ≤ ‖cfcₙ (p := p) f a‖₊

Tactic:
IsGreatest.nnnorm_cfcₙ f a hf hf₀ ha |>.2 ⟨x, hx, rfl⟩

Premises used: IsGreatest.nnnorm_cfcₙ, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
⊢ ‖cfcₙ (p := p) f a‖ ≤ c

Tactic:
cfcₙ_cases (‖·‖ ≤ c) a f ?_ fun hf hf0 ha ↦ ?_

Premises used: Norm.norm, LE.le, cfcₙ_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
refine_1 : norm.{u_2} (E := A) 0 ≤ c
refine_2 :
  ∀ (hf : ContinuousOn f (σₙ 𝕜 a))
    (hf0 :
      Eq (α := 𝕜)
        (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ :
                C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
              (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
            0 :
          𝕜)
        (0 : 𝕜))
    (ha : p a),
    (fun (x : A) ↦ ‖x‖ ≤ c)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A)
        { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 :
          C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ })
⊢ ‖cfcₙ (p := p) f a‖ ≤ c

Tactic:
refine cfcₙ_cases (‖·‖ ≤ c) a f ?_ fun hf hf0 ha ↦ ?_

Premises used: Norm.norm, LE.le, cfcₙ_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
⊢ (fun (x : A) ↦ ‖x‖ ≤ c) 0

Tactic:
simpa using (norm_nonneg _).trans <| h 0 (quasispectrum.zero_mem 𝕜 a)

Premises used: quasispectrum.zero_mem, LE.le.trans, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 :
  Eq (α := 𝕜)
    (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
          (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
        0 :
      𝕜)
    (0 : 𝕜)
ha : p a
refine_2 : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a)) c
⊢ norm.{u_2} (E := A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A)
          { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 :
            C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } :
        A) ≤
    c

Tactic:
simp only [← cfcₙ_apply f a, isLUB_le_iff (IsGreatest.norm_cfcₙ f a hf hf0 ha |>.isLUB)]

Premises used: IsGreatest.norm_cfcₙ, isLUB_le_iff, IsGreatest.isLUB, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 :
  Eq (α := 𝕜)
    (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
          (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
        0 :
      𝕜)
    (0 : 𝕜)
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤ c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 :
  Eq (α := 𝕜)
    (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
          (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
        0 :
      𝕜)
    (0 : 𝕜)
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤ c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ ‖cfcₙ (p := p) f a‖ ≤ c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c

Tactic:
⟨fun h _ hx ↦ norm_apply_le_norm_cfcₙ f a hx hf hf₀ ha |>.trans h, norm_cfcₙ_le⟩

Premises used: norm_cfcₙ_le, Iff.intro, LE.le.trans, norm_apply_le_norm_cfcₙ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
⊢ ‖cfcₙ (p := p) f a‖ < c

Tactic:
cfcₙ_cases (‖·‖ < c) a f ?_ fun hf hf0 ha ↦ ?_

Premises used: Norm.norm, LT.lt, cfcₙ_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
refine_1 : norm.{u_2} (E := A) 0 < c
refine_2 :
  ∀ (hf : ContinuousOn f (σₙ 𝕜 a))
    (hf0 :
      Eq (α := 𝕜)
        (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ :
                C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
              (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
            0 :
          𝕜)
        (0 : 𝕜))
    (ha : p a),
    (fun (x : A) ↦ ‖x‖ < c)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A)
        { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 :
          C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ })
⊢ ‖cfcₙ (p := p) f a‖ < c

Tactic:
refine cfcₙ_cases (‖·‖ < c) a f ?_ fun hf hf0 ha ↦ ?_

Premises used: Norm.norm, LT.lt, cfcₙ_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
⊢ (fun (x : A) ↦ ‖x‖ < c) 0

Tactic:
simpa using (norm_nonneg _).trans_lt <| h 0 (quasispectrum.zero_mem 𝕜 a)

Premises used: quasispectrum.zero_mem, OfNat.ofNat, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 :
  Eq (α := 𝕜)
    (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
          (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
        0 :
      𝕜)
    (0 : 𝕜)
ha : p a
refine_2 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σₙ 𝕜 a) x → x < c
⊢ norm.{u_2} (E := A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → A)
          { toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 :
            C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ } :
        A) <
    c

Tactic:
simp only [← cfcₙ_apply f a, (IsGreatest.norm_cfcₙ f a hf hf0 ha |>.lt_iff)]

Premises used: IsGreatest.lt_iff, IsGreatest.norm_cfcₙ, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 :
  Eq (α := 𝕜)
    (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
          (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
        0 :
      𝕜)
    (0 : 𝕜)
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x < c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 :
  Eq (α := 𝕜)
    (({ toFun := (σₙ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) } :
          (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
        0 :
      𝕜)
    (0 : 𝕜)
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x < c

Tactic:
exact h x hx