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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
h : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 x) ((fun (x : ℝ) ↦ t⁻¹ • x) '' quasispectrum ℝ a)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
refine cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_

Premises used: Real.rpowIntegrand₀₁, cfcₙ_comp_smul, Inv.inv, OfNat.ofNat
-- 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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 x) ((fun (x : ℝ) ↦ t⁻¹ • x) '' quasispectrum ℝ a)

Tactic:
continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one |>.mono <|
            (h_mapsTo.mono_left hspec).image_subset

Premises used: Set.MapsTo.mono_left, zero_lt_one, Real.continuousOn_rpowIntegrand₀₁_Ici, ContinuousOn.mono, Set.MapsTo.image_subset
-- 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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 x) ((fun (x : ℝ) ↦ t⁻¹ • x) '' quasispectrum ℝ a)

Tactic:
exact continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one |>.mono <|
            (h_mapsTo.mono_left hspec).image_subset

Premises used: Set.MapsTo.mono_left, zero_lt_one, Real.continuousOn_rpowIntegrand₀₁_Ici, ContinuousOn.mono, Set.MapsTo.image_subset
-- 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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
calc :
  cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a
calc₁ :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a
calc₂ :
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) 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:
calc _ = cfcₙ (fun x => t ^ ((p : ℝ) - 1) * (rpowIntegrand₀₁ p 1 (t⁻¹ • x))) a := by
          refine cfcₙ_congr ?_
          refine Set.EqOn.mono hspec (rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one ht)
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (fun x => rpowIntegrand₀₁ p 1 (t⁻¹ • x)) a := by
          refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_
          refine ContinuousOn.mono ?_ hspec
          have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one
          fun_prop
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
          congr! 1
          refine cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_
          exact continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one |>.mono <|
            (h_mapsTo.mono_left hspec).image_subset

Premises used: cfcₙ, HMul.hMul, HSub.hSub, Real.rpowIntegrand₀₁, Inv.inv, HPow.hPow, HSMul.hSMul, OfNat.ofNat
-- 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
obtain :
  ∀ (μ : 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 ∂μ),
    ∃ (μ : Measure ℝ),
      ∀ (a : A),
        Membership.mem (γ := Set A) (Ici 0) a →
          IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a)
              (Ioi 0) μ ∧
            a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
⊢ ∃ (μ : Measure ℝ),
    ∀ (a : A),
      Membership.mem (γ := Set A) (Ici 0) a →
        IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
            μ ∧
          a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ

Tactic:
obtain ⟨μ, hμ⟩ := exists_measure_rpow_eq_integral_rpowIntegrand₀₁ hp

Premises used: Real.exists_measure_rpow_eq_integral_rpowIntegrand₀₁
-- 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 ∂μ
⊢ ∃ (μ : Measure ℝ),
    ∀ (a : A),
      Membership.mem (γ := Set A) (Ici 0) a →
        IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
            μ ∧
          a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ

Tactic:
⟨μ, fun a (ha : 0 ≤ a) => ?_⟩

Premises used: Exists.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 ∂μ
refine :
  ∀ (a : A) (ha : 0 ≤ a),
    IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
⊢ ∃ (μ : Measure ℝ),
    ∀ (a : A),
      Membership.mem (γ := Set A) (Ici 0) a →
        IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
            μ ∧
          a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ

Tactic:
refine ⟨μ, fun a (ha : 0 ≤ a) => ?_⟩
-- 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
⊢ Nontrivial A

Tactic:
nontriviality A
-- 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
⊢ 0 < (↑p : ℝ)

Tactic:
exact_mod_cast hp.1

Premises used: 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
⊢ 0 < (↑p : ℝ)

Tactic:
have p_pos : 0 < (p : ℝ) := by exact_mod_cast hp.1
-- 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)
⊢ IsCompact (quasispectrum ℝ a)

Tactic:
grind
-- 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)
⊢ 0 ∈ quasispectrum ℝ a

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)
⊢ LE.le (α := ℝ) 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)
⊢ 0 ≤ maxr

Tactic:
have maxr_nonneg : 0 ≤ maxr :=
    le_csSup_of_le (b := 0) (IsCompact.bddAbove (by grind)) (by simp) (by 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‖
⊢ ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))

Tactic:
continuousOn_rpowIntegrand₀₁_uncurry hp (quasispectrum ℝ a) ?_

Premises used: Real.continuousOn_rpowIntegrand₀₁_uncurry, Real, quasispectrum, 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‖
refine : quasispectrum ℝ a ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))

Tactic:
refine continuousOn_rpowIntegrand₀₁_uncurry hp (quasispectrum ℝ a) ?_

Premises used: Real.continuousOn_rpowIntegrand₀₁_uncurry, Real, quasispectrum
-- 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‖
⊢ quasispectrum ℝ a ⊆ Ici 0

Tactic:
grind
-- 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‖
⊢ ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))

Tactic:
have hf : ContinuousOn (Function.uncurry f) (Ioi (0 : ℝ) ×ˢ quasispectrum ℝ a) := by
    refine continuousOn_rpowIntegrand₀₁_uncurry hp (quasispectrum ℝ a) ?_
    grind
-- 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))
h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
⊢ ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.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
⊢ 0 ≤ z

Tactic:
grind
-- 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
⊢ 0 ≤ z

Tactic:
have hz' : 0 ≤ z := by grind