Source indexedlemma · leanprover/lean4:v4.32.0

ChoiceScale.d_eq_top_top

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:263 to 271

Mathematical statement

Exact Lean statement

lemma d_eq_top_top (hq₀ : 0 < q₀) (hq₀q₁ : q₀ ≠ q₁) (hp₁' : p₁ = ⊤) (hq₁' : q₁ = ⊤) :
    @d α ε m p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f = C₁

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma d_eq_top_top (hq₀ : 0 < q₀) (hq₀q₁ : q₀ ≠ q₁) (hp₁' : p₁ = ⊤) (hq₁' : q₁ = ⊤) :    @d α ε m p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f = C₁ := by  unfold d  rw [hp₁', hq₁']  simp only [inv_top, toReal_zero, zero_sub, zero_div, ENNReal.rpow_zero, mul_zero, mul_one,    zero_mul, one_div]  rw [div_neg, div_eq_mul_inv, mul_inv_cancel₀]  · rw [ENNReal.rpow_neg, ENNReal.rpow_one, inv_inv]  · exact (toReal_pos (ENNReal.inv_ne_zero.mpr (hq₁' ▸ hq₀q₁)) (by finiteness)).ne'