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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
x : R
hx : x ∈ σₙ R (cfcₙ 0 0)
⊢ 0 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
⊢ σₙ R 0 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: a b : ℝ
h : a < b
⊢ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) =
    polynomialFunctions (Set.Icc a b)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
⊢ cfcₙ f 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ polynomialFunctions s = R[(toContinuousMapOnAlgHom s) X]

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ polynomialFunctions s ≤ φ.equalizer ψ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
inst✝¹ : StarRing R
inst✝ : ContinuousStar R
s : Set R
⊢ (polynomialFunctions s).starClosure = adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : IsTopologicalSemiring R
A : Type u_2
inst✝⁴ : StarRing R
inst✝³ : ContinuousStar R
inst✝² : Semiring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →⋆ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: ⊢ (polynomialFunctions I).topologicalClosure = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f✝ g : R → R
a✝ : A
hf : ContinuousOn f✝ (σₙ R a✝)
hf0 : f✝ 0 = 0
hg : ContinuousOn g (σₙ R a✝)
hg0 : g 0 = 0
ha : p a✝
f : R → R
a : A
⊢ Commute (star (cfcₙ f a)) (cfcₙ f a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: n k : ℕ
h : k ≤ n + 1
⊢ LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = (X + (1 - X)) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (X + (1 - X)) ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ (pderiv true) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
⊢ (pderiv true) y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
hf_neg : ContinuousOn (fun x ↦ -f x) (σₙ R a)
⊢ ContinuousOn f (σₙ R a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(n.choose k) * X

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
⊢ cfcₙ (-f) = -cfcₙ f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ cfcₙ (fun x ↦ -x) a = -a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommRing R
inst✝¹² : Nontrivial R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
inst✝ : UniqueHom R A
hf : ContinuousOn f ((fun x ↦ -x) '' σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f (-x)) a = cfcₙ f (-a)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ (cfcₙHom ha) f ↔ 0 ≤ f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ g x
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
⊢ cfcₙ f a ≤ cfcₙ g a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ 0 ≤ cfcₙ f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ ContinuousOn id (σₙ R a)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ (bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
⊢ 0 ≤ 1 - ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ 0 ≤ (bernstein n ν) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ ↑↑k / ↑n ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n : ℕ
⊢ 0/ₙ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Fin.last n/ₙ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n : ℕ
x : ↑I
⊢ ∑ k, (bernstein n ↑k) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
⊢ 0 ≤ cfcₙ f a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ∑ k, (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
n : ℕ
f : C(↑I, E)
x : ↑I
⊢ (bernsteinApproximation n f) x = ∑ k, (bernstein n ↑k) x • f k/ₙ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
n : ℕ
f : C(↑I, E)
⊢ (bernsteinApproximation n f) 0 = f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
n : ℕ
hn : n ≠ 0
f : C(↑I, E)
⊢ (bernsteinApproximation n f) 1 = f 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E
this : ∀ U ∈ 𝓝 0, Convex ℝ U → ∀ᶠ (n : ℕ) in atTop, ∀ (x : ↑I), gauge U ((bernsteinApproximation n f) x - f x) < 1
⊢ Tendsto (fun n ↦ bernsteinApproximation n f) atTop (𝓝 f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : PartialOrder R
inst✝¹⁶ : Nontrivial R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : MetricSpace R
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : ContinuousStar R
inst✝¹¹ : ContinuousSqrt R
inst✝¹⁰ : StarOrderedRing R
inst✝⁹ : NoZeroDivisors R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
⊢ cfcₙ f a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
⊢ Continuous fun x ↦
    match x with
    | (x, y) => gauge U (f x - f y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
⊢ ∃ C, ∀ (x y : ↑I), gauge U (f x - f y) ≤ C

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
⊢ (cfcₙHom ha) f ≤ (cfcₙHom ha) g ↔ f ≤ g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
this : ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (x y : ↑I), (x, y) ∈ {p | dist p.1 p.2 < j} → (f x, f y) ∈ {x | x.1 - x.2 ∈ id i}
⊢ 0 < 1 / 2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ cfcₙ f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
⊢ ∃ δ > 0, ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2

Tactic:
by

Goal state after: