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 0 1) 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
h_1 : Nontrivial A
p_pos : 0 < (↑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
h : ‖(↑p : ℝ).rpowIntegrand₀₁ t z‖ ≤ ‖(↑p : ℝ).rpowIntegrand₀₁ t maxr‖
⊢ ‖f t z‖ ≤ bound t

Tactic:
unfold bound f
-- 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 0 1) 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
h_1 : Nontrivial A
p_pos : 0 < (↑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
h : (↑p : ℝ).rpowIntegrand₀₁ t z ≤ (↑p : ℝ).rpowIntegrand₀₁ t maxr
⊢ ‖(↑p : ℝ).rpowIntegrand₀₁ t z‖ ≤ ‖(↑p : ℝ).rpowIntegrand₀₁ t maxr‖

Tactic:
rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) hz'),
        Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) maxr_nonneg)]

Premises used: le_of_lt, Real.rpowIntegrand₀₁_nonneg, Real.norm_of_nonneg
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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

Tactic:
rpowIntegrand₀₁_monotoneOn hp (le_of_lt ht) hz' maxr_nonneg ?_

Premises used: Real.rpowIntegrand₀₁_monotoneOn, le_of_lt, 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 0 1) 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
h_1 : Nontrivial A
p_pos : 0 < (↑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
h : z ≤ maxr
⊢ (↑p : ℝ).rpowIntegrand₀₁ t z ≤ (↑p : ℝ).rpowIntegrand₀₁ t maxr

Tactic:
refine rpowIntegrand₀₁_monotoneOn hp (le_of_lt ht) hz' maxr_nonneg ?_

Premises used: Real.rpowIntegrand₀₁_monotoneOn, le_of_lt
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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
⊢ z ≤ maxr

Tactic:
le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz

Premises used: quasispectrum.isCompact, IsCompact.bddAbove, le_csSup
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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
⊢ z ≤ maxr

Tactic:
exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz

Premises used: le_csSup
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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 : ℝ) ∂μ.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 p_pos (le_of_lt ht) hz'),
        Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) maxr_nonneg)]
    refine rpowIntegrand₀₁_monotoneOn hp (le_of_lt ht) hz' maxr_nonneg ?_
    exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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
rw : HasFiniteIntegral (ε := ℝ) (fun (t : ℝ) ↦ f t maxr) (μ.restrict (Ioi 0))
⊢ HasFiniteIntegral bound (μ.restrict (Ioi 0))

Tactic:
rw [hasFiniteIntegral_norm_iff]

Premises used: MeasureTheory.hasFiniteIntegral_norm_iff
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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 (ε := ℝ) (fun (t : ℝ) ↦ f t maxr) (μ.restrict (Ioi 0))

Tactic:
(hμ maxr maxr_nonneg).1.2

Premises used: And.right, And.left, 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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 (ε := ℝ) (fun (t : ℝ) ↦ f t maxr) (μ.restrict (Ioi 0))

Tactic:
exact (hμ maxr maxr_nonneg).1.2

Premises used: And.right, And.left
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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))

Tactic:
have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0)) := by
    rw [hasFiniteIntegral_norm_iff]
    exact (hμ maxr maxr_nonneg).1.2
-- 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 0 1) 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
h_1 : Nontrivial A
p_pos : 0 < (↑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))
h : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) a → (↑p : ℝ).rpowIntegrand₀₁ a 0 = 0
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₀₁ x 0 = 0

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi]

Premises used: MeasureTheory.ae_restrict_mem, 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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))
⊢ ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) a → (↑p : ℝ).rpowIntegrand₀₁ a 0 = 0

Tactic:
simp
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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

Tactic:
have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₀₁ p x 0 = 0 := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi]
    simp
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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 ∂μ

Tactic:
⟨?integrable, ?integral⟩

Premises used: And.intro
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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) μ
refine₁ : a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) 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 ∂μ

Tactic:
refine ⟨?integrable, ?integral⟩
-- 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 0 1) 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
h : Nontrivial A
p_pos : 0 < (↑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) μ

Tactic:
integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral

Premises used: measurableSet_Ioi, integrableOn_cfcₙ