awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
⊢ 0 ≤ b

Tactic:
have hb : 0 ≤ b := ha.trans hab
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (Icc 0 1) x ↔ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) x
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
x : ℝ≥0
⊢ Membership.mem (γ := Set ℝ≥0) (Icc 0 1) x ↔ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})

Tactic:
have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
pos :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p) ⦃a b : A⦄ (hab : a ≤ b) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})),
    LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
rw [hIcc] at hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
pos :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p),
    LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
pos₁ :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) {0} p), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
pos₂ :
  ∀ (hp : Membership.mem (γ := Set ℝ≥0) {1} p), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
obtain (hp | hp) | hp := hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
monotoneOn_nnrpow_Ioo hp ha hb hab

Premises used: _private.0.CFC.monotoneOn_nnrpow_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
exact monotoneOn_nnrpow_Ioo hp ha hb hab

Premises used: _private.0.CFC.monotoneOn_nnrpow_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) {0} p
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
simp_all [mem_singleton_iff]

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) {1} p
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
simp_all [mem_singleton_iff, nnrpow_one a, nnrpow_one b]

Premises used: CFC.nnrpow_one, Set.mem_singleton_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
⊢ a ^ p = 0

Tactic:
have : a ^ p = 0 := cfcₙ_apply_of_not_predicate a ha
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
this : a ^ p = 0
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
rw : a ^ (1 / 2) ≤ b ^ (1 / 2)
⊢ sqrt a ≤ sqrt b

Tactic:
rw [CFC.sqrt_eq_nnrpow a, CFC.sqrt_eq_nnrpow b]

Premises used: CFC.sqrt_eq_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ a ^ (1 / 2) ≤ b ^ (1 / 2)

Tactic:
(monotone_nnrpow (A := A) ?_) hab

Premises used: CFC.monotone_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
refine : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) (1 / 2)
⊢ a ^ (1 / 2) ≤ b ^ (1 / 2)

Tactic:
refine (monotone_nnrpow (A := A) ?_) hab

Premises used: CFC.monotone_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
left : 0 ≤ 1 / 2
right : 1 / 2 ≤ 1
⊢ Membership.mem (γ := Set ℝ≥0) (Icc 0 1) (1 / 2)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
⊢ a ^ p ≤ b ^ p

Tactic:
monotone_nnrpow hp hab

Premises used: CFC.monotone_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ sqrt a ≤ sqrt b

Tactic:
monotone_sqrt hab

Premises used: CFC.monotone_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
obtain :
  ∀ (μ : Measure ℝ)
    (hμ :
      ∀ (a : A),
        Membership.mem (γ := Set A) (Ici 0) a →
          IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a)
              (Ioi 0) μ ∧
            a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ),
    ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
obtain ⟨μ, hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ A hp

Premises used: CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
ConcaveOn.congr ?_ h₃'.symm

Premises used: ConcaveOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
refine :
  ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦
    ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
refine ConcaveOn.congr ?_ h₃'.symm

Premises used: ConcaveOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦
    ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ

Tactic:
integral_concaveOn_of_integrand_ae (convex_Ici _) ?_ fun a ha => (hμ a ha).1

Premises used: And.left, convex_Ici, MeasureTheory.integral_concaveOn_of_integrand_ae
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
refine : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x))
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦
    ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ

Tactic:
refine integral_concaveOn_of_integrand_ae (convex_Ici _) ?_ fun a ha => (hμ a ha).1

Premises used: And.left, convex_Ici, MeasureTheory.integral_concaveOn_of_integrand_ae
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t))
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x))

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t))

Tactic:
concaveOn_cfcₙ_rpowIntegrand₀₁ hp ht

Premises used: CFC.concaveOn_cfcₙ_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t))

Tactic:
exact concaveOn_cfcₙ_rpowIntegrand₀₁ hp ht

Premises used: CFC.concaveOn_cfcₙ_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (Icc 0 1) x ↔ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) x
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
x : ℝ≥0
⊢ Membership.mem (γ := Set ℝ≥0) (Icc 0 1) x ↔ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})

Tactic:
have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
⊢ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p

Tactic:
rw [hIcc] at hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp₁ : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
⊢ Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})

Tactic:
rw [hIcc] at hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1 ∪ {0} ∪ {1}) p
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
inl : ∀ (hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
inl₁ : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {0} p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
inr : ∀ (hp : Membership.mem (γ := Set ℝ≥0) {1} p), ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
obtain (hp | hp) | hp := hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
concaveOn_nnrpow_Ioo hp

Premises used: _private.0.CFC.concaveOn_nnrpow_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
exact concaveOn_nnrpow_Ioo hp

Premises used: _private.0.CFC.concaveOn_nnrpow_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) {0} p
⊢ p = 0

Tactic:
simp only [mem_singleton_iff] at hp

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 0
inl : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
simp only [hp, nnrpow_zero]

Premises used: CFC.nnrpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ 0

Tactic:
concaveOn_const _ (convex_Ici _)

Premises used: convex_Ici, concaveOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 0
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ 0

Tactic:
exact concaveOn_const _ (convex_Ici _)

Premises used: convex_Ici, concaveOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : Membership.mem (γ := Set ℝ≥0) {1} p
⊢ p = 1

Tactic:
simp only [mem_singleton_iff] at hp

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 1
inr : ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ≥0) a 1
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ a ^ p

Tactic:
simp only [hp]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 1
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ≥0) a 1

Tactic:
ConcaveOn.congr (concaveOn_id (convex_Ici _)) nnrpow_one_eqOn.symm

Premises used: concaveOn_id, CFC.nnrpow_one_eqOn, ConcaveOn.congr, convex_Ici, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hIcc : Eq (α := Set ℝ≥0) (Icc 0 1) (Ioo 0 1 ∪ {0} ∪ {1})
hp : p = 1
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (a : A) ↦ HPow.hPow (β := ℝ≥0) a 1

Tactic:
exact ConcaveOn.congr (concaveOn_id (convex_Ici _)) nnrpow_one_eqOn.symm

Premises used: concaveOn_id, CFC.nnrpow_one_eqOn, ConcaveOn.congr, convex_Ici, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
simp_rw : ConcaveOn ℝ (β := A) (fun (a : A) ↦ Ici 0 a) fun (a : A) ↦ a ^ (1 / 2)
⊢ ConcaveOn ℝ (β := A) (fun (a : A) ↦ Ici 0 a) fun (a : A) ↦ sqrt a

Tactic:
simp_rw [sqrt_eq_nnrpow]

Premises used: CFC.sqrt_eq_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ ConcaveOn ℝ (β := A) (fun (a : A) ↦ Ici 0 a) fun (a : A) ↦ a ^ (1 / 2)

Tactic:
exact concaveOn_nnrpow ⟨by norm_num, by norm_num⟩

Premises used: CFC.concaveOn_nnrpow, And.intro