awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : SMulCommClass ℝ A A
inst_4 : IsScalarTower ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : CompleteSpace A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 1 2) p
μ : Measure ℝ
hμ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧
        x ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : Membership.mem (γ := Set ℝ) (Ioo 1 2) (↑p : ℝ)
f : (t x : ℝ) → ℝ := fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
⊢ cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a =
    ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ

Tactic:
cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint

Premises used: cfcₙ_setIntegral, LE.le.isSelfAdjoint, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : SMulCommClass ℝ A A
inst_4 : IsScalarTower ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : CompleteSpace A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 1 2) p
μ : Measure ℝ
hμ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧
        x ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : Membership.mem (γ := Set ℝ) (Ioo 1 2) (↑p : ℝ)
f : (t x : ℝ) → ℝ := fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
a₁ : a ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
a₂ :
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a =
    cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ

Tactic:
calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint

Premises used: cfcₙ, Set.Ioi, cfcₙ_setIntegral, LE.le.isSelfAdjoint, MeasureTheory.Measure.restrict, measurableSet_Ioi, NNReal.nnrpow, MeasureTheory.integral, Real.rpowIntegrand₁₂, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : SMulCommClass ℝ A A
inst_4 : IsScalarTower ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : CompleteSpace A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 1 2) p
μ : Measure ℝ
hμ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧
        x ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : Membership.mem (γ := Set ℝ) (Ioo 1 2) (↑p : ℝ)
f : (t x : ℝ) → ℝ := fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
case : a ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
case₁ :
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a =
    cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ

Tactic:
case integral => calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint

Premises used: cfcₙ, Set.Ioi, cfcₙ_setIntegral, LE.le.isSelfAdjoint, MeasureTheory.Measure.restrict, measurableSet_Ioi, NNReal.nnrpow, MeasureTheory.integral, Real.rpowIntegrand₁₂, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
⊢ p ≠ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
rw :
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
⊢ cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) x =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x

Tactic:
rw [rpowIntegrand₀₁_eq_sub (by grind) ht]

Premises used: Real.rpowIntegrand₀₁_eq_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
⊢ ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
⊢ ∀ (x : ℝ), x ≠ 0

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
⊢ ∀ x_1 ∈ spectrum ℝ x, t + x_1 ≠ 0

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
funProp : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
funProp₁ : ∀ (x : ℝ), x ≠ 0
funProp₂ : ∀ x_1 ∈ spectrum ℝ x, t + x_1 ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)

Tactic:
fun_prop (disch := grind -abstractProof)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)

Tactic:
have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
      fun_prop (disch := grind -abstractProof)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)

Tactic:
have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)
⊢ ∀ r ∈ spectrum ℝ x, t + r ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)
⊢ ∀ r ∈ spectrum ℝ x, t + r ≠ 0

Tactic:
have hspectrum :  ∀ r ∈ spectrum ℝ x, t + r ≠ 0 := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1)) x -
      cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ t ^ p * (t + z)⁻¹) x

Tactic:
have := cfc_sub (fun _ : ℝ => t ^ (p - 1)) (fun z : ℝ => t ^ p * (t + z)⁻¹) x
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
⊢ EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)

Tactic:
have h₁ : (Ici (0 : A)).EqOn (cfc (rpowIntegrand₀₁ p t))
      (fun x : A =>
        algebraMap ℝ A (t ^ (p - 1)) - t ^ p • Ring.inverse (algebraMap ℝ A t + x)) := by
    intro x hx
    rw [rpowIntegrand₀₁_eq_sub (by grind) ht]
    have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
      fun_prop (disch := grind -abstractProof)
    have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop
    have hspectrum :  ∀ r ∈ spectrum ℝ x, t + r ≠ 0 := by grind
    have := cfc_sub (fun _ : ℝ => t ^ (p - 1)) (fun z : ℝ => t ^ p * (t + z)⁻¹) x
    rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
h₁ :
  EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)
⊢ ConcaveOn ℝ (Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))

Tactic:
ConcaveOn.congr ?_ h₁.symm

Premises used: ConcaveOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
h₁ :
  EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)
refine :
  ConcaveOn ℝ (β := A) (Ici 0) fun (x : A) ↦
    HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x))
⊢ ConcaveOn ℝ (Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))

Tactic:
refine ConcaveOn.congr ?_ h₁.symm

Premises used: ConcaveOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
h₁ :
  EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (x : A) ↦
    HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x))

Tactic:
ConcaveOn.sub (concaveOn_const _ (convex_Ici 0)) ?_

Premises used: convex_Ici, ConcaveOn.sub, OfNat.ofNat, concaveOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
h₁ :
  EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)
refine :
  ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦
    t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
⊢ ConcaveOn ℝ (β := A) (Ici 0) fun (x : A) ↦
    HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x))

Tactic:
refine ConcaveOn.sub (concaveOn_const _ (convex_Ici 0)) ?_

Premises used: convex_Ici, ConcaveOn.sub, OfNat.ofNat, concaveOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
h₁ :
  EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)
⊢ 0 ≤ t ^ p

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
h₁ :
  EqOn (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
    (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    (Ici 0)
⊢ ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦
    t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)

Tactic:
exact ConvexOn.smul (by positivity) <| CStarAlgebra.convexOn_ringInverse_algebraMap_add ht

Premises used: CStarAlgebra.convexOn_ringInverse_algebraMap_add, ConvexOn.smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
this :
  ∀ (ha : 0 ≤ a) ⦃b : A⦄,
    Membership.mem (γ := Set A) (Ici 0) b →
      a ≤ b → cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
⊢ Membership.mem (γ := Set A) (Ici 0) a →
    ∀ ⦃b : A⦄,
      Membership.mem (γ := Set A) (Ici 0) b →
        a ≤ b → cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b

Tactic:
(ha : 0 ≤ a)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
this :
  ∀ (hb : 0 ≤ b),
    a ≤ b → cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
⊢ Membership.mem (γ := Set A) (Ici 0) b →
    a ≤ b → cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b

Tactic:
(hb : 0 ≤ b)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
rw rw₁ :
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]

Premises used: CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
hb₁ :
  cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
⊢ t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
hb₁ :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 p * (1⁻¹ - (1 + x)⁻¹)) (t⁻¹ • a) ≤
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 p * (1⁻¹ - (1 + x)⁻¹)) (t⁻¹ • b)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)

Tactic:
unfold rpowIntegrand₀₁

Premises used: Real.rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
hb₁ :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • a) ≤
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • b)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 p * (1⁻¹ - (1 + x)⁻¹)) (t⁻¹ • a) ≤
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 p * (1⁻¹ - (1 + x)⁻¹)) (t⁻¹ • b)

Tactic:
simp only [Real.one_rpow, one_mul, inv_one]

Premises used: inv_one, Real.one_rpow, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
ha₁ : 0 ≤ t⁻¹
⊢ t⁻¹ • a ≤ t⁻¹ • b

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
hb₁ : 0 ≤ t⁻¹ • a
hb₂ : 0 ≤ t⁻¹ • b
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • a) ≤
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • b)

Tactic:
refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)

Premises used: CFC.monotoneOn_one_sub_one_add_inv_real
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ 0 ≤ t⁻¹ • a

Tactic:
positivity