Source indexedlemma · leanprover/lean4:v4.32.0

ChoiceScale.d_eq_top_of_eq

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:252 to 261

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma d_eq_top_of_eq (hC₁ : 0 < C₁) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hq₀' : q₀ ≠ ⊤)(hp₀' : p₀ ≠ ⊤) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ = p₁) (hpp₀ : p = p₀) (hq₁' : q₁ = ⊤) :    @d α ε m p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f = C₁ * eLpNorm f p μ := by  rw [d_eq_top₁, ← hp₀p₁, hpp₀] <;> try assumption  on_goal 1 => rw [ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_rpow_inv, ENNReal.rpow_rpow_inv]  · exact (toReal_pos hp₀.ne' hp₀').ne'  · exact (toReal_pos hp₀.ne' hp₀').ne'  · positivity  · exact hp₀p₁ ▸ hp₀'  · exact hq₁' ▸ hq₀'