awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
this :
  Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    0
rw :
  x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹ *
      (x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)
rw₁ :
  x ^ p =
    (x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1) *
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
rw₂ :
  x ^ p =
    x ^ p *
      HMul.hMul (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
            p.rpowIntegrand₀₁ t 1)⁻¹
rw₃ : x ^ p = x ^ p * 1
rw₄ rw₅ : x ^ p = x ^ p
⊢ x ^ p =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x)

Tactic:
rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, mul_comm, mul_one, Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
case case₁ case₂ :
  ∀
    (this :
      Ne (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)
        0),
    x ^ p =
      HMul.hMul (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
            p.rpowIntegrand₀₁ t 1)⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t x)
⊢ x ^ p =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x)

Tactic:
case inr =>
    have : ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 ≠ 0 :=
      ne_of_gt <| integral_rpowIntegrand₀₁_one_pos hp
    rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]

Premises used: mul_assoc, mul_comm, mul_one, Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
rw :
  LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹

Tactic:
rw [inv_nonneg]

Premises used: inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)

Tactic:
le_of_lt <| integral_rpowIntegrand₀₁_one_pos hp

Premises used: le_of_lt, Real.integral_rpowIntegrand₀₁_one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)

Tactic:
exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos hp

Premises used: le_of_lt, Real.integral_rpowIntegrand₀₁_one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
⊢ ∃ (μ : 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 ∂μ

Tactic:
⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩

Premises used: MeasureTheory.MeasureSpace.volume, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
    IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) (HSMul.hSMul (β := Measure ℝ) C volume)
refine_2 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
    x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂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 ∂μ

Tactic:
refine ⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_1 :
  Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
    (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) ((HSMul.hSMul (β := Measure ℝ) C volume).restrict (Ioi 0))

Tactic:
rw [Measure.restrict_smul]

Premises used: MeasureTheory.Measure.restrict_smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
    (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))

Tactic:
Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₀₁_Ioi hp hx

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi, MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
    (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))

Tactic:
exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₀₁_Ioi hp hx

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi, MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hx : 0 ≤ x
ht : 0 < t
⊢ p.rpowIntegrand₁₂ t x = x * (p - 1).rpowIntegrand₀₁ t x

Tactic:
grind [rpowIntegrand₁₂, rpowIntegrand₀₁]

Premises used: Real.rpowIntegrand₀₁, Real.rpowIntegrand₁₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
pos : ∀ (ht' : 0 < t), 0 ≤ p.rpowIntegrand₁₂ t x
neg : ∀ (ht' : ¬0 < t), 0 ≤ p.rpowIntegrand₁₂ t x
⊢ 0 ≤ p.rpowIntegrand₁₂ t x

Tactic:
by_cases ht' : 0 < t
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
pos : 0 ≤ x * (p - 1).rpowIntegrand₀₁ t x
⊢ 0 ≤ p.rpowIntegrand₁₂ t x

Tactic:
rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht']

Premises used: Real.rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ x * (p - 1).rpowIntegrand₀₁ t x

Tactic:
mul_nonneg hx ?_

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
pos : 0 ≤ (p - 1).rpowIntegrand₀₁ t x
⊢ 0 ≤ x * (p - 1).rpowIntegrand₀₁ t x

Tactic:
refine mul_nonneg hx ?_

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 < p - 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ t

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : 0 < t
⊢ 0 ≤ (p - 1).rpowIntegrand₀₁ t x

Tactic:
exact rpowIntegrand₀₁_nonneg (by grind) (by grind) hx

Premises used: Real.rpowIntegrand₀₁_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬0 < t
⊢ t = 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬0 < t
⊢ t = 0

Tactic:
have ht' : t = 0 := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht'_1 : ¬0 < t
ht' : t = 0
⊢ p - 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht'_1 : ¬0 < t
ht' : t = 0
⊢ 0 ≤ p.rpowIntegrand₁₂ t x

Tactic:
simp [rpowIntegrand₁₂, ht', zero_rpow (by grind : p - 1 ≠ 0)]

Premises used: Real.zero_rpow, Real.rpowIntegrand₁₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
ht : 0 < t
⊢ p.rpowIntegrand₁₂ t 0 = 0

Tactic:
grind [rpowIntegrand₁₂]

Premises used: Real.rpowIntegrand₁₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
⊢ 0 ≤ p - 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ∀ (x : ℝ), x ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioi 1) p
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 + x.2 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
funProp₅ : ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 + x.2 ≠ 0
⊢ ContinuousOn (Y := ℝ) (Function.uncurry fun (t x : ℝ) ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1))
    (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
fun_prop (disch := grind)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
⊢ MonotoneOn (p.rpowIntegrand₁₂ t) (Ici 0)

Tactic:
MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm

Premises used: MonotoneOn.congr, Real.rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
refine : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)
⊢ MonotoneOn (p.rpowIntegrand₁₂ t) (Ici 0)

Tactic:
refine MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm

Premises used: MonotoneOn.congr, Real.rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
hg₀ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 ≤ (p - 1).rpowIntegrand₀₁ t x
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)

Tactic:
apply monotoneOn_id.mul

Premises used: MonotoneOn.mul, monotoneOn_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
⊢ MonotoneOn ((p - 1).rpowIntegrand₀₁ t) (Ici 0)

Tactic:
grind [rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg]

Premises used: Real.rpowIntegrand₀₁_monotoneOn, Real.rpowIntegrand₀₁_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 ≤ id x

Tactic:
grind [rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg]

Premises used: Real.rpowIntegrand₀₁_monotoneOn, Real.rpowIntegrand₀₁_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
ht : 0 < t
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 ≤ (p - 1).rpowIntegrand₀₁ t x

Tactic:
grind [rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg]

Premises used: Real.rpowIntegrand₀₁_monotoneOn, Real.rpowIntegrand₀₁_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
h : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioi 0) a), p.rpowIntegrand₁₂ a x = x * (p - 1).rpowIntegrand₀₁ a 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

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioi 0) a
h h₁ : x * (p - 1).rpowIntegrand₀₁ a x = x * (p - 1).rpowIntegrand₀₁ a x
⊢ p.rpowIntegrand₁₂ a x = x * (p - 1).rpowIntegrand₀₁ a x

Tactic:
rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]

Premises used: Real.rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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

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]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x)
    (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) (Ioi 0) volume

Tactic:
rw [integrableOn_congr_fun_ae hmain]

Premises used: MeasureTheory.integrableOn_congr_fun_ae
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
refine :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ (p - 1).rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioi 0))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x)
    (Ioi 0) volume

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
⊢ Membership.mem (γ := Set ℝ) (Ioo 0 1) (p - 1)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ (p - 1).rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioi 0))

Tactic:
exact integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
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)
⊢ 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)

Tactic:
rw [integral_congr_ae hmain, integral_const_mul_of_integrable
      (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx)]

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi, MeasureTheory.integral_congr_ae, integral_const_mul_of_integrable
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
⊢ p - 1 + 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
rw : x ^ p = x ^ (p - 1 + 1)
⊢ x ^ p = x * x ^ (p - 1)

Tactic:
rw [mul_comm, ← rpow_add_one' hx (by grind)]

Premises used: mul_comm, Real.rpow_add_one'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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 ^ (p - 1 + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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)

Tactic:
have h₁ : x ^ p = x * x ^ (p - 1) := by
    rw [mul_comm, ← rpow_add_one' hx (by grind)]
    simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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)
⊢ Membership.mem (γ := Set ℝ) (Ioo 0 1) (p - 1)

Tactic:
grind