awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
case :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
have case₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a
Tactic: case finite =>
    refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le
    case finitebound =>
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
      · linarith
      · exact zero_lt_one
    case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ 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 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioc 0 1 ∪ Ioi 1)
  volume
Tactic: rw [← Set.Ioc_union_Ioi_eq_Ioi zero_le_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have inl : ∀ (hx : LE.le (α := ℝ) 0 0),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 0) =
    HPow.hPow (α := ℝ) 0 p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
Tactic: obtain (rfl | hx) := hx.eq_or_lt
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
inl :
  ∀ (hx : LE.le (α := ℝ) 0 0),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 0) =
      HPow.hPow (α := ℝ) 0 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 x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have inr : ∀ (hx : 0 < x),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
Tactic: obtain (rfl | hx) := hx.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    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 x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have hft : Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop
Tactic: rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
hft : Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have hff' : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → HasDerivWithinAt (fun (x_2 : ℝ) ↦ x * x_2) x (Ioi x_1) x_1
Tactic: rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
hft : Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop
hff' : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → HasDerivWithinAt (fun (x_2 : ℝ) ↦ x * x_2) x (Ioi x_1) x_1
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have hg_cont : ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ((fun (x_1 : ℝ) ↦ x * x_1) '' Ioi 0)
Tactic: rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
hft : Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop
hff' : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → HasDerivWithinAt (fun (x_2 : ℝ) ↦ x * x_2) x (Ioi x_1) x_1
hg_cont : ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ((fun (x_1 : ℝ) ↦ x * x_1) '' Ioi 0)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have hg1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
  ((fun (x_1 : ℝ) ↦ x * x_1) '' Ici 0) volume
Tactic: rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
hft : Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop
hff' : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → HasDerivWithinAt (fun (x_2 : ℝ) ↦ x * x_2) x (Ioi x_1) x_1
hg_cont : ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ((fun (x_1 : ℝ) ↦ x * x_1) '' Ioi 0)
hg1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    ((fun (x_1 : ℝ) ↦ x * x_1) '' Ici 0) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have hg2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (x_1 : ℝ) ↦ ((fun (x_2 : ℝ) ↦ p.rpowIntegrand₀₁ x_2 x) ∘ fun (x_2 : ℝ) ↦ x * x_2) x_1 * x) (Ici 0) volume
Tactic: rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ (x * x_1) x * x)
    (Ici 0) volume
have hg2 : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0) volume
Tactic: rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have inr : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
  x ^ p *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1
Tactic: suffices ∫ t in Ioi 0, ((rpowIntegrand₀₁ p · x) ∘ (x * ·)) t * x =
      x ^ p * (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1) by
    rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
    · exact tendsto_id.const_mul_atTop hx
    · simpa using fun t _ ↦ hasDerivWithinAt_id t (Ioi t) |>.const_mul x
    · simpa [Set.image_mul_left_Ioi hx] using continuousOn_rpowIntegrand₀₁ hp hx.le
    · simpa [Set.image_mul_left_Ici hx] using integrableOn_rpowIntegrand₀₁_Ici hp hx.le
    · simp only [Function.comp]
      rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]
      exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have heqOn : EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
Tactic: have heqOn : EqOn (fun t => rpowIntegrand₀₁ p (x * t) x * x)
      (fun t => (rpowIntegrand₀₁ p t 1) * x ^ p) (Ioi 0) :=
    EqOn.mono Ioi_subset_Ici_self (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
heqOn :
  EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
have inr : HSMul.hSMul (α := ℝ)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1) (x ^ p) =
  x ^ p *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      p.rpowIntegrand₀₁ x 1
Tactic: simp only [Function.comp, setIntegral_congr_fun measurableSet_Ioi heqOn,
    ← smul_eq_mul (b := x ^ p), integral_smul_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
heqOn :
  EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
⊢ HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1)
      (x ^ p) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1
have inr : (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1) * x ^ p =
  x ^ p *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      p.rpowIntegrand₀₁ x 1
Tactic: rw [smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
heqOn :
  EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
inr :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1) * x ^ p =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1
⊢ HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1)
      (x ^ p) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1
have inr₁ : (x ^ p * @integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1) =
  x ^ p *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      p.rpowIntegrand₀₁ x 1
Tactic: rw [smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ -1 / (2 * (p - 1)) = 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1)
have rw : -1 / 2 / (p - 1) = 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1)
Tactic: rw [← div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)
have hp₁ : 0 < p ∧ p < 1
Tactic: push _ ∈ _ at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ p - 2 < -1
have linarith : -1 ≤ p - 2 → p - 1 + (-1 - (p - 2)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)
have rw : 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1) = 1 / 2 * (-HPow.hPow (α := ℝ) 1 (p - 2 + 1) / (p - 2 + 1))
Tactic: rw [integral_const_mul, integral_Ioi_rpow_of_lt (by linarith) zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      1 / 2 * t ^ (p - 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
have refine_1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      1 / 2 * t ^ (p - 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
have refine_2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume
refine_2 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      1 / 2 * t ^ (p - 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
have refine_3 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) x → 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume
have refine_1 : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 2)) (Measure.restrict volume (Ioi 1))
Tactic: refine Integrable.const_mul ?_ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 2)) (Measure.restrict volume (Ioi 1))
have hp₁ : 0 < p ∧ p < 1
Tactic: push _ ∈ _ at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
have refine_1 : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1
Tactic: refine setIntegral_mono_set (integrableOn_rpowIntegrand₀₁_Ioi hp zero_le_one) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
have refine_2 : Ioi 1 ≤ᶠ[ae (F := Measure ℝ) volume] Ioi 0
Tactic: refine setIntegral_mono_set (integrableOn_rpowIntegrand₀₁_Ioi hp zero_le_one) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1
have refine_1 : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t), LE.le (α := ℝ) (0 t) ((fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) t)
Tactic: refine ae_restrict_of_forall_mem measurableSet_Ioi fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ 0 < -1 / (2 * (p - 1))
have rw : 2 * (p - 1) < 0
Tactic: rw [neg_div, neg_pos, one_div_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ 2 * (p - 1) < 0
have hp₁ : 0 < p ∧ p < 1
Tactic: push _ ∈ _ at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 2 * (p - 1) < 0
have linarith : 0 ≤ 2 * (p - 1) → 2 * (p - 1) + (0 - 2 * (p - 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
linarith : 0 ≤ 2 * (p - 1) → 2 * (p - 1) + (0 - 2 * (p - 1)) = 0
⊢ 2 * (p - 1) < 0
have linarith₁ : 0 ≤ 2 * (p - 1) → GT.gt (α := ℝ) 2 0
Tactic: linarith