Source indexedlemma · leanprover/lean4:v4.32.0

ChoiceScale.d_eq_top₁

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:231 to 250

Mathematical statement

Exact Lean statement

lemma d_eq_top₁ (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ = ⊤)
    (hq₀q₁ : q₀ ≠ q₁) (hC₁ : 0 < C₁) :
    @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₁ (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ = ⊤)    (hq₀q₁ : q₀ ≠ q₁) (hC₁ : 0 < C₁) :    @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, zero_sub, zero_div, ENNReal.rpow_zero, mul_zero, mul_one,    one_div]  rw [div_neg, div_neg]  rw [mul_div_cancel_right₀]  · rw [div_eq_mul_inv, mul_inv_cancel₀, ENNReal.rpow_neg_one]    · rw [ENNReal.mul_rpow_of_nonneg]      · rw [ENNReal.rpow_rpow_inv, ← toReal_inv, ENNReal.mul_inv, inv_inv]        · rw [← ENNReal.rpow_neg_one, ← ENNReal.rpow_mul, toReal_inv, mul_neg, mul_one, neg_neg]        · left; exact ENNReal.inv_ne_zero.mpr coe_ne_top        · left; finiteness        · exact (exp_toReal_pos hp₁ hp₁').ne'      · positivity    · exact (inv_toReal_pos_of_ne_top hq₀ (hq₁' ▸ hq₀q₁)).ne'  · exact (inv_toReal_pos_of_ne_top hq₀ (hq₁' ▸ hq₀q₁)).ne'