Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.lintegral_rpow_of_gt

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:362 to 373

Mathematical statement

Exact Lean statement

lemma lintegral_rpow_of_gt {β γ : ℝ} (hβ : 0 ≤ β) (hγ : -1 < γ) :
    ∫⁻ s : ℝ in Ioo 0 β, ENNReal.ofReal (s ^ γ) =
    ENNReal.ofReal (β ^ (γ + 1) / (γ + 1))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lintegral_rpow_of_gt {β γ : ℝ} (hβ : 0 ≤ β) (hγ : -1 < γ) :    ∫⁻ s : ℝ in Ioo 0 β, ENNReal.ofReal (s ^ γ) =    ENNReal.ofReal (β ^ (γ + 1) / (γ + 1)) := by  have hγ2 : 0 < γ + 1 := by linarith  rw [setLIntegral_congr Ioo_ae_eq_Ioc, ← ofReal_integral_eq_lintegral_ofReal]  · rw [← intervalIntegral.integral_of_le hβ, integral_rpow]    · rw [Real.zero_rpow hγ2.ne', sub_zero]    · exact Or.inl hγ  · apply (@intervalIntegral.intervalIntegrable_rpow' 0 β γ ?_).1    linarith  · filter_upwards [self_mem_ae_restrict measurableSet_Ioc]      with s hs using Real.rpow_nonneg hs.1.le γ