Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.value_lintegral_res₁

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:1181 to 1192

Mathematical statement

Exact Lean statement

lemma value_lintegral_res₁ {γ p' : ℝ} {spf : ScaledPowerFunction} (ht : 0 < t) (ht' : t ≠ ∞) :
    (((spf_to_tc spf).inv t) ^ (γ + 1) / ENNReal.ofReal |γ + 1|) * (t ^ p') =
    (spf.d ^ (γ + 1) * t ^ (spf.σ⁻¹ * (γ + 1) + p') / ENNReal.ofReal |γ + 1|)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma value_lintegral_res₁ {γ p' : ℝ} {spf : ScaledPowerFunction} (ht : 0 < t) (ht' : t ≠ ∞) :    (((spf_to_tc spf).inv t) ^ (γ + 1) / ENNReal.ofReal |γ + 1|) * (t ^ p') =    (spf.d ^ (γ + 1) * t ^ (spf.σ⁻¹ * (γ + 1) + p') / ENNReal.ofReal |γ + 1|) := by  have := spf.hd  unfold spf_to_tc  dsimp only  rw [← ENNReal.mul_div_right_comm, ENNReal.mul_rpow_of_ne_zero, mul_assoc, ← ENNReal.rpow_mul,      ← ENNReal.rpow_add]  · positivity  · finiteness  · positivity  · exact (ENNReal.rpow_pos ht ht').ne'