From 53b3b7bccaf8dd569fe1c34b65c53ffa642b98c4 Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Sat, 19 Oct 2024 23:49:47 +0800 Subject: [PATCH] fix --- Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean index 2cb20696e3a4a..24517a7d729a6 100644 --- a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean +++ b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean @@ -537,8 +537,7 @@ theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner {u : E → F'} have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by refine lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top (NNReal.coe_pos_iff_ne_zero.mpr h0p') ?_ |>.ne - dsimp only - rw [NNReal.val_eq_coe, ← eLpNorm_nnreal_eq_eLpNorm' h0p'] + rw [← eLpNorm_nnreal_eq_eLpNorm' h0p'] exact hu.continuous.memℒp_of_hasCompactSupport (μ := μ) h2u |>.eLpNorm_lt_top have h5u : (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ 0 := ENNReal.rpow_pos (pos_iff_ne_zero.mpr h3u) h4u |>.ne'