awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ p.rpowIntegrand₁₂ t x
have pos : 0 ≤ x * (p - 1).rpowIntegrand₀₁ t x
Tactic: rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ x * (p - 1).rpowIntegrand₀₁ t x
have pos : 0 ≤ (p - 1).rpowIntegrand₀₁ t x
Tactic: refine mul_nonneg hx ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬0 < t
⊢ 0 ≤ p.rpowIntegrand₁₂ t x
have ht'₁ : t = 0
Tactic: have ht' : t = 0 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Y := ℝ) (Function.uncurry fun (t x : ℝ) ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1))
    (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have funProp : 0 ≤ p - 1
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
funProp : 0 ≤ p - 1
⊢ ContinuousOn (Y := ℝ) (Function.uncurry fun (t x : ℝ) ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1))
    (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have funProp₁ : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
funProp : 0 ≤ p - 1
funProp₁ : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
⊢ ContinuousOn (Y := ℝ) (Function.uncurry fun (t x : ℝ) ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1))
    (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have funProp₂ : ∀ (x : ℝ), x ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
funProp : 0 ≤ p - 1
funProp₁ : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
funProp₂ : ∀ (x : ℝ), x ≠ 0
⊢ ContinuousOn (Y := ℝ) (Function.uncurry fun (t x : ℝ) ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1))
    (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have funProp₃ : ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
funProp : 0 ≤ p - 1
funProp₁ : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
funProp₂ : ∀ (x : ℝ), x ≠ 0
funProp₃ : ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 ≠ 0
funProp₄ : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
⊢ ContinuousOn (Y := ℝ) (Function.uncurry fun (t x : ℝ) ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1))
    (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have funProp₅ : ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 + x.2 ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
⊢ MonotoneOn (p.rpowIntegrand₁₂ t) (Ici 0)
have refine : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)
Tactic: refine MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)
have hg : MonotoneOn ((p - 1).rpowIntegrand₀₁ t) (Ici 0)
Tactic: apply monotoneOn_id.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
hg : MonotoneOn ((p - 1).rpowIntegrand₀₁ t) (Ici 0)
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)
have hf₀ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 ≤ id x
Tactic: apply monotoneOn_id.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
hg : MonotoneOn ((p - 1).rpowIntegrand₀₁ t) (Ici 0)
hf₀ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 ≤ id x
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)
have hg₀ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 ≤ (p - 1).rpowIntegrand₀₁ t x
Tactic: apply monotoneOn_id.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
have h : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioi 0) a), p.rpowIntegrand₁₂ a x = x * (p - 1).rpowIntegrand₀₁ a x
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioi 0) a
⊢ p.rpowIntegrand₁₂ a x = x * (p - 1).rpowIntegrand₀₁ a x
have h : x * (p - 1).rpowIntegrand₀₁ a x = x * (p - 1).rpowIntegrand₀₁ a x
Tactic: rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) (Ioi 0) volume
have hmain : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x)
  fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
Tactic: have hmain : (rpowIntegrand₁₂ p · x)
      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) (Ioi 0) volume
have rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x) (Ioi 0)
  volume
Tactic: rw [integrableOn_congr_fun_ae hmain]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x)
    (Ioi 0) volume
have refine : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ (p - 1).rpowIntegrand₀₁ x_1 x)
  (Measure.restrict volume (Ioi 0))
Tactic: refine Integrable.const_mul ?_ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
⊢ x ^ p =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₁₂ t x)
have hmain : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x)
  fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
Tactic: have hmain : (rpowIntegrand₁₂ p · x)
      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₁₂ t x)
have rw : x ^ p =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
    (x *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ x_1 x)
Tactic: rw [integral_congr_ae hmain, integral_const_mul_of_integrable
      (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p = x * x ^ (p - 1)
have rw : x ^ p = x ^ (p - 1 + 1)
Tactic: rw [mul_comm, ← rpow_add_one' hx (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
      (x *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ x_1 x)
have h₁ : x ^ p = x * x ^ (p - 1)
Tactic: have h₁ : x ^ p = x * x ^ (p - 1) := by
    rw [mul_comm, ← rpow_add_one' hx (by grind)]
    simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
h₁ : x ^ p = x * x ^ (p - 1)
⊢ x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
      (x *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ x_1 x)
have rw : x *
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t x) =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
    (x *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ x_1 x)
Tactic: rw [h₁, rpow_eq_const_mul_integral (by grind) hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
have rw : LE.le (α := ℝ) 0
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (p - 1).rpowIntegrand₀₁ t 1)
Tactic: rw [inv_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
⊢ ∃ (μ : Measure ℝ),
    ∀ (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 ∂μ
have refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
  IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ
Tactic: refine ⟨μ, fun x hx => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
    IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ
⊢ ∃ (μ : Measure ℝ),
    ∀ (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 ∂μ
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x), x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ
Tactic: refine ⟨μ, fun x hx => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ
have refine_1 : Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) ((HSMul.hSMul (β := Measure ℝ) C volume).restrict (Ioi 0))
Tactic: unfold μ IntegrableOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) ((HSMul.hSMul (β := Measure ℝ) C volume).restrict (Ioi 0))
have refine_1 : Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x)
  (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))
Tactic: rw [Measure.restrict_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ
have refine_2 : HMul.hMul (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₁₂ t x) =
  HSMul.hSMul (β := ℝ) C
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x)
Tactic: rw [Measure.restrict_smul, integral_smul_nnreal_measure,
      rpow_eq_const_mul_integral_rpowIntegrand₁₂ hp hx]
-- 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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
have hspec : quasispectrum ℝ a ⊆ Ici 0
Tactic: have hspec : quasispectrum ℝ a ⊆ Ici 0 := by grind
-- 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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Membership.mem (γ := Set ℝ) (Ici 0) ((fun (x : ℝ) ↦ t⁻¹ • x) x)
have hx₁ : 0 ≤ x
Tactic: simp only [mem_Ici, smul_eq_mul] at hx ⊢
Cleared hypotheses: hx
-- 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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
have h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
Tactic: have h_mapsTo : MapsTo (t⁻¹ • · : ℝ → ℝ) (Ici 0) (Ici 0) := by
    intro x hx
    simp only [mem_Ici, smul_eq_mul] at hx ⊢
    positivity
-- 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
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)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a
have refine : EqOn (p.rpowIntegrand₀₁ t) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)
Tactic: refine cfcₙ_congr ?_
-- 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
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)
⊢ 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
have refine : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)
Tactic: refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_
-- 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
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 (t⁻¹ • x)) (quasispectrum ℝ a)
have refine : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)
Tactic: refine ContinuousOn.mono ?_ hspec
-- 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
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 (t⁻¹ • x)) (Ici 0)
have this : ContinuousOn (p.rpowIntegrand₀₁ 1) (Ici 0)
Tactic: have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one