Source indexedlemma · leanprover/lean4:v4.32.0

ChoiceScale.d_eq_top₀

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:217 to 229

Mathematical statement

Exact Lean statement

lemma d_eq_top₀ (hp₀ : 0 < p₀) (hq₁ : 0 < q₁) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ = ⊤) (hq₀q₁ : q₀ ≠ q₁) :
    @d α ε m p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f =
    (↑C₀ ^ p₀.toReal * eLpNorm f p μ ^ p.toReal) ^ p₀.toReal⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma d_eq_top₀ (hp₀ : 0 < p₀) (hq₁ : 0 < q₁) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ = ⊤) (hq₀q₁ : q₀ ≠ q₁) :    @d α ε m p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f =    (↑C₀ ^ p₀.toReal * eLpNorm f p μ ^ p.toReal) ^ p₀.toReal⁻¹ := by  unfold d  rw [hq₀']  simp only [inv_top, toReal_zero, sub_zero, zero_div, ENNReal.rpow_zero, mul_zero, mul_one,    div_one]  rw [mul_div_cancel_right₀]  · rw [div_eq_mul_inv, mul_inv_cancel₀, ENNReal.rpow_one]    · rw [ENNReal.mul_rpow_of_nonneg (hz := by positivity), ENNReal.rpow_rpow_inv, toReal_inv]      exact (exp_toReal_pos hp₀ hp₀').ne'    · exact (inv_toReal_pos_of_ne_top hq₁ ((hq₀' ▸ hq₀q₁).symm)).ne'  · exact (inv_toReal_pos_of_ne_top hq₁ ((hq₀' ▸ hq₀q₁).symm)).ne'