awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
refine : MonotoneOn g {a : A | IsStrictlyPositive a}
⊢ MonotoneOn log {a : A | IsStrictlyPositive a}

Tactic:
refine MonotoneOn.congr ?_ hg

Premises used: MonotoneOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ MonotoneOn g {a : A | IsStrictlyPositive a}

Tactic:
isClosed_monotoneOn.mem_of_tendsto (f := f) (b := (𝓝[>] 0))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_

Premises used: Set.Mem, setOf, IsClosed.mem_of_tendsto, MonotoneOn, CFC.tendsto_ite_cfc_rpow_sub_one_ite_log, isClosed_monotoneOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
refine :
  ∀ᶠ (x : ℝ) in 𝓝[>] 0,
    Membership.mem (γ := Set ((a : A) → A)) {f : A → A | MonotoneOn f {a : A | IsStrictlyPositive a}} (f x)
⊢ MonotoneOn g {a : A | IsStrictlyPositive a}

Tactic:
refine isClosed_monotoneOn.mem_of_tendsto (f := f) (b := (𝓝[>] 0))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_

Premises used: IsClosed.mem_of_tendsto, CFC.tendsto_ite_cfc_rpow_sub_one_ite_log, isClosed_monotoneOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1

Tactic:
have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1 := nhdsGT_basis 0 |>.mem_of_mem zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
h : ∀ (hp : 0 < p) (hp' : p < 1), MonotoneOn (f p) {a : A | IsStrictlyPositive a}
⊢ 0 < p ∧ p < 1 → MonotoneOn (f p) {a : A | IsStrictlyPositive a}

Tactic:
⟨hp, hp'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
h : ∀ (p : ℝ) (hp : 0 < p) (hp' : p < 1), MonotoneOn (f p) {a : A | IsStrictlyPositive a}
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0,
    Membership.mem (γ := Set ((a : A) → A)) {f : A → A | MonotoneOn f {a : A | IsStrictlyPositive a}} (f x)

Tactic:
filter_upwards [h₁] with p ⟨hp, hp'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ MonotoneOn (f p) {a : A | IsStrictlyPositive a}

Tactic:
MonotoneOn.congr (fun a ha b hb hab ↦ ?_) CFC.cfc_rpow_sub_one_eqOn.symm

Premises used: MonotoneOn.congr, _private.0.CFC.cfc_rpow_sub_one_eqOn, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h :
  ∀ (a : A) (ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a) (b : A)
    (hb : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b) (hab : a ≤ b),
    p⁻¹ • (a ^ p - 1) ≤ p⁻¹ • (b ^ p - 1)
⊢ MonotoneOn (f p) {a : A | IsStrictlyPositive a}

Tactic:
refine MonotoneOn.congr (fun a ha b hb hab ↦ ?_) CFC.cfc_rpow_sub_one_eqOn.symm

Premises used: MonotoneOn.congr, _private.0.CFC.cfc_rpow_sub_one_eqOn, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
b : A
hb : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b
hab : a ≤ b
h : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) p
⊢ p⁻¹ • (a ^ p - 1) ≤ p⁻¹ • (b ^ p - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
b : A
hb : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b
hab : a ≤ b
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) p

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : IsStrictlyPositive a
⊢ log a ≤ log b

Tactic:
log_monotoneOn ha (ha.of_le hab) hab

Premises used: CFC.log_monotoneOn, IsStrictlyPositive.of_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
set :
  let s : Set A := {a : A | IsStrictlyPositive a};
  ConcaveOn ℝ s log
⊢ ConcaveOn ℝ {a : A | IsStrictlyPositive a} log

Tactic:
set s := {a : A | IsStrictlyPositive a}
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
⊢ EqOn g log s

Tactic:
simp +contextual [g, Set.EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
⊢ EqOn g log s

Tactic:
have hg : s.EqOn g (log (A := A)) := by simp +contextual [g, Set.EqOn]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ConcaveOn ℝ s log

Tactic:
ConcaveOn.congr ?_ hg

Premises used: ConcaveOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
refine : ConcaveOn ℝ s g
⊢ ConcaveOn ℝ s log

Tactic:
refine ConcaveOn.congr ?_ hg

Premises used: ConcaveOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
apply : ∀ᶠ (x : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ((a : A) → A)) {f : A → A | ConcaveOn ℝ s f} (f x)
⊢ ConcaveOn ℝ s g

Tactic:
apply isClosed_setOf_concaveOn.mem_of_tendsto (f := f) (b := (𝓝[>] (0 : ℝ)))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_

Premises used: isClosed_setOf_concaveOn, IsClosed.mem_of_tendsto, CFC.tendsto_ite_cfc_rpow_sub_one_ite_log
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1

Tactic:
have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1 := nhdsGT_basis 0 |>.mem_of_mem zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
h : ∀ (hp : 0 < p) (hp' : p < 1), ConcaveOn ℝ s (f p)
⊢ 0 < p ∧ p < 1 → ConcaveOn ℝ s (f p)

Tactic:
⟨hp, hp'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
h : ∀ (p : ℝ) (hp : 0 < p) (hp' : p < 1), ConcaveOn ℝ s (f p)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ((a : A) → A)) {f : A → A | ConcaveOn ℝ s f} (f x)

Tactic:
filter_upwards [h₁] with p ⟨hp, hp'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ ConcaveOn ℝ s (f p)

Tactic:
ConcaveOn.congr ?_ CFC.cfc_rpow_sub_one_eqOn.symm

Premises used: _private.0.CFC.cfc_rpow_sub_one_eqOn, ConcaveOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h : ConcaveOn ℝ (β := A) s fun (a : A) ↦ p⁻¹ • (a ^ p - 1)
⊢ ConcaveOn ℝ s (f p)

Tactic:
refine ConcaveOn.congr ?_ CFC.cfc_rpow_sub_one_eqOn.symm

Premises used: _private.0.CFC.cfc_rpow_sub_one_eqOn, ConcaveOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ 0 ≤ p⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h : ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p - 1
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ p⁻¹ • (a ^ p - 1)

Tactic:
refine ConcaveOn.smul (by positivity) ?_

Premises used: ConcaveOn.smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ Convex ℝ s

Tactic:
grind [convex_iff_forall_pos]

Premises used: convex_iff_forall_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ Convex ℝ s

Tactic:
have h_convex : Convex ℝ s := by grind [convex_iff_forall_pos]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p - 1

Tactic:
ConcaveOn.sub ?_ (convexOn_const _ h_convex)

Premises used: ConcaveOn.sub, convexOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
h : ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p - 1

Tactic:
refine ConcaveOn.sub ?_ (convexOn_const _ h_convex)

Premises used: ConcaveOn.sub, convexOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ s ⊆ Ici 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
h : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
⊢ ConcaveOn ℝ (β := A) s fun (a : A) ↦ a ^ p

Tactic:
refine ConcaveOn.subset (t := Ici 0) ?_ (by grind) h_convex

Premises used: ConcaveOn.subset
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) p

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
exact CFC.concaveOn_rpow (by grind)

Premises used: CFC.concaveOn_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ a⁺ = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ a⁻ = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ Eq.{u_1 + 1} (α := A) 0⁺ 0

Tactic:
simp [posPart_def]

Premises used: CFC.posPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ Eq.{u_1 + 1} (α := A) 0⁻ 0

Tactic:
simp [negPart_def]

Premises used: CFC.negPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ a⁺ = 0

Tactic:
cfcₙ_apply_of_not_predicate a ha

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ a⁻ = 0

Tactic:
cfcₙ_apply_of_not_predicate a ha

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
⊢ a⁺ * a⁻ = 0

Tactic:
rw [posPart_def, negPart_def]

Premises used: CFC.negPart_def, CFC.posPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
pos :
  ∀ (ha : IsSelfAdjoint a),
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
neg :
  ∀ (ha : ¬IsSelfAdjoint a),
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint