ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>S : Type u_3<VAR>SMulZeroClass S R<VAR>ContinuousConstSMul S R<VAR>SMulZeroClass S A<VAR>IsScalarTower S R A<VAR>IsScalarTower S R (R → R)<VAR>s : S<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>h0 : f 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (fun x => s • f x) a = s • cfcₙ f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>h0 : f 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (fun x => r * f x) a = r • cfcₙ f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>cfcₙ (fun x => star (f x)) a = star (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>S : Type u_3<VAR>SMulZeroClass S R<VAR>ContinuousConstSMul S R<VAR>SMulZeroClass S A<VAR>IsScalarTower S R A<VAR>IsScalarTower S R (R → R)<VAR>s : S<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => s • x) a = s • a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>r : R<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => r * x) a = r • a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => star x) a = star a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : ContinuousOn g (f '' σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : ContinuousOn g (f '' σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => g (f x)) a = cfcₙ g (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>S : Type u_3<VAR>SMulZeroClass S R<VAR>ContinuousConstSMul S R<VAR>SMulZeroClass S A<VAR>IsScalarTower S R A<VAR>IsScalarTower S R (R → R)<VAR>s : S<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f ((fun x => s • x) '' σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => f (s • x)) a = cfcₙ f (s • a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f ((fun x => r * x) '' σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => f (r * x)) a = cfcₙ f (r • a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>hf : ContinuousOn f (star '' σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => f (star x)) a = cfcₙ f (star a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>h_spec : σₙ R a ⊆ {0}<VAR>ha : p a := by cfc_tac<GOAL>a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<GOAL>σₙ R 0 = {0}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<GOAL>cfcₙ f 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ (fun x => f x - g x) a = cfcₙ f a - cfcₙ g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>cfcₙ (fun x => -f x) a = -cfcₙ f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => -x) a = -a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>hf : ContinuousOn f ((fun x => -x) '' σₙ R a) := by cfc_cont_tac<VAR>h0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ (fun x => f (-x)) a = cfcₙ f (-a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f g : C(↑(σₙ R a), R)₀<VAR>hfg : f ≤ g<GOAL>(cfcₙHom ha) f ≤ (cfcₙHom ha) g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>0 ≤ (cfcₙHom ha) f ↔ 0 ≤ f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>h : ∀ x ∈ σₙ R a, f x ≤ g x<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ f a ≤ cfcₙ g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>h0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>0 ≤ cfcₙ f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ σₙ R a, 0 ≤ f x<GOAL>0 ≤ cfcₙ f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ σₙ R a, f x ≤ 0<GOAL>cfcₙ f a ≤ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a<VAR>f g : C(↑(σₙ R a), R)₀<GOAL>(cfcₙHom ha) f ≤ (cfcₙHom ha) g ↔ f ≤ g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<VAR>hg0 : g 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommRing R<VAR>Nontrivial R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>h0 : f 0 = 0 := by cfc_zero_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcₙ f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Field R<VAR>StarRing R<VAR>MetricSpace R<VAR>CompleteSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<GOAL>ClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Field R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>σₙ R ((cfcₙHom_of_cfcHom R ha) f) = Set.range ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Field R<VAR>StarRing R<VAR>MetricSpace R<VAR>CompleteSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<GOAL>cfcₙHom ha = cfcₙHom_of_cfcHom R ha
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Field R<VAR>StarRing R<VAR>MetricSpace R<VAR>CompleteSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac<VAR>hf0 : f 0 = 0 := by cfc_zero_tac<GOAL>cfcₙ f a = cfc f a
<VAR>a : ℝ<VAR>ha : a < 0<VAR>b s : ℝ<GOAL>(fun x => rexp (a * x ^ 2 + b * x)) =o[Filter.atTop] fun x => x ^ s
<VAR>a : ℂ<VAR>ha : a.re < 0<VAR>b : ℂ<VAR>s : ℝ<GOAL>(fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.atTop] fun x => x ^ s
<VAR>a : ℂ<VAR>ha : a.re < 0<VAR>b : ℂ<VAR>s : ℝ<GOAL>(fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.cocompact ℝ] fun x => |x| ^ s
<VAR>a : ℝ<VAR>ha : 0 < a<VAR>s : ℝ<GOAL>Filter.Tendsto (fun x => |x| ^ s * rexp (-a * x ^ 2)) (Filter.cocompact ℝ) (𝓝 0)
<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>s : ℝ<GOAL>(fun x => cexp (-a * ↑x ^ 2)) =o[Filter.cocompact ℝ] fun x => |x| ^ s
<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + Complex.I * b) ^ 2)
<VAR>a : ℂ<VAR>ha : 0 < a.re<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * ↑n ^ 2)
<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>∑' (n : ℤ), rexp (-π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), rexp (-π / a * ↑n ^ 2)
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>HasStrictDerivAt Real.log x⁻¹ x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasStrictDerivAt Real.log x⁻¹ x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt Real.log x⁻¹ x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>DifferentiableAt ℝ Real.log x
<GOAL>DifferentiableOn ℝ Real.log {0}ᶜ
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.log x ↔ x ≠ 0
<VAR>x : ℝ<GOAL>deriv Real.log x = x⁻¹
<VAR>n : ℕ∞<GOAL>ContDiffOn ℝ n Real.log {0}ᶜ
<VAR>x : ℝ<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n Real.log x ↔ x ≠ 0
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>hf : HasDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasDerivAt (fun y => Real.log (f y)) (f' / f x) x
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => Real.log (f x)) s x = derivWithin f s x / f x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0<GOAL>deriv (fun x => Real.log (f x)) x = deriv f x / f x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>h₁ : DifferentiableAt ℝ f x<VAR>h₂ : f x ≠ 0<GOAL>deriv (Real.log ∘ f) x = logDeriv f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x ≠ 0<GOAL>HasFDerivWithinAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasFDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasFDerivAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasStrictFDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasStrictFDerivAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0<GOAL>DifferentiableWithinAt ℝ (fun x => Real.log (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0<GOAL>DifferentiableAt ℝ (fun x => Real.log (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>hx : f x ≠ 0<GOAL>ContDiffAt ℝ n (fun x => Real.log (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>hx : f x ≠ 0<GOAL>ContDiffWithinAt ℝ n (fun x => Real.log (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<VAR>hs : ∀ x ∈ s, f x ≠ 0<GOAL>ContDiffOn ℝ n (fun x => Real.log (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>ContDiff ℝ n fun x => Real.log (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hf : DifferentiableOn ℝ f s<VAR>hx : ∀ x ∈ s, f x ≠ 0<GOAL>DifferentiableOn ℝ (fun x => Real.log (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hf : Differentiable ℝ f<VAR>hx : ∀ (x : E), f x ≠ 0<GOAL>Differentiable ℝ fun x => Real.log (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.log (f x)) s x = (f x)⁻¹ • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0<GOAL>fderiv ℝ (fun x => Real.log (f x)) x = (f x)⁻¹ • fderiv ℝ f x
<VAR>t : ℝ<GOAL>Filter.Tendsto (fun x => x * Real.log (1 + t / x)) Filter.atTop (𝓝 t)
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>n : ℕ<GOAL>|∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + Real.log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
<VAR>x : ℝ<VAR>h : |x| < 1<GOAL>HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-Real.log (1 - x))
<VAR>x : ℝ<VAR>h : |x| < 1<GOAL>HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (Real.log (1 + x) - Real.log (1 - x))
<VAR>a : ℝ<VAR>h : 0 < a<GOAL>HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (Real.log (1 + a⁻¹))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>l.NeBot<VAR>Filter.TendstoIxxClass Set.Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop<VAR>hfg : deriv f =O[l] g<GOAL>¬MeasureTheory.IntegrableOn g k MeasureTheory.volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>l.NeBot<VAR>Filter.TendstoIxxClass Set.Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop<VAR>hfg : deriv f =O[l] g<GOAL>¬MeasureTheory.IntegrableOn g k MeasureTheory.volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>a b : ℝ<VAR>l : Filter ℝ<VAR>l.NeBot<VAR>Filter.TendstoIxxClass Set.Icc l l<VAR>hl : [[a, b]] ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop<VAR>hfg : deriv f =O[l] g<GOAL>¬IntervalIntegrable g MeasureTheory.volume a b