feat: remove completeness assumption in Sobolev inequality (#14262)

sgouezel · sgouezel · commit 03cf1129cb3d · 2024-06-29T17:35:34.000Z
diff --git a/Mathlib/Analysis/Normed/Group/Completion.lean b/Mathlib/Analysis/Normed/Group/Completion.lean
@@ -43,6 +43,10 @@ instance [SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E) where
       exact Continuous.comp Completion.continuous_extension continuous_sub
     · rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]
 
+@[simp]
+theorem nnnorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖₊ = ‖x‖₊ := by
+  simp [nnnorm]
+
 end Completion
 
 end UniformSpace
diff --git a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
@@ -1022,6 +1022,24 @@ theorem _root_.HasCompactSupport.integral_Iic_deriv_eq (hf : ContDiff ℝ 1 f)
   rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f
   exact h2f.filter_mono _root_.atBot_le_cocompact |>.tendsto
 
+open UniformSpace in
+lemma _root_.HasCompactSupport.ennnorm_le_lintegral_Ici_deriv
+    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {f : ℝ → F} (hf : ContDiff ℝ 1 f) (h'f : HasCompactSupport f) (x : ℝ) :
+    (‖f x‖₊ : ℝ≥0∞) ≤ ∫⁻ y in Iic x, ‖deriv f y‖₊ := by
+  let I : F →L[ℝ] Completion F := Completion.toComplL
+  let f' : ℝ → Completion F := I ∘ f
+  have hf' : ContDiff ℝ 1 f' := hf.continuousLinearMap_comp I
+  have h'f' : HasCompactSupport f' := h'f.comp_left rfl
+  have : (‖f' x‖₊ : ℝ≥0∞) ≤ ∫⁻ y in Iic x, ‖deriv f' y‖₊ := by
+    rw [← HasCompactSupport.integral_Iic_deriv_eq hf' h'f' x]
+    exact ennnorm_integral_le_lintegral_ennnorm _
+  convert this with y
+  · simp [f', I, Completion.nnnorm_coe]
+  · rw [fderiv.comp_deriv _ I.differentiableAt (hf.differentiable le_rfl _)]
+    simp only [ContinuousLinearMap.fderiv]
+    simp [I]
+
 end IicFTC
 
 section UnivFTC
diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -263,11 +263,13 @@ theorem lintegral_mul_prod_lintegral_pow_le {p : ℝ} (hp₀ : 0 ≤ p)
 
 /-- Special case of the grid-lines lemma `lintegral_mul_prod_lintegral_pow_le`, taking the extremal
 exponent `p = (#ι - 1)⁻¹`. -/
-theorem lintegral_prod_lintegral_pow_le [Nontrivial ι]
+theorem lintegral_prod_lintegral_pow_le
     {p : ℝ} (hp : Real.IsConjExponent #ι p)
     {f} (hf : Measurable f) :
     ∫⁻ x, ∏ i, (∫⁻ xᵢ, f (update x i xᵢ) ∂μ i) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) ∂.pi μ
     ≤ (∫⁻ x, f x ∂.pi μ) ^ p := by
+  have : Nontrivial ι :=
+    Fintype.one_lt_card_iff_nontrivial.mp (by exact_mod_cast hp.one_lt)
   have h0 : (1:ℝ) < #ι := by norm_cast; exact Fintype.one_lt_card
   have h1 : (0:ℝ) < #ι - 1 := by linarith
   have h2 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
@@ -279,7 +281,7 @@ theorem lintegral_prod_lintegral_pow_le [Nontrivial ι]
 
 /-! ## The Gagliardo-Nirenberg-Sobolev inequality -/
 
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on `ℝⁿ`, for `n ≥ 2`.  (More literally we encode `ℝⁿ` as
@@ -299,8 +301,6 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux
   By taking the product over these `n` factors, raising them to the power `(n-1)⁻¹` and integrating,
   we get the inequality `∫ |u| ^ (n/(n-1)) ≤ ∫ x, ∏ i, (∫ xᵢ, |Du(update x i xᵢ)|)^(n-1)⁻¹`.
   The result then follows from the grid-lines lemma. -/
-  have : Nontrivial ι :=
-    Fintype.one_lt_card_iff_nontrivial.mp (by exact_mod_cast hp.one_lt)
   have : (1:ℝ) ≤ ↑#ι - 1 := by
     have hι : (2:ℝ) ≤ #ι := by exact_mod_cast hp.one_lt
     linarith
@@ -316,20 +316,18 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux
         simp_rw [prod_const, card_univ]
         norm_cast
     _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖₊) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
-    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p :=
+    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p := by
         -- apply the grid-lines lemma
-        lintegral_prod_lintegral_pow_le _ hp (by fun_prop)
+        apply lintegral_prod_lintegral_pow_le _ hp
+        have : Continuous (fderiv ℝ u) := hu.continuous_fderiv le_rfl
+        fun_prop
   -- we estimate |u x| using the fundamental theorem of calculus.
   gcongr with x i
   calc (‖u x‖₊ : ℝ≥0∞)
-      = (‖∫ xᵢ in Iic (x i), deriv (u ∘ update x i) xᵢ‖₊ : ℝ≥0∞) := by
-        -- apply the half-infinite fundamental theorem of calculus
-        have h3u : ContDiff ℝ 1 (u ∘ update x i) := hu.comp (by convert contDiff_update 1 x i)
-        have h4u : HasCompactSupport (u ∘ update x i) :=
-          h2u.comp_closedEmbedding (closedEmbedding_update x i)
-        simp [HasCompactSupport.integral_Iic_deriv_eq h3u h4u (x i)]
-    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖₊ :=
-        ennnorm_integral_le_lintegral_ennnorm _ -- apply the triangle inequality
+    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖₊ := by
+        apply le_trans (by simp) (HasCompactSupport.ennnorm_le_lintegral_Ici_deriv _ _ _)
+        · exact hu.comp (by convert contDiff_update 1 x i)
+        · exact h2u.comp_closedEmbedding (closedEmbedding_update x i)
     _ ≤ ∫⁻ xᵢ, (‖fderiv ℝ u (update x i xᵢ)‖₊ : ℝ≥0∞) := ?_
   gcongr with y; swap; exact Measure.restrict_le_self
   -- bound the derivative which appears
@@ -420,6 +418,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {u : E → F}
         * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂(volume : Measure (ι → ℝ)).map e.symm) ^ p := by
         congr
         rw [lintegral_map _ e.symm.continuous.measurable]
+        have : Continuous (fderiv ℝ u) := hu.continuous_fderiv le_rfl
         fun_prop
   rw [← ENNReal.mul_le_mul_left h3c ENNReal.coe_ne_top, ← mul_assoc, ← ENNReal.coe_mul, ← hC,
     ENNReal.coe_mul] at this
