awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖(↑p : ℝ).rpowIntegrand₁₂ t z‖ ≤ ‖(↑p : ℝ).rpowIntegrand₁₂ t maxr‖
have h : (↑p : ℝ).rpowIntegrand₁₂ t z ≤ (↑p : ℝ).rpowIntegrand₁₂ t maxr
Tactic: rw [Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) hz'),
        Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) maxr_nonneg)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ (↑p : ℝ).rpowIntegrand₁₂ t z ≤ (↑p : ℝ).rpowIntegrand₁₂ t maxr
have h : z ≤ maxr
Tactic: refine monotoneOn_rpowIntegrand₁₂ (by grind) (by grind) hz' maxr_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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))
⊢ 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 ∂μ
have hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
Tactic: have hbound : ∀ᵐ t ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
    intro z hz
    have hz' : 0 ≤ z := by grind
    unfold bound f
    rw [Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) hz'),
        Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) maxr_nonneg)]
    refine monotoneOn_rpowIntegrand₁₂ (by grind) (by grind) hz' maxr_nonneg ?_
    exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ HasFiniteIntegral bound (μ.restrict (Ioi 0))
have rw : HasFiniteIntegral (ε := ℝ) (fun (t : ℝ) ↦ f t maxr) (μ.restrict (Ioi 0))
Tactic: rw [hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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
⊢ 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 ∂μ
have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
Tactic: have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0)) := by
    rw [hasFiniteIntegral_norm_iff]
    exact (hμ maxr maxr_nonneg).1.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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))
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t), (↑p : ℝ).rpowIntegrand₁₂ t 0 = 0
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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))
⊢ 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 ∂μ
have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
Tactic: have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₁₂ p x 0 = 0 := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
    simp [rpowIntegrand₁₂_zero ht]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
⊢ 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 ∂μ
have refine : IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a) (Ioi 0) μ
Tactic: refine ⟨?integrable, ?integral⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
refine :
  IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a) (Ioi 0) μ
⊢ 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 ∂μ
have refine₁ : a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ
Tactic: refine ⟨?integrable, ?integral⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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 ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
have rw : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a =
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
Tactic: rw [CFC.nnrpow_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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 := 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
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow p) : ℝ)) a =
  cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a
Tactic: rw [cfcₙ_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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 (x : ℝ) ↦ (↑(x.toNNReal.nnrpow p) : ℝ)) a =
    cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a
have refine : ∀ (r : ℝ) (hr : r ∈ quasispectrum ℝ a),
  (↑(r.toNNReal.nnrpow p) : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ
Tactic: refine cfcₙ_congr fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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
r : ℝ
hr : r ∈ quasispectrum ℝ a
⊢ (↑(r.toNNReal.nnrpow p) : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ
have hr' : 0 ≤ r
Tactic: have hr' : 0 ≤ r := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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
r : ℝ
hr : r ∈ quasispectrum ℝ a
hr' : 0 ≤ r
⊢ (↑(r.toNNReal.nnrpow p) : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ
have simp : r ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ
Tactic: simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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 ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ
have a₁ : a ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) 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