awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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
⊢ ConcaveOn ℝ (Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
have 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)
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' ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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))
have 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))
Tactic: refine ConcaveOn.congr ?_ h₁.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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))
have refine : ConvexOn ℝ (β := A) (Ici 0) fun (x : A) ↦
  t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)
Tactic: refine ConcaveOn.sub (concaveOn_const _ (convex_Ici 0)) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ 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
have 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
Tactic: (ha : 0 ≤ a)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ Membership.mem (γ := Set A) (Ici 0) b →
    a ≤ b → cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
have this : ∀ (hb : 0 ≤ b),
  a ≤ b → cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
Tactic: (hb : 0 ≤ b)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
have rw : t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
have hb₁ : cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
have 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)
Tactic: unfold rpowIntegrand₀₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ 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)
have hb₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • a) ≤
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • b)
Tactic: simp only [Real.one_rpow, one_mul, inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ t⁻¹ • a ≤ t⁻¹ • b
have ha₁ : 0 ≤ t⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • a) ≤
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • b)
have hb₁ : 0 ≤ t⁻¹ • a
Tactic: refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • a) ≤
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (t⁻¹ • b)
have hb₂ : 0 ≤ t⁻¹ • b
Tactic: refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) =
    cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
have rw : t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) =
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
Tactic: rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
have _ : cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
Tactic: calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
_ :
  cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
have _₁ : t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
Tactic: calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
_ :
  cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
_₁ :
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
have _₂ : t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) =
  cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
Tactic: calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
have hf : ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
Tactic: apply concaveOn_cfcₙ_of_concaveOn_cfc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
have hf : Convex.{0, u_1} ℝ (E := Unitization ℂ A) (Unitization.inr '' Ici 0)
Tactic: refine ConcaveOn.subset (concaveOn_cfc_rpowIntegrand₀₁ hp ht) inr_map_Ici_zero ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
⊢ 0 < HPow.hPow (β := ℝ) x 0
have rw : LT.lt (α := ℝ≥0) 0 1
Tactic: rw [rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
have rw : (↑x : ℝ) ^ y = (↑0 : ℝ) ↔ (↑x : ℝ) = 0 ∧ y ≠ 0
Tactic: rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0) 0 y = if y = 0 then 1 else 0
have pos : ∀ (h : y = 0), HPow.hPow (α := ℝ≥0) 0 y = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
pos : ∀ (h : y = 0), HPow.hPow (α := ℝ≥0) 0 y = 1
⊢ HPow.hPow (α := ℝ≥0) 0 y = if y = 0 then 1 else 0
have neg : ∀ (h : ¬y = 0), HPow.hPow (α := ℝ≥0) 0 y = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℤ
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
have ofNat : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℤ
ofNat : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
have negSucc : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.negSucc a) : ℝ) = x ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have a : (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
n : ℤ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
n : ℕ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
n : ℤ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have a : (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
n : ℕ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have a : (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : y + 1 ≠ 0
x : ℝ≥0
⊢ x ^ (y + 1) = x ^ y * x
have rw : x ^ y * HPow.hPow (β := ℝ) x 1 = x ^ y * x
Tactic: rw [rpow_add' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : y + 1 ≠ 0
x : ℝ≥0
rw : x ^ y * HPow.hPow (β := ℝ) x 1 = x ^ y * x
⊢ x ^ (y + 1) = x ^ y * x
have rw₁ : x ^ y * x = x ^ y * x
Tactic: rw [rpow_add' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : 1 + y ≠ 0
x : ℝ≥0
⊢ x ^ (1 + y) = x * x ^ y
have rw : HPow.hPow (β := ℝ) x 1 * x ^ y = x * x ^ y
Tactic: rw [rpow_add' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : 1 + y ≠ 0
x : ℝ≥0
rw : HPow.hPow (β := ℝ) x 1 * x ^ y = x * x ^ y
⊢ x ^ (1 + y) = x * x ^ y
have rw₁ : x * x ^ y = x * x ^ y
Tactic: rw [rpow_add' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z
have a : (↑(x ^ (y + z)) : ℝ) = (↑(x ^ y * x ^ z) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z
have h₁ : y + z ≠ 0
Tactic: rw [← h, rpow_add']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℕ
z : ℝ
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℕ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw₁ : (x ^ n) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
n : ℕ
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℤ
z : ℝ
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℤ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw₁ : (x ^ n) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
n : ℤ
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
n : ℤ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : y - 1 ≠ 0
x : ℝ≥0
⊢ x ^ (y - 1) = x ^ y / x
have rw : x ^ y / HPow.hPow (β := ℝ) x 1 = x ^ y / x
Tactic: rw [rpow_sub' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : y - 1 ≠ 0
x : ℝ≥0
rw : x ^ y / HPow.hPow (β := ℝ) x 1 = x ^ y / x
⊢ x ^ (y - 1) = x ^ y / x
have rw₁ : x ^ y / x = x ^ y / x
Tactic: rw [rpow_sub' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : 1 - y ≠ 0
x : ℝ≥0
⊢ x ^ (1 - y) = x / x ^ y
have rw : HPow.hPow (β := ℝ) x 1 / x ^ y = x / x ^ y
Tactic: rw [rpow_sub' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
h : 1 - y ≠ 0
x : ℝ≥0
rw : HPow.hPow (β := ℝ) x 1 / x ^ y = x / x ^ y
⊢ x ^ (1 - y) = x / x ^ y
have rw₁ : x / x ^ y = x / x ^ y
Tactic: rw [rpow_sub' h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ (1 / y) = x
have rw : x ^ (y * (1 / y)) = x
Tactic: rw [← rpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (y * (1 / y)) = x
have field_simp : HPow.hPow (β := ℝ) x 1 = x
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x
have rw : x ^ (1 / y * y) = x
Tactic: rw [← rpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (1 / y * y) = x
have field_simp : HPow.hPow (β := ℝ) x 1 = x
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) x = x ^ (1 / 2)
have refine : (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)
Tactic: refine NNReal.eq ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
⊢ (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)
have push_cast : √(↑x : ℝ) = (↑x : ℝ) ^ (1 / 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ List.prod (List.map (fun (x : ι) ↦ f x ^ r) l) = (List.map f l).prod ^ r
have rw : Eq (α := ℝ≥0) (List.prod (List.map (fun (x : ι) ↦ f x ^ r) l)) (List.prod (List.map ((fun (x : ℝ≥0) ↦ x ^ r) ∘ f) l))
Tactic: rw [← list_prod_map_rpow, List.map_map]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
l : List ℝ
hl : ∀ x ∈ l, 0 ≤ x
r : ℝ
⊢ List.prod (List.map (fun (x : ℝ) ↦ x ^ r) l) = l.prod ^ r
have lift : ∀ (l : List ℝ≥0), List.prod (List.map (fun (x : ℝ) ↦ x ^ r) (List.map toReal l)) = (List.map toReal l).prod ^ r
Tactic: lift l to List ℝ≥0 using hl
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
r : ℝ
l : List ℝ≥0
⊢ List.prod (List.map (fun (x : ℝ) ↦ x ^ r) (List.map toReal l)) = (List.map toReal l).prod ^ r
have this : (↑(List.prod (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)) : ℝ) = (↑(l.prod ^ r) : ℝ)
Tactic: have := congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.list_prod_map_rpow l r)