From e315fa4a54fc846887118ed92f67cd89c3cc248f Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Mon, 10 Jun 2024 12:03:13 +0200
Subject: [PATCH 01/29] some lemmas

---
 Mathlib/Analysis/Calculus/ContDiff/Defs.lean    |  4 ++++
 .../SpecialFunctions/Pow/Continuity.lean        |  3 +++
 .../Analysis/SpecialFunctions/Pow/NNReal.lean   | 17 +++++++++++++++++
 Mathlib/Logic/Basic.lean                        |  6 ++++++
 4 files changed, 30 insertions(+)

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean
index 490d1195d8b98b..c7bc3a3ff0ed47 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean
@@ -1537,6 +1537,10 @@ theorem contDiff_succ_iff_hasFDerivAt {n : ℕ} :
     contDiffOn_succ_iff_hasFDerivWithin uniqueDiffOn_univ, Set.mem_univ, forall_true_left]
 #align cont_diff_succ_iff_has_fderiv contDiff_succ_iff_hasFDerivAt
 
+theorem contDiff_one_iff_hasFDerivAt : ContDiff 𝕜 1 f ↔
+    ∃ f' : E → E →L[𝕜] F, Continuous f' ∧ ∀ x, HasFDerivAt f (f' x) x := by
+  convert contDiff_succ_iff_hasFDerivAt using 4; simp
+
 /-! ### Iterated derivative -/
 
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
index 346d8cb187c42d..c4dfe149660a9b 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
@@ -248,6 +248,9 @@ theorem continuousAt_rpow_const (x : ℝ) (q : ℝ) (h : x ≠ 0 ∨ 0 < q) :
   · exact (continuous_id'.prod_mk continuous_const).continuousAt
 #align real.continuous_at_rpow_const Real.continuousAt_rpow_const
 
+@[fun_prop]
+theorem continuous_rpow_const {q : ℝ} (h : 0 < q) : Continuous (fun x : ℝ => x ^ q) :=
+  continuous_iff_continuousAt.mpr fun x ↦ continuousAt_rpow_const x q (.inr h)
 end Real
 
 section
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
index 3bea719cfd8faa..3f519e135f3dbb 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -82,6 +82,10 @@ theorem rpow_add' (x : ℝ≥0) {y z : ℝ} (h : y + z ≠ 0) : x ^ (y + z) = x
   NNReal.eq <| Real.rpow_add' x.2 h
 #align nnreal.rpow_add' NNReal.rpow_add'
 
+theorem rpow_add_of_nonneg (x : ℝ≥0) {y z : ℝ} (hy : 0 ≤ y) (hz : 0 ≤ z) :
+    x ^ (y + z) = x ^ y * x ^ z := by
+  ext; exact Real.rpow_add_of_nonneg x.2 hy hz
+
 /-- Variant of `NNReal.rpow_add'` that avoids having to prove `y + z = w` twice. -/
 lemma rpow_of_add_eq (x : ℝ≥0) (hw : w ≠ 0) (h : y + z = w) : x ^ w = x ^ y * x ^ z := by
   rw [← h, rpow_add']; rwa [h]
@@ -372,6 +376,9 @@ theorem orderIsoRpow_symm_eq (y : ℝ) (hy : 0 < y) :
     (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) (one_div_pos.2 hy) := by
   simp only [orderIsoRpow, one_div_one_div]; rfl
 
+theorem nnnorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : ‖x ^ y‖₊ = ‖x‖₊ ^ y := by
+  ext; exact Real.norm_rpow_of_nonneg hx
+
 end NNReal
 
 namespace ENNReal
@@ -533,6 +540,16 @@ theorem rpow_add {x : ℝ≥0∞} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) :
   simp [coe_rpow_of_ne_zero this, NNReal.rpow_add this]
 #align ennreal.rpow_add ENNReal.rpow_add
 
+theorem rpow_add_of_nonneg {x : ℝ≥0∞} (y z : ℝ) (hy : 0 ≤ y) (hz : 0 ≤ z) :
+    x ^ (y + z) = x ^ y * x ^ z := by
+  induction x using recTopCoe
+  · rcases hy.eq_or_lt with rfl|hy
+    · rw [rpow_zero, one_mul, zero_add]
+    rcases hz.eq_or_lt with rfl|hz
+    · rw [rpow_zero, mul_one, add_zero]
+    simp [top_rpow_of_pos, hy, hz, add_pos hy hz]
+  simp [coe_rpow_of_nonneg, hy, hz, add_nonneg hy hz, NNReal.rpow_add_of_nonneg _ hy hz]
+
 theorem rpow_neg (x : ℝ≥0∞) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹ := by
   cases' x with x
   · rcases lt_trichotomy y 0 with (H | H | H) <;>
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index 002592b8bbbd18..67d3f8ebe63bcc 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -1161,6 +1161,12 @@ theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀
   Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and
 #align ball_and_distrib forall₂_and
 
+theorem forall_and_left [Nonempty α] (q : Prop) (p : α → Prop) :
+    (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x) := by rw [forall_and, forall_const]
+
+theorem forall_and_right [Nonempty α] (p : α → Prop) (q : Prop) :
+    (∀ x, p x ∧ q) ↔ (∀ x, p x) ∧ q := by rw [forall_and, forall_const]
+
 theorem exists_mem_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h :=
   Iff.trans (exists_congr fun _ ↦ exists_or) exists_or
 #align bex_or_distrib exists_mem_or

From 0bb2c5daa79417ba7d0bb8c4401833af6e312cdf Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Tue, 25 Jun 2024 19:40:58 +0200
Subject: [PATCH 02/29] add more

---
 Mathlib.lean                                  |   1 +
 .../Analysis/InnerProductSpace/NormPow.lean   | 125 ++++++++++++++++++
 2 files changed, 126 insertions(+)
 create mode 100644 Mathlib/Analysis/InnerProductSpace/NormPow.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 90617714bd5e7d..51d7d551bfb89e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -984,6 +984,7 @@ import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 import Mathlib.Analysis.InnerProductSpace.LaxMilgram
 import Mathlib.Analysis.InnerProductSpace.LinearPMap
 import Mathlib.Analysis.InnerProductSpace.MeanErgodic
+import Mathlib.Analysis.InnerProductSpace.NormPow
 import Mathlib.Analysis.InnerProductSpace.OfNorm
 import Mathlib.Analysis.InnerProductSpace.Orientation
 import Mathlib.Analysis.InnerProductSpace.Orthogonal
diff --git a/Mathlib/Analysis/InnerProductSpace/NormPow.lean b/Mathlib/Analysis/InnerProductSpace/NormPow.lean
new file mode 100644
index 00000000000000..3601ca71c5dc0d
--- /dev/null
+++ b/Mathlib/Analysis/InnerProductSpace/NormPow.lean
@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2024 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Heather Macbeth
+-/
+import Mathlib.Analysis.InnerProductSpace.Calculus
+import Mathlib.Analysis.NormedSpace.Dual
+import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
+
+/-!
+# Properties about the powers of the norm
+
+In this file we prove that `x ↦ ‖x‖ ^ p` is continuously differentiable for
+an inner product space and for a real number `p > 1`.
+
+## Todo:
+* `x ↦ ‖x‖ ^ p` should be `C^n` for `p > n`.
+
+-/
+
+section ContDiffNormPow
+
+open Asymptotics Real Topology
+open scoped NNReal
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+theorem hasFDerivAt_norm_rpow (x : E) {p : ℝ} (hp : 1 < p) :
+    HasFDerivAt (fun x : E ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • innerSL ℝ x) x := by
+  by_cases hx : x = 0
+  · simp [hx]
+    have h2p : 0 < p - 1 := sub_pos.mpr hp
+    rw [HasFDerivAt, hasFDerivAtFilter_iff_isLittleO]
+    simp [zero_lt_one.trans hp |>.ne']
+    calc (fun x : E ↦ ‖x‖ ^ p) =
+      (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
+          ext x
+          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
+          ring_nf
+      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
+        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by norm_num).mpr ?_
+        convert continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
+        simp [h2p.ne']
+      _ =O[𝓝 0] id := by
+        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), Function.id_def, isBigO_refl]
+  · apply HasStrictFDerivAt.hasFDerivAt
+    convert (hasStrictFDerivAt_norm_sq x).rpow_const (p := p / 2) (by simp [hx]) using 0
+    simp_rw [← Real.rpow_natCast_mul (norm_nonneg _), nsmul_eq_smul_cast ℝ, smul_smul]
+    ring_nf -- doesn't close the goal?
+    congr! 2
+    ring
+
+theorem differentiable_norm_rpow {p : ℝ} (hp : 1 < p) :
+    Differentiable ℝ (fun x : E ↦ ‖x‖ ^ p) :=
+  fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt
+
+theorem hasDerivAt_norm_rpow (x : ℝ) {p : ℝ} (hp : 1 < p) :
+    HasDerivAt (fun x : ℝ ↦ ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x := by
+  convert hasFDerivAt_norm_rpow x hp |>.hasDerivAt using 1; simp
+
+theorem hasDerivAt_abs_rpow (x : ℝ) {p : ℝ} (hp : 1 < p) :
+    HasDerivAt (fun x : ℝ ↦ |x| ^ p) (p * |x| ^ (p - 2) * x) x := by
+  simpa using hasDerivAt_norm_rpow x hp
+
+theorem fderiv_norm_rpow (x : E) {p : ℝ} (hp : 1 < p) :
+    fderiv ℝ (fun x ↦ ‖x‖ ^ p) x = (p * ‖x‖ ^ (p - 2)) • innerSL ℝ x :=
+  hasFDerivAt_norm_rpow x hp |>.fderiv
+
+theorem Differentiable.fderiv_norm_rpow {f : F → E} (hf : Differentiable ℝ f)
+    {x : F} {p : ℝ} (hp : 1 < p) :
+    fderiv ℝ (fun x ↦ ‖f x‖ ^ p) x =
+    (p * ‖f x‖ ^ (p - 2)) • (innerSL ℝ (f x)).comp (fderiv ℝ f x) :=
+  hasFDerivAt_norm_rpow (f x) hp |>.comp x (hf x).hasFDerivAt |>.fderiv
+
+theorem norm_fderiv_norm_rpow_le {f : F → E} (hf : Differentiable ℝ f) {x : F}
+    {p : ℝ} (hp : 1 < p) :
+    ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ p) x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖ := by
+  rw [hf.fderiv_norm_rpow hp, norm_smul, norm_mul]
+  simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
+    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc]
+  gcongr _ * ?_
+  refine mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le ..) (by positivity)
+    |>.trans_eq ?_
+  rw [innerSL_apply_norm, ← mul_assoc, ← Real.rpow_add_one' (by positivity) (by linarith)]
+  ring_nf
+
+theorem norm_fderiv_norm_id_rpow (x : E) {p : ℝ} (hp : 1 < p) :
+    ‖fderiv ℝ (fun x ↦ ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1) := by
+  rw [fderiv_norm_rpow x hp, norm_smul, norm_mul]
+  simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
+    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc, innerSL_apply_norm]
+  rw [← Real.rpow_add_one' (by positivity) (by linarith)]
+  ring_nf
+
+theorem nnnorm_fderiv_norm_rpow_le {f : F → E} (hf : Differentiable ℝ f)
+    {x : F} {p : ℝ≥0} (hp : 1 < p) :
+    ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ (p : ℝ)) x‖₊ ≤ p * ‖f x‖₊ ^ ((p : ℝ) - 1) * ‖fderiv ℝ f x‖₊ :=
+  norm_fderiv_norm_rpow_le hf hp
+
+theorem contDiff_norm_rpow {p : ℝ} (hp : 1 < p) : ContDiff ℝ 1 (fun x : E ↦ ‖x‖ ^ p) := by
+  rw [contDiff_one_iff_fderiv]
+  refine ⟨fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt, ?_⟩
+  simp_rw [continuous_iff_continuousAt]
+  intro x
+  by_cases hx : x = 0
+  · simp [hx, ContinuousAt, fderiv_norm_rpow (E := E) (x := 0) hp]
+    rw [tendsto_zero_iff_norm_tendsto_zero]
+    refine tendsto_of_tendsto_of_tendsto_of_le_of_le (tendsto_const_nhds) ?_
+      (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_fderiv_norm_id_rpow _ hp |>.le)
+    suffices ContinuousAt (fun x : E ↦ p * ‖x‖ ^ (p - 1)) 0  by
+      simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this
+    fun_prop (discharger := simp [*])
+  · simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]
+    fun_prop (discharger := simp [*])
+
+theorem ContDiff.norm_rpow {f : F → E} (hf : ContDiff ℝ 1 f) {p : ℝ} (hp : 1 < p) :
+    ContDiff ℝ 1 (fun x ↦ ‖f x‖ ^ p) :=
+  contDiff_norm_rpow hp |>.comp hf
+
+theorem Differentiable.norm_rpow {f : F → E} (hf : Differentiable ℝ f) {p : ℝ} (hp : 1 < p) :
+    Differentiable ℝ (fun x ↦ ‖f x‖ ^ p) :=
+  contDiff_norm_rpow hp |>.differentiable le_rfl |>.comp hf
+
+end ContDiffNormPow

From 5d8db3d8598d35be11e401f9141db0c30967304d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 17:14:59 +0200
Subject: [PATCH 03/29] various lemmas

---
 Mathlib/Analysis/Calculus/FDeriv/Basic.lean   |  4 +++
 .../Analysis/Normed/Group/Constructions.lean  | 12 ++++++++
 .../Analysis/SpecialFunctions/Pow/Real.lean   |  4 +++
 Mathlib/Data/ENNReal/Inv.lean                 | 16 ++++++++++
 Mathlib/Data/ENNReal/Operations.lean          |  4 +--
 Mathlib/Data/Set/Prod.lean                    |  5 ++++
 .../Function/LpSeminorm/Basic.lean            | 29 ++++++++++++++-----
 Mathlib/MeasureTheory/Function/LpSpace.lean   | 20 +++++++++++++
 .../Function/UniformIntegrable.lean           |  2 +-
 Mathlib/Topology/Separation.lean              | 12 ++++++++
 Mathlib/Topology/Support.lean                 | 11 +++++++
 11 files changed, 109 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
index 816a0ba2d3435b..f9d4f5feb7e2fd 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -1281,4 +1281,8 @@ protected theorem HasCompactSupport.fderiv (hf : HasCompactSupport f) :
   hf.mono' <| support_fderiv_subset 𝕜
 #align has_compact_support.fderiv HasCompactSupport.fderiv
 
+protected theorem HasCompactSupport.fderiv_apply (hf : HasCompactSupport f) (v : E) :
+    HasCompactSupport (fderiv 𝕜 f · v) :=
+  hf.fderiv 𝕜 |>.comp_left (g := fun L : E →L[𝕜] F ↦ L v) rfl
+
 end Support
diff --git a/Mathlib/Analysis/Normed/Group/Constructions.lean b/Mathlib/Analysis/Normed/Group/Constructions.lean
index c59986e6d92400..527f66b6473dd3 100644
--- a/Mathlib/Analysis/Normed/Group/Constructions.lean
+++ b/Mathlib/Analysis/Normed/Group/Constructions.lean
@@ -454,6 +454,18 @@ instance Pi.normedCommGroup [∀ i, NormedCommGroup (π i)] : NormedCommGroup (
 #align pi.normed_comm_group Pi.normedCommGroup
 #align pi.normed_add_comm_group Pi.normedAddCommGroup
 
+theorem Pi.nnnorm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (π i)] {i : ι} (y : π i) :
+    ‖Pi.single i y‖₊ = ‖y‖₊ := by
+  have H : ∀ b, ‖single i y b‖₊ = single (f := fun _ ↦ ℝ≥0) i ‖y‖₊ b := by
+    intro b
+    refine Pi.apply_single (fun i (x : π i) ↦ ‖x‖₊) ?_ i y b
+    simp
+  simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']
+
+theorem Pi.norm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (π i)] {i : ι} (y : π i) :
+    ‖Pi.single i y‖ = ‖y‖ :=
+  congr_arg Subtype.val <| Pi.nnnorm_single y
+
 end Pi
 
 /-! ### Multiplicative opposite -/
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
index 2c177c91065600..5d484d45c5e4b2 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@@ -263,6 +263,10 @@ theorem rpow_sub' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} (h : y - z ≠ 0) : x ^ (
   simp only [rpow_add' hx h, rpow_neg hx, div_eq_mul_inv]
 #align real.rpow_sub' Real.rpow_sub'
 
+protected theorem _root_.HasCompactSupport.rpow_const {α : Type*} [TopologicalSpace α] {f : α → ℝ}
+    (hf : HasCompactSupport f) {r : ℝ} (hr : r ≠ 0) : HasCompactSupport (fun x ↦ f x ^ r) :=
+  hf.comp_left (g := (· ^ r)) (Real.zero_rpow hr)
+
 end Real
 
 /-!
diff --git a/Mathlib/Data/ENNReal/Inv.lean b/Mathlib/Data/ENNReal/Inv.lean
index 4283ecc0ec9904..b438e7d8f1b903 100644
--- a/Mathlib/Data/ENNReal/Inv.lean
+++ b/Mathlib/Data/ENNReal/Inv.lean
@@ -154,6 +154,22 @@ protected theorem div_pos (ha : a ≠ 0) (hb : b ≠ ∞) : 0 < a / b :=
   ENNReal.mul_pos ha <| ENNReal.inv_ne_zero.2 hb
 #align ennreal.div_pos ENNReal.div_pos
 
+protected theorem inv_mul_le_iff {x y z : ℝ≥0∞} (h1 : x ≠ 0) (h2 : x ≠ ∞) :
+    x⁻¹ * y ≤ z ↔ y ≤ x * z := by
+  rw [← mul_le_mul_left h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]
+
+protected theorem mul_inv_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
+    x * y⁻¹ ≤ z ↔ x ≤ z * y := by
+  rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]
+
+protected theorem div_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
+    x / y ≤ z ↔ x ≤ z * y := by
+  rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]
+
+protected theorem div_le_iff' {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
+    x / y ≤ z ↔ x ≤ y * z := by
+  rw [mul_comm, ENNReal.div_le_iff h1 h2]
+
 protected theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) :
     (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
   induction' b with b
diff --git a/Mathlib/Data/ENNReal/Operations.lean b/Mathlib/Data/ENNReal/Operations.lean
index a1f4fec391c81f..f5c11dc910fb71 100644
--- a/Mathlib/Data/ENNReal/Operations.lean
+++ b/Mathlib/Data/ENNReal/Operations.lean
@@ -96,7 +96,7 @@ theorem mul_eq_mul_right : c ≠ 0 → c ≠ ∞ → (a * c = b * c ↔ a = b) :
 #align ennreal.mul_eq_mul_right ENNReal.mul_eq_mul_right
 
 -- Porting note (#11215): TODO: generalize to `WithTop`
-theorem mul_le_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : (a * b ≤ a * c ↔ b ≤ c) :=
+theorem mul_le_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b ≤ a * c ↔ b ≤ c :=
   (mul_left_strictMono h0 hinf).le_iff_le
 #align ennreal.mul_le_mul_left ENNReal.mul_le_mul_left
 
@@ -106,7 +106,7 @@ theorem mul_le_mul_right : c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤
 #align ennreal.mul_le_mul_right ENNReal.mul_le_mul_right
 
 -- Porting note (#11215): TODO: generalize to `WithTop`
-theorem mul_lt_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : (a * b < a * c ↔ b < c) :=
+theorem mul_lt_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b < a * c ↔ b < c :=
   (mul_left_strictMono h0 hinf).lt_iff_lt
 #align ennreal.mul_lt_mul_left ENNReal.mul_lt_mul_left
 
diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 06469a0cb68e2b..c66fe0d368114c 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -971,6 +971,11 @@ theorem update_preimage_pi [DecidableEq ι] {f : ∀ i, α i} (hi : i ∈ s)
       exact hf j hj h
 #align set.update_preimage_pi Set.update_preimage_pi
 
+theorem update_image [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) :
+    update x i '' s = Set.univ.pi (update (fun j ↦ {x j}) i s) := by
+  ext y
+  simp [update_eq_iff, and_left_comm (a := _ ∈ s), forall_update_iff, eq_comm (a := y _)]
+
 theorem update_preimage_univ_pi [DecidableEq ι] {f : ∀ i, α i} (hf : ∀ j ≠ i, f j ∈ t j) :
     update f i ⁻¹' pi univ t = t i :=
   update_preimage_pi (mem_univ i) fun j _ => hf j
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index 6cf3a09f8462d0..5494e638850458 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -88,11 +88,18 @@ theorem snorm_eq_snorm' (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α 
     snorm f p μ = snorm' f (ENNReal.toReal p) μ := by simp [snorm, hp_ne_zero, hp_ne_top]
 #align measure_theory.snorm_eq_snorm' MeasureTheory.snorm_eq_snorm'
 
+lemma snorm_nnreal_eq_snorm' {f : α → F} {p : ℝ≥0} (hp : p ≠ 0) : snorm f p μ = snorm' f p μ :=
+  snorm_eq_snorm' (by exact_mod_cast hp) ENNReal.coe_ne_top
+
 theorem snorm_eq_lintegral_rpow_nnnorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → F} :
     snorm f p μ = (∫⁻ x, (‖f x‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) ^ (1 / p.toReal) := by
   rw [snorm_eq_snorm' hp_ne_zero hp_ne_top, snorm']
 #align measure_theory.snorm_eq_lintegral_rpow_nnnorm MeasureTheory.snorm_eq_lintegral_rpow_nnnorm
 
+lemma snorm_nnreal_eq_lintegral {f : α → F} {p : ℝ≥0} (hp : p ≠ 0) :
+    snorm f p μ = (∫⁻ x, ‖f x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) :=
+  snorm_nnreal_eq_snorm' hp
+
 theorem snorm_one_eq_lintegral_nnnorm {f : α → F} : snorm f 1 μ = ∫⁻ x, ‖f x‖₊ ∂μ := by
   simp_rw [snorm_eq_lintegral_rpow_nnnorm one_ne_zero ENNReal.coe_ne_top, ENNReal.one_toReal,
     one_div_one, ENNReal.rpow_one]
@@ -115,11 +122,16 @@ theorem Memℒp.aestronglyMeasurable {f : α → E} {p : ℝ≥0∞} (h : Memℒ
 #align measure_theory.mem_ℒp.ae_strongly_measurable MeasureTheory.Memℒp.aestronglyMeasurable
 
 theorem lintegral_rpow_nnnorm_eq_rpow_snorm' {f : α → F} (hq0_lt : 0 < q) :
-    (∫⁻ a, (‖f a‖₊ : ℝ≥0∞) ^ q ∂μ) = snorm' f q μ ^ q := by
+    ∫⁻ a, (‖f a‖₊ : ℝ≥0∞) ^ q ∂μ = snorm' f q μ ^ q := by
   rw [snorm', ← ENNReal.rpow_mul, one_div, inv_mul_cancel, ENNReal.rpow_one]
   exact (ne_of_lt hq0_lt).symm
 #align measure_theory.lintegral_rpow_nnnorm_eq_rpow_snorm' MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'
 
+lemma snorm_nnreal_pow_eq_lintegral {f : α → F} {p : ℝ≥0} (hp : p ≠ 0) :
+    snorm f p μ ^ (p : ℝ) = ∫⁻ x, ‖f x‖₊ ^ (p : ℝ) ∂μ := by
+  simp [snorm_eq_snorm' (by exact_mod_cast hp) ENNReal.coe_ne_top,
+    lintegral_rpow_nnnorm_eq_rpow_snorm' (show 0 < (p : ℝ) from pos_iff_ne_zero.mpr hp)]
+
 end ℒpSpaceDefinition
 
 section Top
@@ -1013,9 +1025,9 @@ theorem snorm_const_smul (c : 𝕜) (f : α → F) :
 
 end NormedSpace
 
-theorem snorm_indicator_ge_of_bdd_below (hp : p ≠ 0) (hp' : p ≠ ∞) {f : α → F} (C : ℝ≥0) {s : Set α}
-    (hs : MeasurableSet s) (hf : ∀ᵐ x ∂μ, x ∈ s → C ≤ ‖s.indicator f x‖₊) :
-    C • μ s ^ (1 / p.toReal) ≤ snorm (s.indicator f) p μ := by
+theorem le_snorm_of_bddBelow (hp : p ≠ 0) (hp' : p ≠ ∞) {f : α → F} (C : ℝ≥0) {s : Set α}
+    (hs : MeasurableSet s) (hf : ∀ᵐ x ∂μ, x ∈ s → C ≤ ‖f x‖₊) :
+    C • μ s ^ (1 / p.toReal) ≤ snorm f p μ := by
   rw [ENNReal.smul_def, smul_eq_mul, snorm_eq_lintegral_rpow_nnnorm hp hp',
     ENNReal.le_rpow_one_div_iff (ENNReal.toReal_pos hp hp'),
     ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg, ← ENNReal.rpow_mul,
@@ -1023,13 +1035,15 @@ theorem snorm_indicator_ge_of_bdd_below (hp : p ≠ 0) (hp' : p ≠ ∞) {f : α
     ← lintegral_indicator _ hs]
   refine lintegral_mono_ae ?_
   filter_upwards [hf] with x hx
-  rw [nnnorm_indicator_eq_indicator_nnnorm]
   by_cases hxs : x ∈ s
   · simp only [Set.indicator_of_mem hxs] at hx ⊢
     gcongr
     exact hx hxs
   · simp [Set.indicator_of_not_mem hxs]
-#align measure_theory.snorm_indicator_ge_of_bdd_below MeasureTheory.snorm_indicator_ge_of_bdd_below
+#align measure_theory.snorm_indicator_ge_of_bdd_below MeasureTheory.le_snorm_of_bddBelow
+
+@[deprecated (since := "2024-06-26")]
+alias snorm_indicator_ge_of_bdd_below := le_snorm_of_bddBelow
 
 section RCLike
 
@@ -1114,7 +1128,8 @@ theorem ae_bdd_liminf_atTop_of_snorm_bdd {p : ℝ≥0∞} (hp : p ≠ 0) {f : 
 
 end Liminf
 
-/-- A continuous function with compact support belongs to `L^∞`. -/
+/-- A continuous function with compact support belongs to `L^∞`.
+See `Continuous.memℒp_of_hasCompactSupport` for a version for `L^p`. -/
 theorem _root_.Continuous.memℒp_top_of_hasCompactSupport
     {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
     {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) (μ : Measure X) : Memℒp f ⊤ μ := by
diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
index 749a8a6c486929..d7ddb8fdfbd567 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -752,6 +752,26 @@ protected lemma Memℒp.piecewise [DecidablePred (· ∈ s)] {g}
 
 end Indicator
 
+section Topology
+variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
+  {μ : Measure X} [IsFiniteMeasureOnCompacts μ]
+
+/-- A bounded measurable function with compact support is in L^p. -/
+theorem HasCompactSupport.memℒp_of_bound {f : X → E} (hf : HasCompactSupport f)
+    (h2f : AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : Memℒp f p μ := by
+  have := memℒp_top_of_bound h2f C hfC
+  exact this.memℒp_of_exponent_le_of_measure_support_ne_top
+    (fun x ↦ image_eq_zero_of_nmem_tsupport) (hf.measure_lt_top.ne) le_top
+
+/-- A continuous function with compact support is in L^p. -/
+theorem Continuous.memℒp_of_hasCompactSupport {f : X → E} (hf : Continuous f)
+    (h'f : HasCompactSupport f) : Memℒp f p μ := by
+  have := hf.memℒp_top_of_hasCompactSupport h'f μ
+  exact this.memℒp_of_exponent_le_of_measure_support_ne_top
+    (fun x ↦ image_eq_zero_of_nmem_tsupport) (h'f.measure_lt_top.ne) le_top
+
+end Topology
+
 section IndicatorConstLp
 
 open Set Function
diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
index e14ccb6cec0f2e..485679d5010493 100644
--- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
+++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
@@ -870,7 +870,7 @@ theorem UniformIntegrable.spec' (hp : p ≠ 0) (hp' : p ≠ ∞) (hf : ∀ i, St
           refine mul_le_mul' le_rfl
             (ENNReal.rpow_le_rpow (hℐ C).le (one_div_nonneg.2 ENNReal.toReal_nonneg))
         _ ≤ snorm ({ x | C ≤ ‖f (ℐ C) x‖₊ }.indicator (f (ℐ C))) p μ := by
-          refine snorm_indicator_ge_of_bdd_below hp hp' _
+          refine le_snorm_of_bddBelow hp hp' _
             (measurableSet_le measurable_const (hf _).nnnorm.measurable)
             (eventually_of_forall fun x hx => ?_)
           rwa [nnnorm_indicator_eq_indicator_nnnorm, Set.indicator_of_mem hx]
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 7fd22227b0f842..c0806a2027b29b 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1099,6 +1099,18 @@ theorem disjoint_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x
 
 #align topological_space.subset_trans embedding_inclusionₓ
 
+theorem closedEmbedding_update {ι : Type*} {β : ι → Type*}
+    [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)]
+    (x : (i : ι) → β i) (i : ι) {s : Set (β i)} [(i : ι) → T1Space (β i)] :
+    ClosedEmbedding (update x i) := by
+  apply closedEmbedding_of_continuous_injective_closed
+  · exact continuous_const.update i continuous_id
+  · exact update_injective x i
+  · intro s hs
+    rw [update_image]
+    apply isClosed_set_pi
+    simp [forall_update_iff, hs, isClosed_singleton]
+
 /-! ### R₁ (preregular) spaces -/
 
 section R1Space
diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean
index a7b4a459b31d53..aa5d34700aea14 100644
--- a/Mathlib/Topology/Support.lean
+++ b/Mathlib/Topology/Support.lean
@@ -400,6 +400,17 @@ theorem HasCompactSupport.mul_left (hf : HasCompactSupport f') : HasCompactSuppo
 
 end MulZeroClass
 
+section OrderedAddGroup
+
+variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [Lattice β]
+  [CovariantClass β β (· + ·) (· ≤ ·)]
+
+protected theorem HasCompactSupport.abs {f : α → β} (hf : HasCompactSupport f) :
+    HasCompactSupport |f| :=
+  hf.comp_left (g := abs) abs_zero
+
+end OrderedAddGroup
+
 end CompactSupport2
 
 section LocallyFinite

From d3c40856c92dd5a188a823bf1bece7be40cd44b6 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 17:22:38 +0200
Subject: [PATCH 04/29] two logic lemmas

---
 Mathlib/Logic/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index 5d763ba8c6d322..0d044e99bc9223 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -1157,6 +1157,12 @@ theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀
   Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and
 #align ball_and_distrib forall₂_and
 
+theorem forall_and_left [Nonempty α] (q : Prop) (p : α → Prop) :
+    (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x) := by rw [forall_and, forall_const]
+
+theorem forall_and_right [Nonempty α] (p : α → Prop) (q : Prop) :
+    (∀ x, p x ∧ q) ↔ (∀ x, p x) ∧ q := by rw [forall_and, forall_const]
+
 theorem exists_mem_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h :=
   Iff.trans (exists_congr fun _ ↦ exists_or) exists_or
 #align bex_or_distrib exists_mem_or

From 5258d7cb3d947249d9a6c244935aa78439b2bb66 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 17:24:20 +0200
Subject: [PATCH 05/29] remove logic lemmas

---
 Mathlib/Logic/Basic.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index 0d044e99bc9223..5d763ba8c6d322 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -1157,12 +1157,6 @@ theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀
   Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and
 #align ball_and_distrib forall₂_and
 
-theorem forall_and_left [Nonempty α] (q : Prop) (p : α → Prop) :
-    (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x) := by rw [forall_and, forall_const]
-
-theorem forall_and_right [Nonempty α] (p : α → Prop) (q : Prop) :
-    (∀ x, p x ∧ q) ↔ (∀ x, p x) ∧ q := by rw [forall_and, forall_const]
-
 theorem exists_mem_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h :=
   Iff.trans (exists_congr fun _ ↦ exists_or) exists_or
 #align bex_or_distrib exists_mem_or

From 19e92f8c3acd66d4bbaf1423e0505feef48e0434 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 18:24:53 +0200
Subject: [PATCH 06/29] fix

---
 Mathlib/Topology/Separation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index c0806a2027b29b..83b584b2c00a85 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1101,7 +1101,7 @@ theorem disjoint_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x
 
 theorem closedEmbedding_update {ι : Type*} {β : ι → Type*}
     [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)]
-    (x : (i : ι) → β i) (i : ι) {s : Set (β i)} [(i : ι) → T1Space (β i)] :
+    (x : (i : ι) → β i) (i : ι) [(i : ι) → T1Space (β i)] :
     ClosedEmbedding (update x i) := by
   apply closedEmbedding_of_continuous_injective_closed
   · exact continuous_const.update i continuous_id

From 5891d3ba742852baa43ef5a27600a0a4b6bd23de Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 19:55:09 +0200
Subject: [PATCH 07/29] prove sobolev inequality

---
 Mathlib.lean                                  |   1 +
 .../Integral/SobolevInequality.lean           | 619 ++++++++++++++++++
 2 files changed, 620 insertions(+)
 create mode 100644 Mathlib/MeasureTheory/Integral/SobolevInequality.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index ef922cb212bcd8..4c292ba53fc79c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3045,6 +3045,7 @@ import Mathlib.MeasureTheory.Integral.Pi
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Integral.SetToL1
+import Mathlib.MeasureTheory.Integral.SobolevInequality
 import Mathlib.MeasureTheory.Integral.TorusIntegral
 import Mathlib.MeasureTheory.Integral.VitaliCaratheodory
 import Mathlib.MeasureTheory.MeasurableSpace.Basic
diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
new file mode 100644
index 00000000000000..ef505d83803d18
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -0,0 +1,619 @@
+/-
+Copyright (c) 2022 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Heather Macbeth
+-/
+import Mathlib.Analysis.InnerProductSpace.Calculus
+import Mathlib.Data.Finset.Interval
+import Mathlib.MeasureTheory.Integral.IntegralEqImproper
+import Mathlib.Tactic.FunProp.AEMeasurable
+import Mathlib.Tactic.FunProp.ContDiff
+import Mathlib.Analysis.Calculus.Deriv.Pi
+import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+
+/-!
+# Gagliardo-Nirenberg-Sobolev inequality
+
+In this file we prove the Gagliardo-Nirenberg-Sobolev inequality.
+This states that for compactly supported `C¹`-functions between finite dimensional vector spaces,
+we can bound the `L^p`-norm of `u` by the `L^q` norm of the derivative of `u`.
+The bound is up to a constant that is independent of the function `u`.
+Let `n` be the dimension of the domain.
+
+## Main results
+
+* `MeasureTheory.snorm_le_snorm_fderiv_of_eq`:
+  The bound holds for `1 ≤ p < n` and `q⁻¹ = p⁻¹ - n⁻¹`
+* `MeasureTheory.snorm_le_snorm_fderiv_of_le`:
+  The bound holds when `1 ≤ p < n`, `0 ≤ q` and `p⁻¹ - n⁻¹ ≤ q⁻¹`.
+  Note that in this case the constant depends on the support of `u`.
+-/
+
+open scoped Classical BigOperators ENNReal NNReal Topology
+open Set Function Finset MeasureTheory Measure Filter
+
+noncomputable section
+
+variable {ι : Type*} [Fintype ι] [DecidableEq ι]
+
+local prefix:max "#" => Fintype.card
+
+/-! ## The grid-lines lemma -/
+
+variable {A : ι → Type*} [∀ i, MeasurableSpace (A i)]
+  (μ : ∀ i, Measure (A i)) [∀ i, SigmaFinite (μ i)]
+
+namespace MeasureTheory
+
+namespace GridLines
+
+/-- The "grid-lines operation" (not a standard name) which is central in the inductive proof of the
+Sobolev inequality.
+
+For a finite dependent product `Π i : ι, A i` of sigma-finite measure spaces, a finite set `s` of
+indices from `ι`, and a (later assumed nonnegative) real number `p`, this operation acts on a
+function `f` from `Π i, A i` into the extended nonnegative reals.  The operation is to partially
+integrate, in the `s` co-ordinates, the function whose value at `x : Π i, A i` is obtained by
+multiplying a certain power of `f` with the product, for each co-ordinate `i` in `s`, of a certain
+power of the integral of `f` along the "grid line" in the `i` direction through `x`.
+
+We are most interested in this operation when the set `s` is the universe in `ι`, but as a proxy for
+"induction on dimension" we define it for a general set `s` of co-ordinates: the `s`-grid-lines
+operation on a function `f` which is constant along the co-ordinates in `sᶜ` is morally (that is, up
+to type-theoretic nonsense) the same thing as the universe-grid-lines operation on the associated
+function on the "lower-dimensional" space `Π i : s, A i`. -/
+def T (p : ℝ) (f : (∀ i, A i) → ℝ≥0∞) (s : Finset ι) : (∀ i, A i) → ℝ≥0∞ :=
+  ∫⋯∫⁻_s, f ^ (1 - (s.card - 1 : ℝ) * p) * ∏ i in s, (∫⋯∫⁻_{i}, f ∂μ) ^ p ∂μ
+
+variable {p : ℝ}
+
+@[simp] lemma T_univ (f : (∀ i, A i) → ℝ≥0∞) (x : ∀ i, A i) :
+    T μ p f univ x =
+    ∫⁻ (x : ∀ i, A i), (f x ^ (1 - (#ι - 1 : ℝ) * p)
+    * ∏ i : ι, (∫⁻ t : A i, f (update x i t) ∂(μ i)) ^ p) ∂(.pi μ) := by
+  simp [T, lmarginal_univ, lmarginal_singleton, card_univ]
+
+@[simp] lemma T_empty (f : (∀ i, A i) → ℝ≥0∞) (x : ∀ i, A i) :
+    T μ p f ∅ x = f x ^ (1 + p) := by
+  simp [T]
+
+/-- The main inductive step in the grid-lines lemma for the Gagliardo-Nirenberg-Sobolev inequality.
+
+The grid-lines operation `GridLines.T` on a nonnegative function on a finitary product type is
+less than or equal to the grid-lines operation of its partial integral in one co-ordinate
+(the latter intuitively considered as a function on a space "one dimension down"). -/
+theorem T_insert_le_T_lmarginal_singleton (hp₀ : 0 ≤ p) (s : Finset ι)
+    (hp : (s.card : ℝ) * p ≤ 1)
+    (i : ι) (hi : i ∉ s) {f : (∀ i, A i) → ℝ≥0∞} (hf : Measurable f) :
+    T μ p f (insert i s) ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := by
+  calc T μ p f (insert i s)
+      = ∫⋯∫⁻_insert i s,
+            f ^ (1 - (s.card : ℝ) * p) * ∏ j in (insert i s), (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ := by
+          simp_rw [T, card_insert_of_not_mem hi]
+          congr!
+          push_cast
+          ring
+    _ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ (t : A i),
+            (f (update x i t) ^ (1 - (s.card : ℝ) * p)
+            * ∏ j in (insert i s), (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p)  ∂ (μ i)) ∂μ := by
+          rw [lmarginal_insert' _ _ hi]
+          · congr! with x t
+            simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
+          · change Measurable (fun x ↦ _)
+            simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
+            refine (hf.pow_const _).mul <| Finset.measurable_prod _ ?_
+            exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _
+    _ ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := lmarginal_mono (s:=s) (fun x ↦ ?_)
+  simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
+  have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (update x i t) :=
+    fun {_} ↦ hf.lmarginal μ |>.comp <| measurable_update _
+  have hF₀ : Measurable fun t ↦ f (update x i t) := hf.comp <| measurable_update _
+  let k : ℝ := s.card
+  have hk' : 0 ≤ 1 - k * p := by linarith only [hp]
+  let X := update x i
+  calc ∫⁻ t, f (X t) ^ (1 - k * p)
+          * ∏ j in (insert i s), (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂ (μ i)
+      = ∫⁻ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p)
+          * ∏ j in s, ((∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p)) ∂(μ i) := by
+              -- rewrite integrand so that `(∫⋯∫⁻_insert i s, f ∂μ) ^ p` comes first
+              clear_value X
+              congr! 2 with t
+              simp_rw [prod_insert hi]
+              ring_nf
+    _ = (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
+          ∫⁻ t, f (X t) ^ (1 - k * p) * ∏ j in s, ((∫⋯∫⁻_{j}, f ∂μ) (X t)) ^ p ∂(μ i) := by
+              -- pull out this constant factor
+              have : ∀ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x := by
+                intro t
+                rw [lmarginal_update_of_mem]
+                exact Iff.mpr Finset.mem_singleton rfl
+              simp_rw [this]
+              rw [lintegral_const_mul]
+              exact (hF₀.pow_const _).mul <| Finset.measurable_prod _ fun _ _ ↦ hF₁.pow_const _
+    _ ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
+          ((∫⁻ t, f (X t) ∂μ i) ^ (1 - k * p)
+          * ∏ j in s, (∫⁻ t, (∫⋯∫⁻_{j}, f ∂μ) (X t) ∂μ i) ^ p) := by
+              -- apply Hölder's inequality
+              gcongr
+              apply ENNReal.lintegral_mul_prod_norm_pow_le
+              · exact hF₀.aemeasurable
+              · intros
+                exact hF₁.aemeasurable
+              · simp only [sum_const, nsmul_eq_mul]
+                ring
+              · exact hk'
+              · exact fun _ _ ↦ hp₀
+    _ = (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
+          ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j in s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p) := by
+              -- absorb the newly-created integrals into `∫⋯∫`
+              congr! 2
+              · rw [lmarginal_singleton]
+              refine prod_congr rfl fun j hj => ?_
+              have hi' : i ∉ ({j} : Finset ι) := by
+                simp only [Finset.mem_singleton, Finset.mem_insert, Finset.mem_compl] at hj ⊢
+                exact fun h ↦ hi (h ▸ hj)
+              rw [lmarginal_insert _ hf hi']
+    _ = (∫⋯∫⁻_{i}, f ∂μ) x ^ (p + (1 - k * p)) *  ∏ j in s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p := by
+              -- combine two `(∫⋯∫⁻_insert i s, f ∂μ) x` terms
+              rw [ENNReal.rpow_add_of_nonneg]
+              · ring
+              · exact hp₀
+              · exact hk'
+    _ ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (s.card - 1 : ℝ) * p) *
+          ∏ j in s, (∫⋯∫⁻_{j}, (∫⋯∫⁻_{i}, f ∂μ) ∂μ) x ^ p := by
+              -- identify the result with the RHS integrand
+              congr! 2 with j hj
+              · push_cast
+                ring_nf
+              · congr! 1
+                rw [← lmarginal_union μ f hf]
+                · congr
+                  rw [Finset.union_comm]
+                  rfl
+                · rw [Finset.disjoint_singleton]
+                  simp only [Finset.mem_insert, Finset.mem_compl] at hj
+                  exact fun h ↦ hi (h ▸ hj)
+
+/-- Auxiliary result for the grid-lines lemma.  Given a nonnegative function on a finitary product
+type indexed by `ι`, and a set `s` in `ι`, consider partially integrating over the variables in
+`sᶜ` and performing the "grid-lines operation" (see `GridLines.T`) to the resulting function in the
+variables `s`.  This theorem states that this operation decreases as the number of grid-lines taken
+increases. -/
+theorem T_lmarginal_antitone (hp₀ : 0 ≤ p) (hp : (#ι - 1 : ℝ) * p ≤ 1)
+    {f : (∀ i, A i) → ℝ≥0∞} (hf : Measurable f) :
+    Antitone (fun s ↦ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s) := by
+  -- Reformulate (by induction): a function is decreasing on `Finset ι` if it decreases under the
+  -- insertion of any element to any set.
+  rw [Finset.antitone_iff_forall_insert_le]
+  intro s i hi
+  -- apply the lemma designed to encapsulate the inductive step
+  convert T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2
+  · rw [← lmarginal_union μ f hf]
+    · rw [← insert_compl_insert hi]
+      rfl
+    rw [Finset.disjoint_singleton_left, not_mem_compl]
+    exact mem_insert_self i s
+  · -- the main nontrivial point is to check that an exponent `p` satisfying `0 ≤ p` and
+    -- `(#ι - 1) * p ≤ 1` is in the valid range for the inductive-step lemma
+    refine le_trans ?_ hp
+    gcongr
+    suffices (s.card : ℝ) + 1 ≤ #ι by linarith
+    rw [← card_add_card_compl s]
+    norm_cast
+    gcongr
+    have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
+    rwa [← card_pos] at hi'
+
+end GridLines
+
+/-- The "grid-lines lemma" (not a standard name), stated with a general parameter `p` as the
+exponent.  Compare with `lintegral_prod_lintegral_pow_le`.
+
+For any finite dependent product `Π i : ι, A i` of sigma-finite measure spaces, for any
+nonnegative real number `p` such that `(#ι - 1) * p ≤ 1`, for any function `f` from `Π i, A i` into
+the extended nonnegative reals, we consider an associated "grid-lines quantity", the integral of an
+associated function from `Π i, A i` into the extended nonnegative reals.  The value of this function
+at `x : Π i, A i` is obtained by multiplying a certain power of `f` with the product, for each
+co-ordinate `i`, of a certain power of the integral of `f` along the "grid line" in the `i`
+direction through `x`.
+
+This lemma bounds the Lebesgue integral of the grid-lines quantity by a power of the Lebesgue
+integral of `f`. -/
+theorem lintegral_mul_prod_lintegral_pow_le {p : ℝ} (hp₀ : 0 ≤ p)
+    (hp : (#ι - 1 : ℝ) * p ≤ 1) {f : (∀ i : ι, A i) → ℝ≥0∞} (hf : Measurable f) :
+    ∫⁻ x, f x ^ (1 - (#ι - 1 : ℝ) * p) * ∏ i, (∫⁻ xᵢ, f (update x i xᵢ) ∂μ i) ^ p ∂.pi μ
+    ≤ (∫⁻ x, f x ∂.pi μ) ^ (1 + p) := by
+  cases isEmpty_or_nonempty (∀ i, A i)
+  · simp_rw [lintegral_of_isEmpty]; refine' zero_le _
+  inhabit ∀ i, A i
+  have H : (∅ : Finset ι) ≤ Finset.univ := Finset.empty_subset _
+  simpa [lmarginal_univ] using GridLines.T_lmarginal_antitone μ hp₀ hp hf H default
+
+/-- 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 ι]
+    {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 h0 : (1:ℝ) < #ι := by norm_cast; exact Fintype.one_lt_card
+  have h1 : (0:ℝ) < #ι - 1 := by linarith
+  have h3 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
+  have h4 : (#ι - 1 : ℝ) * ((1 : ℝ) / (#ι - 1 : ℝ)) ≤ 1 := by field_simp
+  have h5 : p = 1 + 1 / (↑#ι - 1) := by field_simp; rw [mul_comm, hp.sub_one_mul_conj]
+  rw [h5]
+  convert lintegral_mul_prod_lintegral_pow_le μ h3 h4 hf using 2
+  field_simp
+
+/-! ## The Gagliardo-Nirenberg-Sobolev inequality -/
+
+variable [Nontrivial ι] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace 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
+`ι → ℝ` where `n := #ι` is finite and at least 2.)  Then the Lebesgue integral of the pointwise
+expression `|u x| ^ (n / (n - 1))` is bounded above by the `n / (n - 1)`-th power of the Lebesgue
+integral of the Fréchet derivative of `u`.
+
+For a basis-free version, see `lintegral_pow_le_pow_lintegral_fderiv`. -/
+theorem lintegral_pow_le_pow_lintegral_fderiv_aux
+    {p : ℝ} (hp : Real.IsConjExponent #ι p)
+    {u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u)
+    (h2u : HasCompactSupport u) :
+    ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p := by
+  have : (1:ℝ) ≤ ↑#ι - 1 := by
+    have hι : (2:ℝ) ≤ #ι := by exact_mod_cast Fintype.one_lt_card
+    linarith
+  calc ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p
+      = ∫⁻ x, ((‖u x‖₊ : ℝ≥0∞) ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
+        -- a little algebraic manipulation of the exponent
+        congr! 2 with x
+        rw [← ENNReal.rpow_mul, hp.conj_eq]
+        field_simp
+    _ = ∫⁻ x, ∏ _i : ι, (‖u x‖₊ : ℝ≥0∞) ^ (1 / (#ι - 1 : ℝ)) := by
+        -- express the left-hand integrand as a product of identical factors
+        congr! 2 with x
+        simp_rw [prod_const, card_univ]
+        norm_cast
+    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖₊) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
+    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p :=
+        -- apply the grid-lines lemma
+        lintegral_prod_lintegral_pow_le _ hp (by fun_prop)
+  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ᵢ, (‖fderiv ℝ u (update x i xᵢ)‖₊ : ℝ≥0∞) := ?_
+  gcongr with y; swap; exact Measure.restrict_le_self
+  -- bound the derivative which appears
+  calc ‖deriv (u ∘ update x i) y‖₊ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖₊ := by
+        rw [fderiv.comp_deriv _ (hu.differentiable le_rfl).differentiableAt
+          (hasDerivAt_update x i y).differentiableAt]
+    _ ≤ ‖fderiv ℝ u (update x i y)‖₊ * ‖deriv (update x i) y‖₊ :=
+        ContinuousLinearMap.le_opNNNorm ..
+    _ ≤ ‖fderiv ℝ u (update x i y)‖₊ := by simp [deriv_update, Pi.nnnorm_single]
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
+  [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ]
+
+open FiniteDimensional
+
+set_option linter.unusedVariables false in
+variable (F) in
+/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
+compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
+with Haar measure. There exists a constant `C` depending only on `E`, such that the Lebesgue
+integral of the pointwise expression `|u x| ^ (n / (n - 1))` is bounded above by `C` times the
+`n / (n - 1)`-th power of the Lebesgue integral of the Fréchet derivative of `u`. -/
+theorem lintegral_pow_le_pow_lintegral_fderiv (hE : 2 ≤ finrank ℝ E)
+    {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
+    ∃ C : ℝ≥0, ∀ {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤ C * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
+  -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
+  -- matrices in `lintegral_pow_le_pow_lintegral_fderiv_aux`.
+  let ι := Fin (finrank ℝ E)
+  have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
+  have : Nontrivial ι := by rwa [Fin.nontrivial_iff_two_le]
+  have : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
+  have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
+  have e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
+  have : IsAddHaarMeasure ((volume : Measure (ι → ℝ)).map e.symm) :=
+    (e.symm : (ι → ℝ) ≃+ E).isAddHaarMeasure_map _ e.symm.continuous e.symm.symm.continuous
+  have hp : Real.IsConjExponent #ι p := by rwa [hιcard]
+  have h0p : 0 ≤ p := hp.symm.nonneg
+  let c := addHaarScalarFactor μ ((volume : Measure (ι → ℝ)).map e.symm)
+  have hc : 0 < c := addHaarScalarFactor_pos_of_isAddHaarMeasure ..
+  have h2c : μ = c • ((volume : Measure (ι → ℝ)).map e.symm) := isAddLeftInvariant_eq_smul ..
+  have h3c : (c : ℝ≥0∞) ≠ 0 := by simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
+  have : ∃ C : ℝ≥0, C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
+    use (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹
+    rw [inv_mul_cancel_right₀]
+    exact (NNReal.rpow_pos hc).ne'
+  refine this.imp fun C hC u hu h2u ↦ ?_
+  rw [h2c, ENNReal.smul_def, lintegral_smul_measure, lintegral_smul_measure]
+  let v : (ι → ℝ) → F := u ∘ e.symm
+  have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
+  have h2v : HasCompactSupport v := h2u.comp_homeomorph e.symm.toHomeomorph
+  have :=
+  calc ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂(volume : Measure (ι → ℝ)).map e.symm
+      = ∫⁻ y, (‖v y‖₊ : ℝ≥0∞) ^ p := by
+        refine lintegral_map ?_ e.symm.continuous.measurable
+        borelize F
+        exact hu.continuous.measurable.nnnorm.coe_nnreal_ennreal.pow_const _
+    _ ≤ (∫⁻ y, ‖fderiv ℝ v y‖₊) ^ p :=
+        lintegral_pow_le_pow_lintegral_fderiv_aux hp hv h2v
+    _ = (∫⁻ y, ‖(fderiv ℝ u (e.symm y)).comp (fderiv ℝ e.symm y)‖₊) ^ p := by
+        congr! with y
+        apply fderiv.comp _ (hu.differentiable le_rfl _)
+        exact e.symm.differentiableAt
+    _ ≤ (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖₊ * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊) ^ p := by
+        gcongr with y
+        norm_cast
+        rw [e.symm.fderiv]
+        apply ContinuousLinearMap.opNNNorm_comp_le
+    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ * ∫⁻ y, ‖fderiv ℝ u (e.symm y)‖₊) ^ p := by
+        rw [lintegral_mul_const, mul_comm]
+        refine (Continuous.nnnorm ?_).measurable.coe_nnreal_ennreal
+        exact (hu.continuous_fderiv le_rfl).comp e.symm.continuous
+    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0) * (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖₊) ^ p := by
+        rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, ENNReal.coe_rpow_of_nonneg _ h0p]
+    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0)
+        * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂(volume : Measure (ι → ℝ)).map e.symm) ^ p := by
+        congr
+        rw [lintegral_map _ e.symm.continuous.measurable]
+        fun_prop
+  rw [← ENNReal.mul_le_mul_left h3c ENNReal.coe_ne_top, ← mul_assoc, ← ENNReal.coe_mul, ← hC,
+    ENNReal.coe_mul] at this
+  rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, ← mul_assoc, ENNReal.coe_rpow_of_ne_zero hc.ne']
+  exact this
+
+set_option linter.unusedVariables false in
+variable (F) in
+/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
+compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
+with Haar measure. There exists a constant `C` depending only on `E`, such that the `Lᵖ` norm of
+`u`, where `p := n / (n - 1)`, is bounded above by `C` times the `L¹` norm of the Fréchet derivative
+of `u`. -/
+theorem snorm_le_snorm_fderiv (hE : 2 ≤ finrank ℝ E)
+    {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
+    ∃ C : ℝ≥0, ∀ {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    snorm u p μ ≤ C * snorm (fderiv ℝ u) 1 μ := by
+  obtain ⟨m, hm⟩ : ∃ m, finrank ℝ E = m + 2 := Nat.exists_eq_add_of_le' hE
+  have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
+  obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv F μ hE hp.coe
+  use C ^ (p : ℝ)⁻¹
+  intro u hu h2u
+  rw [snorm_one_eq_lintegral_nnnorm,
+    ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le,
+    ENNReal.coe_rpow_of_nonneg _ h0p.le, ← NNReal.rpow_mul,
+    snorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',
+    inv_mul_cancel h0p.ne', NNReal.rpow_one]
+  exact hC hu h2u
+
+variable (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
+set_option linter.unusedVariables false in
+/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
+compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
+with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
+There exists a constant `C` depending only on `E` and `p`, such that the `Lᵖ'` norm of `u`
+is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+
+Note: The codomain of `u` needs to be a Hilbert space.
+-/
+theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
+    (h2p : p < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
+    ∃ C : ℝ≥0, ∀ {u : E → F'} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  set n := finrank ℝ E
+  let n' := NNReal.conjExponent n
+  have h0n : 2 ≤ n := Nat.succ_le_of_lt <| Nat.one_lt_cast.mp <| hp.trans_lt h2p
+  have hn : NNReal.IsConjExponent n n' := .conjExponent (by norm_cast)
+  have h1n : 1 ≤ (n : ℝ≥0) := hn.one_le
+  have h2n : (0 : ℝ) < n - 1 := by simp_rw [sub_pos]; exact hn.coe.one_lt
+  have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
+  rcases hp.eq_or_lt with rfl|hp
+  -- the case `p = 1`
+  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv F' μ h0n hn
+    refine ⟨C, @fun u hu h2u ↦ ?_⟩
+    convert hC hu h2u
+    ext
+    rw [← inv_inj, hp']
+    field_simp [n', NNReal.conjExponent]
+  -- the case `p > 1`
+  let q := Real.conjExponent p
+  have hq : Real.IsConjExponent p q := .conjExponent hp
+  have h0p : p ≠ 0 := zero_lt_one.trans hp |>.ne'
+  have h1p : (p : ℝ) ≠ 1 := hq.one_lt.ne'
+  -- have h3p : (p : ℝ) ≠ 0 := hq.pos.ne'
+  have h3p : (p : ℝ) - 1 ≠ 0 := sub_ne_zero_of_ne h1p
+  have h0p' : p' ≠ 0 := by
+    suffices 0 < (p' : ℝ) from (show 0 < p' from this) |>.ne'
+    rw [← inv_pos, hp', sub_pos]
+    exact inv_lt_inv_of_lt hq.pos h2p
+  have h2q : 1 / n' - 1 / q = 1 / p' := by
+    simp_rw (config := {zeta := false}) [one_div, hp']
+    rw [← hq.one_sub_inv, ← hn.coe.one_sub_inv, sub_sub_sub_cancel_left]
+    simp only [NNReal.coe_natCast, NNReal.coe_inv]
+  let γ : ℝ≥0 := ⟨p * (n - 1) / (n - p), by positivity⟩
+  have h0γ : (γ : ℝ) = p * (n - 1) / (n - p) := rfl
+  have h1γ : 1 < (γ : ℝ) := by
+    rwa [h0γ, one_lt_div hnp, mul_sub, mul_one, sub_lt_sub_iff_right, lt_mul_iff_one_lt_left]
+    exact hn.coe.pos
+  have h2γ : γ * n' = p' := by
+    rw [← NNReal.coe_inj, ← inv_inj, hp', NNReal.coe_mul, h0γ, hn.coe.conj_eq]
+    field_simp; ring
+  have h3γ : (γ - 1) * q = p' := by
+    rw [← inv_inj, hp', h0γ, hq.conj_eq]
+    have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
+    field_simp [this]; ring
+  have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv ℝ μ h0n hn
+  refine ⟨C * γ, @fun u hu h2u ↦ ?_⟩
+  by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
+  · rw [snorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
+  have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by
+    refine lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top (pos_iff_ne_zero.mpr h0p') ?_ |>.ne
+    dsimp only
+    rw [NNReal.val_eq_coe, ← snorm_nnreal_eq_snorm' h0p']
+    exact hu.continuous.memℒp_of_hasCompactSupport (μ := μ) h2u |>.snorm_lt_top
+  have h5u : (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ 0 :=
+    ENNReal.rpow_pos (pos_iff_ne_zero.mpr h3u) h4u |>.ne'
+  have h6u : (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ ∞ :=
+    ENNReal.rpow_ne_top_of_nonneg (div_nonneg zero_le_one hq.symm.nonneg) h4u
+  have h7u := hu.continuous -- for fun_prop
+  have h8u := (hu.fderiv_right (m := 0) le_rfl).continuous -- for fun_prop
+  let v : E → ℝ := fun x ↦ ‖u x‖ ^ (γ : ℝ)
+  have hv : ContDiff ℝ 1 v := hu.norm_rpow h1γ
+  have h2v : HasCompactSupport v := h2u.norm.rpow_const h4γ
+  have :=
+  calc (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (n' : ℝ)) = snorm v n' μ := by
+        rw [← h2γ, snorm_nnreal_eq_lintegral hn.symm.pos.ne']
+        simp (discharger := positivity) [v, Real.nnnorm_rpow_of_nonneg, ENNReal.rpow_mul,
+          ENNReal.coe_rpow_of_nonneg]
+    _ ≤ C * snorm (fderiv ℝ v) 1 μ := hC hv h2v
+    _ = C * ∫⁻ x, ‖fderiv ℝ v x‖₊ ∂μ := by rw [snorm_one_eq_lintegral_nnnorm]
+    _ ≤ C * γ * ∫⁻ x, ‖u x‖₊ ^ ((γ : ℝ) - 1) * ‖fderiv ℝ u x‖₊ ∂μ := by
+      rw [mul_assoc, ← lintegral_const_mul γ]
+      gcongr
+      simp_rw [← mul_assoc, ENNReal.coe_rpow_of_nonneg _ (sub_nonneg.mpr h1γ.le)]
+      exact ENNReal.coe_le_coe.mpr <| nnnorm_fderiv_norm_rpow_le (hu.differentiable le_rfl) h1γ
+      fun_prop
+    _ ≤ C * γ * ((∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) *
+        (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ))) := by
+        gcongr
+        convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ
+          (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp) ?_ ?_ using 5
+        · simp_rw [← ENNReal.rpow_mul, ← h3γ]
+        · borelize F'
+          fun_prop
+        · fun_prop
+    _ = C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) *
+      (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) := by ring
+  calc
+    snorm u p' μ = (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := snorm_nnreal_eq_lintegral h0p'
+    _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) :=
+      by rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
+    _ = C * γ *  snorm (fderiv ℝ u) (↑p) μ := by rw [snorm_nnreal_eq_lintegral h0p]
+
+set_option linter.unusedVariables false in
+variable (F) in
+/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
+compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
+with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
+There exists a constant `C` depending only on `E` and `p`, such that the `Lᵖ'` norm of `u`
+is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+
+This is the version where the codomain of `u` is a finite dimensional normed space.
+-/
+theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (hp : 1 ≤ p)
+    (h2p : p < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
+    ∃ C : ℝ≥0, ∀ {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
+  let e : F ≃L[ℝ] F' := toEuclidean
+  let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊
+  let C₂ : ℝ≥0 := ‖(e : F →L[ℝ] F')‖₊
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ F' hp h2p hp'
+  refine ⟨C₁ * C * C₂, @fun u hu h2u ↦ ?_⟩ -- nope?
+  let v := e ∘ u
+  have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
+  have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
+  specialize hC hv h2v
+  have h4v : ∀ x, ‖fderiv ℝ v x‖ ≤ C₂ * ‖fderiv ℝ u x‖ := fun x ↦ calc
+    ‖fderiv ℝ v x‖
+      = ‖(fderiv ℝ e (u x)).comp (fderiv ℝ u x)‖ := by
+      rw [fderiv.comp x e.differentiableAt (hu.differentiable le_rfl x)]
+    _ ≤ ‖fderiv ℝ e (u x)‖ * ‖fderiv ℝ u x‖ :=
+      (fderiv ℝ e (u x)).opNorm_comp_le (fderiv ℝ u x)
+    _ = C₂ * ‖fderiv ℝ u x‖ := by simp_rw [e.fderiv, C₂, coe_nnnorm]
+  calc snorm u p' μ
+      = snorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp, e.symm_apply_apply]
+    _ ≤ C₁ • snorm v p' μ := by
+      apply snorm_le_nnreal_smul_snorm_of_ae_le_mul
+      exact eventually_of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
+    _ = C₁ * snorm v p' μ := rfl
+    _ ≤ C₁ * C * snorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
+    _ ≤ C₁ * C * (C₂ * snorm (fderiv ℝ u) p μ) := by
+      gcongr; exact snorm_le_nnreal_smul_snorm_of_ae_le_mul (eventually_of_forall h4v) p
+    _ = (C₁ * C * C₂ : ℝ≥0) * snorm (fderiv ℝ u) p μ := by push_cast; simp_rw [mul_assoc]
+
+variable (F) in
+set_option linter.unusedVariables false in
+/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
+function `u` supported in a bounded measurable set `s` in a normed space `E` of finite dimension
+`n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
+There exists a constant `C` depending only on `E`, `s`, `p` and `q`, such that the `L^q` norm of `u`
+is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+
+Note: The codomain of `u` needs to be a finite dimensional normed space.
+-/
+theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (hp : 1 ≤ p) (hq : 0 < q)
+    (h2p : p < finrank ℝ E) (hpq : p⁻¹ - (finrank ℝ E : ℝ)⁻¹ ≤ (q : ℝ)⁻¹) {s : Set E}
+    (hs : Bornology.IsBounded s) :
+    ∃ C : ℝ≥0, ∀ (u : E → F) (hu : ContDiff ℝ 1 u) (h2u : u.support ⊆ s),
+    snorm u q μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  let p' : ℝ≥0 := (p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹)⁻¹
+  have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ := by
+    rw [inv_inv, NNReal.coe_sub]
+    · simp
+    · gcongr
+  have : (q : ℝ≥0∞) ≤ p' := by
+    have H : (p':ℝ)⁻¹ ≤ (↑q)⁻¹ := trans hp' hpq
+    norm_cast at H ⊢
+    rwa [inv_le_inv] at H
+    · dsimp
+      have : 0 < p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹ := by
+        simp only [tsub_pos_iff_lt]
+        gcongr
+      positivity
+    · positivity
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq F μ hp h2p hp'
+  set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
+  use t * C
+  intro u hu h2u
+  let s' := toMeasurable μ s
+  have hs' : MeasurableSet s' := measurableSet_toMeasurable μ s
+  have hus' : support u ⊆ s' := h2u.trans <| subset_toMeasurable μ s
+  calc snorm u q μ = snorm u q (μ.restrict s') := by rw [snorm_restrict_eq u q μ hs' hus']
+    _ ≤ snorm u p' (μ.restrict s') * t := by
+        convert snorm_le_snorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
+        rw [← ENNReal.coe_rpow_of_nonneg]
+        · simp [s', ENNReal.coe_toNNReal hs.measure_lt_top.ne]
+        · rw [one_div, one_div]
+          norm_cast
+          rw [hp']
+          simpa using hpq
+    _ = snorm u p' μ * t := by rw [snorm_restrict_eq u p' μ hs' hus']
+    _ ≤ (C * snorm (fderiv ℝ u) p μ) * t := by
+        have h2u' : HasCompactSupport u := by
+          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
+          exact h2u.trans subset_closure
+        rel [hC hu h2u']
+    _ = (t * C) * snorm (fderiv ℝ u) p μ := by ring
+
+variable (F) in
+set_option linter.unusedVariables false in
+/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
+function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
+`n`, equipped with Haar measure, and let `1 < p < n`.
+There exists a constant `C` depending only on `E`, `s` and `p`, such that the `Lᵖ` norm of `u`
+is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+
+Note: The codomain of `u` needs to be a finite dimensional normed space.
+-/
+theorem snorm_le_snorm_fderiv' [FiniteDimensional ℝ F]
+    {p : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) {s : Set E} (hs : Bornology.IsBounded s) :
+    ∃ C : ℝ≥0, ∀ (u : E → F) (hu : ContDiff ℝ 1 u) (h2u : u.support ⊆ s),
+    snorm u p μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  refine snorm_le_snorm_fderiv_of_le F μ hp (zero_lt_one.trans_le hp) h2p ?_ hs
+  norm_cast
+  simp only [tsub_le_iff_right, le_add_iff_nonneg_right]
+  positivity
+
+end MeasureTheory

From ab2760a4dc3ff55c6a23c414732889e1f288b284 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 19:58:35 +0200
Subject: [PATCH 08/29] fix

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index ef505d83803d18..f0daca95512b19 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -497,8 +497,8 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
       (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) := by ring
   calc
     snorm u p' μ = (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := snorm_nnreal_eq_lintegral h0p'
-    _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) :=
-      by rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
+    _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) := by
+      rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
     _ = C * γ *  snorm (fderiv ℝ u) (↑p) μ := by rw [snorm_nnreal_eq_lintegral h0p]
 
 set_option linter.unusedVariables false in

From 334a3fe8b0921872ac1cd0fd8b1bee9c9d278211 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 22:57:30 +0200
Subject: [PATCH 09/29] fix build

---
 .../Analysis/Calculus/FDeriv/Measurable.lean  | 10 +++++-----
 Mathlib/MeasureTheory/Function/LpSpace.lean   |  7 +++++++
 .../Integral/SobolevInequality.lean           | 19 +++++++++++--------
 3 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
index 5bc9796457cc7b..adac2cc7b81e8e 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
@@ -392,7 +392,7 @@ theorem measurableSet_of_differentiableAt : MeasurableSet { x | DifferentiableAt
   simp
 #align measurable_set_of_differentiable_at measurableSet_of_differentiableAt
 
-@[measurability]
+@[measurability, fun_prop]
 theorem measurable_fderiv : Measurable (fderiv 𝕜 f) := by
   refine measurable_of_isClosed fun s hs => ?_
   have :
@@ -406,7 +406,7 @@ theorem measurable_fderiv : Measurable (fderiv 𝕜 f) := by
       ((measurableSet_of_differentiableAt _ _).compl.inter (MeasurableSet.const _))
 #align measurable_fderiv measurable_fderiv
 
-@[measurability]
+@[measurability, fun_prop]
 theorem measurable_fderiv_apply_const [MeasurableSpace F] [BorelSpace F] (y : E) :
     Measurable fun x => fderiv 𝕜 f x y :=
   (ContinuousLinearMap.measurable_apply y).comp (measurable_fderiv 𝕜 f)
@@ -414,7 +414,7 @@ theorem measurable_fderiv_apply_const [MeasurableSpace F] [BorelSpace F] (y : E)
 
 variable {𝕜}
 
-@[measurability]
+@[measurability, fun_prop]
 theorem measurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜] [MeasurableSpace F]
     [BorelSpace F] (f : 𝕜 → F) : Measurable (deriv f) := by
   simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1
@@ -747,7 +747,7 @@ theorem measurableSet_of_differentiableWithinAt_Ici :
   simp
 #align measurable_set_of_differentiable_within_at_Ici measurableSet_of_differentiableWithinAt_Ici
 
-@[measurability]
+@[measurability, fun_prop]
 theorem measurable_derivWithin_Ici [MeasurableSpace F] [BorelSpace F] :
     Measurable fun x => derivWithin f (Ici x) x := by
   refine measurable_of_isClosed fun s hs => ?_
@@ -800,7 +800,7 @@ theorem measurableSet_of_differentiableWithinAt_Ioi :
   simpa [differentiableWithinAt_Ioi_iff_Ici] using measurableSet_of_differentiableWithinAt_Ici f
 #align measurable_set_of_differentiable_within_at_Ioi measurableSet_of_differentiableWithinAt_Ioi
 
-@[measurability]
+@[measurability, fun_prop]
 theorem measurable_derivWithin_Ioi [MeasurableSpace F] [BorelSpace F] :
     Measurable fun x => derivWithin f (Ioi x) x := by
   simpa [derivWithin_Ioi_eq_Ici] using measurable_derivWithin_Ici f
diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
index d7ddb8fdfbd567..160e41f5f9ee4f 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -671,6 +671,13 @@ theorem memℒp_indicator_iff_restrict (hs : MeasurableSet s) :
   simp [Memℒp, aestronglyMeasurable_indicator_iff hs, snorm_indicator_eq_snorm_restrict hs]
 #align measure_theory.mem_ℒp_indicator_iff_restrict MeasureTheory.memℒp_indicator_iff_restrict
 
+/-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
+`μ.restrict s` are the same. -/
+theorem snorm_restrict_eq {s : Set α} (hs : MeasurableSet s) (hsf : f.support ⊆ s) :
+    snorm f p (μ.restrict s) = snorm f p μ := by
+  simp_rw [Function.support_subset_iff', ← Set.indicator_apply_eq_self] at hsf
+  simp_rw [← snorm_indicator_eq_snorm_restrict hs, funext hsf]
+
 /-- If a function is supported on a finite-measure set and belongs to `ℒ^p`, then it belongs to
 `ℒ^q` for any `q ≤ p`. -/
 theorem Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top
diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index f0daca95512b19..74f48980c7f9ba 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -3,13 +3,11 @@ Copyright (c) 2022 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Heather Macbeth
 -/
-import Mathlib.Analysis.InnerProductSpace.Calculus
-import Mathlib.Data.Finset.Interval
-import Mathlib.MeasureTheory.Integral.IntegralEqImproper
-import Mathlib.Tactic.FunProp.AEMeasurable
-import Mathlib.Tactic.FunProp.ContDiff
 import Mathlib.Analysis.Calculus.Deriv.Pi
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+import Mathlib.Analysis.InnerProductSpace.NormPow
+import Mathlib.Data.Finset.Interval
+import Mathlib.MeasureTheory.Integral.IntegralEqImproper
 
 /-!
 # Gagliardo-Nirenberg-Sobolev inequality
@@ -29,6 +27,11 @@ Let `n` be the dimension of the domain.
   Note that in this case the constant depends on the support of `u`.
 -/
 
+-- removeme
+set_option pp.explicit false --intentionally fail linter
+alias Continuous.memℒp_of_hasCompactSupport := MeasureTheory.Continuous.memℒp_of_hasCompactSupport
+alias Real.nnnorm_rpow_of_nonneg := NNReal.nnnorm_rpow_of_nonneg
+
 open scoped Classical BigOperators ENNReal NNReal Topology
 open Set Function Finset MeasureTheory Measure Filter
 
@@ -474,7 +477,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
   have :=
   calc (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (n' : ℝ)) = snorm v n' μ := by
         rw [← h2γ, snorm_nnreal_eq_lintegral hn.symm.pos.ne']
-        simp (discharger := positivity) [v, Real.nnnorm_rpow_of_nonneg, ENNReal.rpow_mul,
+        simp (discharger := positivity) [v, NNReal.nnnorm_rpow_of_nonneg, ENNReal.rpow_mul,
           ENNReal.coe_rpow_of_nonneg]
     _ ≤ C * snorm (fderiv ℝ v) 1 μ := hC hv h2v
     _ = C * ∫⁻ x, ‖fderiv ℝ v x‖₊ ∂μ := by rw [snorm_one_eq_lintegral_nnnorm]
@@ -580,7 +583,7 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
   let s' := toMeasurable μ s
   have hs' : MeasurableSet s' := measurableSet_toMeasurable μ s
   have hus' : support u ⊆ s' := h2u.trans <| subset_toMeasurable μ s
-  calc snorm u q μ = snorm u q (μ.restrict s') := by rw [snorm_restrict_eq u q μ hs' hus']
+  calc snorm u q μ = snorm u q (μ.restrict s') := by rw [snorm_restrict_eq hs' hus']
     _ ≤ snorm u p' (μ.restrict s') * t := by
         convert snorm_le_snorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
         rw [← ENNReal.coe_rpow_of_nonneg]
@@ -589,7 +592,7 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
           norm_cast
           rw [hp']
           simpa using hpq
-    _ = snorm u p' μ * t := by rw [snorm_restrict_eq u p' μ hs' hus']
+    _ = snorm u p' μ * t := by rw [snorm_restrict_eq hs' hus']
     _ ≤ (C * snorm (fderiv ℝ u) p μ) * t := by
         have h2u' : HasCompactSupport u := by
           apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure

From 51c9624d926aa2e96e392f9435b2b2f39c22f6d3 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 22:59:33 +0200
Subject: [PATCH 10/29] first review comment

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 74f48980c7f9ba..184211e5d44c8a 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -241,11 +241,11 @@ theorem lintegral_prod_lintegral_pow_le [Nontrivial ι]
     ≤ (∫⁻ x, f x ∂.pi μ) ^ p := by
   have h0 : (1:ℝ) < #ι := by norm_cast; exact Fintype.one_lt_card
   have h1 : (0:ℝ) < #ι - 1 := by linarith
-  have h3 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
-  have h4 : (#ι - 1 : ℝ) * ((1 : ℝ) / (#ι - 1 : ℝ)) ≤ 1 := by field_simp
-  have h5 : p = 1 + 1 / (↑#ι - 1) := by field_simp; rw [mul_comm, hp.sub_one_mul_conj]
-  rw [h5]
-  convert lintegral_mul_prod_lintegral_pow_le μ h3 h4 hf using 2
+  have h2 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
+  have h3 : (#ι - 1 : ℝ) * ((1 : ℝ) / (#ι - 1 : ℝ)) ≤ 1 := by field_simp
+  have h4 : p = 1 + 1 / (↑#ι - 1) := by field_simp; rw [mul_comm, hp.sub_one_mul_conj]
+  rw [h4]
+  convert lintegral_mul_prod_lintegral_pow_le μ h2 h3 hf using 2
   field_simp
 
 /-! ## The Gagliardo-Nirenberg-Sobolev inequality -/
@@ -307,7 +307,6 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace
 
 open FiniteDimensional
 
-set_option linter.unusedVariables false in
 variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped

From a2c3bc7bbf9eeb877f6ddf3b168e1d59ecd8fe1a Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 23:02:59 +0200
Subject: [PATCH 11/29] rest of review

---
 .../Integral/SobolevInequality.lean           | 22 +++++++------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 184211e5d44c8a..862c6c7a88edfc 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -315,7 +315,7 @@ integral of the pointwise expression `|u x| ^ (n / (n - 1))` is bounded above by
 `n / (n - 1)`-th power of the Lebesgue integral of the Fréchet derivative of `u`. -/
 theorem lintegral_pow_le_pow_lintegral_fderiv (hE : 2 ≤ finrank ℝ E)
     {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
-    ∃ C : ℝ≥0, ∀ {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤ C * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
   -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
   -- matrices in `lintegral_pow_le_pow_lintegral_fderiv_aux`.
@@ -375,7 +375,6 @@ theorem lintegral_pow_le_pow_lintegral_fderiv (hE : 2 ≤ finrank ℝ E)
   rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, ← mul_assoc, ENNReal.coe_rpow_of_ne_zero hc.ne']
   exact this
 
-set_option linter.unusedVariables false in
 variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
@@ -384,9 +383,8 @@ with Haar measure. There exists a constant `C` depending only on `E`, such that
 of `u`. -/
 theorem snorm_le_snorm_fderiv (hE : 2 ≤ finrank ℝ E)
     {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
-    ∃ C : ℝ≥0, ∀ {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p μ ≤ C * snorm (fderiv ℝ u) 1 μ := by
-  obtain ⟨m, hm⟩ : ∃ m, finrank ℝ E = m + 2 := Nat.exists_eq_add_of_le' hE
   have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
   obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv F μ hE hp.coe
   use C ^ (p : ℝ)⁻¹
@@ -399,7 +397,7 @@ theorem snorm_le_snorm_fderiv (hE : 2 ≤ finrank ℝ E)
   exact hC hu h2u
 
 variable (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
-set_option linter.unusedVariables false in
+
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
 with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
@@ -410,7 +408,7 @@ Note: The codomain of `u` needs to be a Hilbert space.
 -/
 theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
     (h2p : p < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
-    ∃ C : ℝ≥0, ∀ {u : E → F'} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ {u : E → F'} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
   set n := finrank ℝ E
   let n' := NNReal.conjExponent n
@@ -432,7 +430,6 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
   have hq : Real.IsConjExponent p q := .conjExponent hp
   have h0p : p ≠ 0 := zero_lt_one.trans hp |>.ne'
   have h1p : (p : ℝ) ≠ 1 := hq.one_lt.ne'
-  -- have h3p : (p : ℝ) ≠ 0 := hq.pos.ne'
   have h3p : (p : ℝ) - 1 ≠ 0 := sub_ne_zero_of_ne h1p
   have h0p' : p' ≠ 0 := by
     suffices 0 < (p' : ℝ) from (show 0 < p' from this) |>.ne'
@@ -503,7 +500,6 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
       rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
     _ = C * γ *  snorm (fderiv ℝ u) (↑p) μ := by rw [snorm_nnreal_eq_lintegral h0p]
 
-set_option linter.unusedVariables false in
 variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
@@ -515,14 +511,14 @@ This is the version where the codomain of `u` is a finite dimensional normed spa
 -/
 theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (hp : 1 ≤ p)
     (h2p : p < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
-    ∃ C : ℝ≥0, ∀ {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
   let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
   let e : F ≃L[ℝ] F' := toEuclidean
   let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊
   let C₂ : ℝ≥0 := ‖(e : F →L[ℝ] F')‖₊
   obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ F' hp h2p hp'
-  refine ⟨C₁ * C * C₂, @fun u hu h2u ↦ ?_⟩ -- nope?
+  refine ⟨C₁ * C * C₂, @fun u hu h2u ↦ ?_⟩
   let v := e ∘ u
   have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
   have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
@@ -546,7 +542,6 @@ theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (
     _ = (C₁ * C * C₂ : ℝ≥0) * snorm (fderiv ℝ u) p μ := by push_cast; simp_rw [mul_assoc]
 
 variable (F) in
-set_option linter.unusedVariables false in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded measurable set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
@@ -558,7 +553,7 @@ Note: The codomain of `u` needs to be a finite dimensional normed space.
 theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (hp : 1 ≤ p) (hq : 0 < q)
     (h2p : p < finrank ℝ E) (hpq : p⁻¹ - (finrank ℝ E : ℝ)⁻¹ ≤ (q : ℝ)⁻¹) {s : Set E}
     (hs : Bornology.IsBounded s) :
-    ∃ C : ℝ≥0, ∀ (u : E → F) (hu : ContDiff ℝ 1 u) (h2u : u.support ⊆ s),
+    ∃ C : ℝ≥0, ∀ (u : E → F) (_hu : ContDiff ℝ 1 u) (_h2u : u.support ⊆ s),
     snorm u q μ ≤ C * snorm (fderiv ℝ u) p μ := by
   let p' : ℝ≥0 := (p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹)⁻¹
   have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ := by
@@ -600,7 +595,6 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
     _ = (t * C) * snorm (fderiv ℝ u) p μ := by ring
 
 variable (F) in
-set_option linter.unusedVariables false in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n`.
@@ -611,7 +605,7 @@ Note: The codomain of `u` needs to be a finite dimensional normed space.
 -/
 theorem snorm_le_snorm_fderiv' [FiniteDimensional ℝ F]
     {p : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) {s : Set E} (hs : Bornology.IsBounded s) :
-    ∃ C : ℝ≥0, ∀ (u : E → F) (hu : ContDiff ℝ 1 u) (h2u : u.support ⊆ s),
+    ∃ C : ℝ≥0, ∀ (u : E → F) (_hu : ContDiff ℝ 1 u) (_h2u : u.support ⊆ s),
     snorm u p μ ≤ C * snorm (fderiv ℝ u) p μ := by
   refine snorm_le_snorm_fderiv_of_le F μ hp (zero_lt_one.trans_le hp) h2p ?_ hs
   norm_cast

From 2e64505b7ef95646c760428b0578a5851b3f74c8 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 26 Jun 2024 23:03:58 +0200
Subject: [PATCH 12/29] small

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 862c6c7a88edfc..b4f8d48cb30e89 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -27,7 +27,7 @@ Let `n` be the dimension of the domain.
   Note that in this case the constant depends on the support of `u`.
 -/
 
--- removeme
+-- remove these once merging master
 set_option pp.explicit false --intentionally fail linter
 alias Continuous.memℒp_of_hasCompactSupport := MeasureTheory.Continuous.memℒp_of_hasCompactSupport
 alias Real.nnnorm_rpow_of_nonneg := NNReal.nnnorm_rpow_of_nonneg

From 0ea3684d043db9314af08b45a304d6353a313d14 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 00:48:14 +0200
Subject: [PATCH 13/29] fix

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index b4f8d48cb30e89..fdc793b67b731e 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -27,11 +27,6 @@ Let `n` be the dimension of the domain.
   Note that in this case the constant depends on the support of `u`.
 -/
 
--- remove these once merging master
-set_option pp.explicit false --intentionally fail linter
-alias Continuous.memℒp_of_hasCompactSupport := MeasureTheory.Continuous.memℒp_of_hasCompactSupport
-alias Real.nnnorm_rpow_of_nonneg := NNReal.nnnorm_rpow_of_nonneg
-
 open scoped Classical BigOperators ENNReal NNReal Topology
 open Set Function Finset MeasureTheory Measure Filter
 

From b4d648f5bab58e89c9c0e5157b1bb5f8ffe90f4a Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 00:49:35 +0200
Subject: [PATCH 14/29] fix

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index fdc793b67b731e..a730c3baad0b61 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2022 Floris van Doorn. All rights reserved.
+Copyright (c) 2024 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Heather Macbeth
 -/

From 88fc219e047ff2e0c65b975df0527732091588e3 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 00:51:28 +0200
Subject: [PATCH 15/29] do not prime name

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index a730c3baad0b61..b858a1ab9cc81b 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -376,7 +376,7 @@ compactly-supported function `u` on a normed space `E` of finite dimension `n 
 with Haar measure. There exists a constant `C` depending only on `E`, such that the `Lᵖ` norm of
 `u`, where `p := n / (n - 1)`, is bounded above by `C` times the `L¹` norm of the Fréchet derivative
 of `u`. -/
-theorem snorm_le_snorm_fderiv (hE : 2 ≤ finrank ℝ E)
+theorem snorm_le_snorm_fderiv_one (hE : 2 ≤ finrank ℝ E)
     {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
     ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p μ ≤ C * snorm (fderiv ℝ u) 1 μ := by
@@ -414,7 +414,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
   have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
   rcases hp.eq_or_lt with rfl|hp
   -- the case `p = 1`
-  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv F' μ h0n hn
+  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one F' μ h0n hn
     refine ⟨C, @fun u hu h2u ↦ ?_⟩
     convert hC hu h2u
     ext
@@ -447,7 +447,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
     have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
     field_simp [this]; ring
   have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv ℝ μ h0n hn
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one ℝ μ h0n hn
   refine ⟨C * γ, @fun u hu h2u ↦ ?_⟩
   by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
   · rw [snorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
@@ -598,7 +598,7 @@ is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a finite dimensional normed space.
 -/
-theorem snorm_le_snorm_fderiv' [FiniteDimensional ℝ F]
+theorem snorm_le_snorm_fderiv [FiniteDimensional ℝ F]
     {p : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) {s : Set E} (hs : Bornology.IsBounded s) :
     ∃ C : ℝ≥0, ∀ (u : E → F) (_hu : ContDiff ℝ 1 u) (_h2u : u.support ⊆ s),
     snorm u p μ ≤ C * snorm (fderiv ℝ u) p μ := by

From 4e6ce972a9e05d2d619a622e5a17598c709006c9 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 01:24:17 +0200
Subject: [PATCH 16/29] fix

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index b858a1ab9cc81b..7efc75b19ab209 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -468,7 +468,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
   have :=
   calc (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (n' : ℝ)) = snorm v n' μ := by
         rw [← h2γ, snorm_nnreal_eq_lintegral hn.symm.pos.ne']
-        simp (discharger := positivity) [v, NNReal.nnnorm_rpow_of_nonneg, ENNReal.rpow_mul,
+        simp (discharger := positivity) [v, Real.nnnorm_rpow_of_nonneg, ENNReal.rpow_mul,
           ENNReal.coe_rpow_of_nonneg]
     _ ≤ C * snorm (fderiv ℝ v) 1 μ := hC hv h2v
     _ = C * ∫⁻ x, ‖fderiv ℝ v x‖₊ ∂μ := by rw [snorm_one_eq_lintegral_nnnorm]

From b28295fbb5116bc55f57b710001a94f8d615ba44 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 17:55:06 +0200
Subject: [PATCH 17/29] incoroporate 1 review comment

---
 .../Integral/SobolevInequality.lean           | 39 +++++++++++--------
 1 file changed, 23 insertions(+), 16 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 7efc75b19ab209..285c3c0a3c2077 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -245,7 +245,7 @@ theorem lintegral_prod_lintegral_pow_le [Nontrivial ι]
 
 /-! ## The Gagliardo-Nirenberg-Sobolev inequality -/
 
-variable [Nontrivial ι] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace 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
@@ -259,8 +259,10 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux
     {u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u)
     (h2u : HasCompactSupport u) :
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p := by
+  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 Fintype.one_lt_card
+    have hι : (2:ℝ) ≤ #ι := by exact_mod_cast hp.one_lt
     linarith
   calc ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p
       = ∫⁻ x, ((‖u x‖₊ : ℝ≥0∞) ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
@@ -308,15 +310,13 @@ compactly-supported function `u` on a normed space `E` of finite dimension `n 
 with Haar measure. There exists a constant `C` depending only on `E`, such that the Lebesgue
 integral of the pointwise expression `|u x| ^ (n / (n - 1))` is bounded above by `C` times the
 `n / (n - 1)`-th power of the Lebesgue integral of the Fréchet derivative of `u`. -/
-theorem lintegral_pow_le_pow_lintegral_fderiv (hE : 2 ≤ finrank ℝ E)
-    {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
+theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
     ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤ C * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
   -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
   -- matrices in `lintegral_pow_le_pow_lintegral_fderiv_aux`.
   let ι := Fin (finrank ℝ E)
   have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
-  have : Nontrivial ι := by rwa [Fin.nontrivial_iff_two_le]
   have : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
   have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
   have e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
@@ -376,12 +376,11 @@ compactly-supported function `u` on a normed space `E` of finite dimension `n 
 with Haar measure. There exists a constant `C` depending only on `E`, such that the `Lᵖ` norm of
 `u`, where `p := n / (n - 1)`, is bounded above by `C` times the `L¹` norm of the Fréchet derivative
 of `u`. -/
-theorem snorm_le_snorm_fderiv_one (hE : 2 ≤ finrank ℝ E)
-    {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
+theorem snorm_le_snorm_fderiv_one {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
     ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p μ ≤ C * snorm (fderiv ℝ u) 1 μ := by
   have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
-  obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv F μ hE hp.coe
+  obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv F μ hp.coe
   use C ^ (p : ℝ)⁻¹
   intro u hu h2u
   rw [snorm_one_eq_lintegral_nnnorm,
@@ -395,18 +394,26 @@ variable (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [Comple
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
-with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
+with Haar measure, let `1 ≤ p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
 There exists a constant `C` depending only on `E` and `p`, such that the `Lᵖ'` norm of `u`
 is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a Hilbert space.
 -/
-theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
-    (h2p : p < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
+theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E)
+    (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
     ∃ C : ℝ≥0, ∀ {u : E → F'} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  by_cases hp'0 : p' = 0
+  · simp [hp'0]
   set n := finrank ℝ E
   let n' := NNReal.conjExponent n
+  have h2p : (p : ℝ) < n := by
+    have : 0 < p⁻¹ - (n : ℝ)⁻¹ :=
+      NNReal.coe_lt_coe.mpr (pos_iff_ne_zero.mpr (inv_ne_zero hp'0)) |>.trans_eq hp'
+    simp [sub_pos] at this
+    rwa [inv_lt_inv _ (zero_lt_one.trans_le (NNReal.coe_le_coe.mpr hp))] at this
+    exact_mod_cast hn
   have h0n : 2 ≤ n := Nat.succ_le_of_lt <| Nat.one_lt_cast.mp <| hp.trans_lt h2p
   have hn : NNReal.IsConjExponent n n' := .conjExponent (by norm_cast)
   have h1n : 1 ≤ (n : ℝ≥0) := hn.one_le
@@ -414,7 +421,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
   have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
   rcases hp.eq_or_lt with rfl|hp
   -- the case `p = 1`
-  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one F' μ h0n hn
+  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one F' μ hn
     refine ⟨C, @fun u hu h2u ↦ ?_⟩
     convert hC hu h2u
     ext
@@ -447,7 +454,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p)
     have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
     field_simp [this]; ring
   have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one ℝ μ h0n hn
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one ℝ μ hn
   refine ⟨C * γ, @fun u hu h2u ↦ ?_⟩
   by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
   · rw [snorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
@@ -505,14 +512,14 @@ is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 This is the version where the codomain of `u` is a finite dimensional normed space.
 -/
 theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (hp : 1 ≤ p)
-    (h2p : p < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
+    (hn : 0 < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
     ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
   let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
   let e : F ≃L[ℝ] F' := toEuclidean
   let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊
   let C₂ : ℝ≥0 := ‖(e : F →L[ℝ] F')‖₊
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ F' hp h2p hp'
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ F' hp hn hp'
   refine ⟨C₁ * C * C₂, @fun u hu h2u ↦ ?_⟩
   let v := e ∘ u
   have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
@@ -565,7 +572,7 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
         gcongr
       positivity
     · positivity
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq F μ hp h2p hp'
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq F μ hp (mod_cast (zero_le p).trans_lt h2p) hp'
   set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
   use t * C
   intro u hu h2u

From bed19944a65791de630881fc58038a01b430bae4 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 18:01:21 +0200
Subject: [PATCH 18/29] 2 review comments

---
 .../Integral/SobolevInequality.lean           | 33 ++++++++++---------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 285c3c0a3c2077..c8104c78204159 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -311,7 +311,8 @@ with Haar measure. There exists a constant `C` depending only on `E`, such that
 integral of the pointwise expression `|u x| ^ (n / (n - 1))` is bounded above by `C` times the
 `n / (n - 1)`-th power of the Lebesgue integral of the Fréchet derivative of `u`. -/
 theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
-    ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
+    {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤ C * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
   -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
   -- matrices in `lintegral_pow_le_pow_lintegral_fderiv_aux`.
@@ -332,7 +333,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponen
     use (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹
     rw [inv_mul_cancel_right₀]
     exact (NNReal.rpow_pos hc).ne'
-  refine this.imp fun C hC u hu h2u ↦ ?_
+  refine this.imp fun C hC F _ _ _ u hu h2u ↦ ?_
   rw [h2c, ENNReal.smul_def, lintegral_smul_measure, lintegral_smul_measure]
   let v : (ι → ℝ) → F := u ∘ e.symm
   have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
@@ -377,12 +378,13 @@ with Haar measure. There exists a constant `C` depending only on `E`, such that
 `u`, where `p := n / (n - 1)`, is bounded above by `C` times the `L¹` norm of the Fréchet derivative
 of `u`. -/
 theorem snorm_le_snorm_fderiv_one {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
-    ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
+    {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p μ ≤ C * snorm (fderiv ℝ u) 1 μ := by
   have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
-  obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv F μ hp.coe
+  obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv μ hp.coe
   use C ^ (p : ℝ)⁻¹
-  intro u hu h2u
+  intro F _ _ _ u hu h2u
   rw [snorm_one_eq_lintegral_nnnorm,
     ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le,
     ENNReal.coe_rpow_of_nonneg _ h0p.le, ← NNReal.rpow_mul,
@@ -390,8 +392,6 @@ theorem snorm_le_snorm_fderiv_one {p : ℝ≥0} (hp : NNReal.IsConjExponent (fin
     inv_mul_cancel h0p.ne', NNReal.rpow_one]
   exact hC hu h2u
 
-variable (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
-
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
 with Haar measure, let `1 ≤ p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
@@ -402,7 +402,8 @@ Note: The codomain of `u` needs to be a Hilbert space.
 -/
 theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E)
     (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
-    ∃ C : ℝ≥0, ∀ {u : E → F'} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
+    ∃ C : ℝ≥0, ∀ (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
+      {u : E → F'} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
   by_cases hp'0 : p' = 0
   · simp [hp'0]
@@ -421,8 +422,8 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
   have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
   rcases hp.eq_or_lt with rfl|hp
   -- the case `p = 1`
-  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one F' μ hn
-    refine ⟨C, @fun u hu h2u ↦ ?_⟩
+  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one μ hn
+    refine ⟨C, @fun F _ _ _ u hu h2u ↦ ?_⟩
     convert hC hu h2u
     ext
     rw [← inv_inj, hp']
@@ -454,8 +455,8 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
     have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
     field_simp [this]; ring
   have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one ℝ μ hn
-  refine ⟨C * γ, @fun u hu h2u ↦ ?_⟩
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one μ hn
+  refine ⟨C * γ, @fun F _ _ _ u hu h2u ↦ ?_⟩
   by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
   · rw [snorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
   have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by
@@ -491,7 +492,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
         convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ
           (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp) ?_ ?_ using 5
         · simp_rw [← ENNReal.rpow_mul, ← h3γ]
-        · borelize F'
+        · borelize F
           fun_prop
         · fun_prop
     _ = C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) *
@@ -519,12 +520,12 @@ theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (
   let e : F ≃L[ℝ] F' := toEuclidean
   let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊
   let C₂ : ℝ≥0 := ‖(e : F →L[ℝ] F')‖₊
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ F' hp hn hp'
+  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ hp hn hp'
   refine ⟨C₁ * C * C₂, @fun u hu h2u ↦ ?_⟩
   let v := e ∘ u
   have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
   have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
-  specialize hC hv h2v
+  specialize hC F' hv h2v
   have h4v : ∀ x, ‖fderiv ℝ v x‖ ≤ C₂ * ‖fderiv ℝ u x‖ := fun x ↦ calc
     ‖fderiv ℝ v x‖
       = ‖(fderiv ℝ e (u x)).comp (fderiv ℝ u x)‖ := by
@@ -545,7 +546,7 @@ theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (
 
 variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
-function `u` supported in a bounded measurable set `s` in a normed space `E` of finite dimension
+function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
 There exists a constant `C` depending only on `E`, `s`, `p` and `q`, such that the `L^q` norm of `u`
 is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.

From fce981eed3e141de62563691ff8c1ccc5c0423ba Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 18:59:31 +0200
Subject: [PATCH 19/29] give more explanations about the proof in the module
 doc and two proofs

---
 .../Integral/SobolevInequality.lean           | 35 +++++++++++++++++--
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index c8104c78204159..06c71f99f30c75 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -18,6 +18,17 @@ we can bound the `L^p`-norm of `u` by the `L^q` norm of the derivative of `u`.
 The bound is up to a constant that is independent of the function `u`.
 Let `n` be the dimension of the domain.
 
+The main step in the proof, which we dubbed the "grid-lines lemma" below, is a complicated
+inductive argument that involves manipulating an `n+1`-fold iterated integral and a product of
+`n+2` factors. In each step, one pushes one of the integral inside (all but one of)
+the factors of the product using Hölder's inequality. The precise formulation of the induction
+hypothesis (`MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton`) is tricky,
+and none of the 5 sources we referenced stated it.
+
+In the formalization we use the operation `MeasureTheory.lmarginal` to work with the iterated
+integrals, and use `MeasureTheory.lmarginal_insert'` to conveniently push one of the integrals
+inside. The Hölder's inequality step is done using `ENNReal.lintegral_mul_prod_norm_pow_le`.
+
 ## Main results
 
 * `MeasureTheory.snorm_le_snorm_fderiv_of_eq`:
@@ -84,9 +95,18 @@ theorem T_insert_le_T_lmarginal_singleton (hp₀ : 0 ≤ p) (s : Finset ι)
     (hp : (s.card : ℝ) * p ≤ 1)
     (i : ι) (hi : i ∉ s) {f : (∀ i, A i) → ℝ≥0∞} (hf : Measurable f) :
     T μ p f (insert i s) ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := by
+  /- The proof is a tricky computation that relies on Hölder's inequality at its heart.
+  The left-hand-side is an `|s|+1`-times iterated integral. Let `xᵢ` denote the `i`-th variable.
+  We first push the integral over the `i`-th variable as the
+  innermost integral. This is done in a single step with `MeasureTheory.lmarginal_insert'`,
+  but in fact hides a repeated application of Fubini's theorem.
+  The integrand is a product of `|s|+2` factors, in `|s|+1` of them we integrate over one
+  additional variable. We split of the factor that integrates over `xᵢ`, and apply Hölder's inequality to the remaining factors (whose powers sum exactly to 1).
+  After reordering factors, and combining two factors into one we obtain the right-hand side. -/
   calc T μ p f (insert i s)
       = ∫⋯∫⁻_insert i s,
             f ^ (1 - (s.card : ℝ) * p) * ∏ j in (insert i s), (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ := by
+          -- unfold `T` and reformulate the exponents
           simp_rw [T, card_insert_of_not_mem hi]
           congr!
           push_cast
@@ -94,6 +114,7 @@ theorem T_insert_le_T_lmarginal_singleton (hp₀ : 0 ≤ p) (s : Finset ι)
     _ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ (t : A i),
             (f (update x i t) ^ (1 - (s.card : ℝ) * p)
             * ∏ j in (insert i s), (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p)  ∂ (μ i)) ∂μ := by
+          -- pull out the integral over `xᵢ`
           rw [lmarginal_insert' _ _ hi]
           · congr! with x t
             simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
@@ -102,13 +123,14 @@ theorem T_insert_le_T_lmarginal_singleton (hp₀ : 0 ≤ p) (s : Finset ι)
             refine (hf.pow_const _).mul <| Finset.measurable_prod _ ?_
             exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _
     _ ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := lmarginal_mono (s:=s) (fun x ↦ ?_)
+  -- The remainder of the computation happens within an `|s|`-fold iterated integral
   simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
-  have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (update x i t) :=
+  set X := update x i
+  have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t) :=
     fun {_} ↦ hf.lmarginal μ |>.comp <| measurable_update _
-  have hF₀ : Measurable fun t ↦ f (update x i t) := hf.comp <| measurable_update _
+  have hF₀ : Measurable fun t ↦ f (X t) := hf.comp <| measurable_update _
   let k : ℝ := s.card
   have hk' : 0 ≤ 1 - k * p := by linarith only [hp]
-  let X := update x i
   calc ∫⁻ t, f (X t) ^ (1 - k * p)
           * ∏ j in (insert i s), (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂ (μ i)
       = ∫⁻ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p)
@@ -259,6 +281,12 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux
     {u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u)
     (h2u : HasCompactSupport u) :
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p := by
+  /- For a function `f` in one variable and `t ∈ ℝ` we have
+  `|f(t)| = `|∫_{-∞}^t Df(s)∂s| ≤ ∫_ℝ |Df(s)| ∂s` where we use the fundamental theorem of calculus.
+  For each `x ∈ ℝⁿ` we let `u` vary in one of the `n` coordinates and apply the inequality above.
+  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
@@ -279,6 +307,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux
     _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖₊) ^ p :=
         -- apply the grid-lines lemma
         lintegral_prod_lintegral_pow_le _ hp (by 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

From 4754712a3b25c364e31f8dfbfbc6467cac66a8a6 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 19:15:47 +0200
Subject: [PATCH 20/29] more documentation

---
 .../Integral/SobolevInequality.lean           | 22 +++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 06c71f99f30c75..97ce318b2cb2ae 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -36,6 +36,12 @@ inside. The Hölder's inequality step is done using `ENNReal.lintegral_mul_prod_
 * `MeasureTheory.snorm_le_snorm_fderiv_of_le`:
   The bound holds when `1 ≤ p < n`, `0 ≤ q` and `p⁻¹ - n⁻¹ ≤ q⁻¹`.
   Note that in this case the constant depends on the support of `u`.
+
+Potentially also useful:
+* `MeasureTheory.snorm_le_snorm_fderiv_one`: this is the inequality for `p = 1`. In this version,
+  the codomain can be an arbitrary Banach space.
+* `MeasureTheory.snorm_le_snorm_fderiv_of_eq_inner`: in this version the codomain is assumed to be
+  a Hilbert space, without restrictions on its dimension.
 -/
 
 open scoped Classical BigOperators ENNReal NNReal Topology
@@ -343,8 +349,13 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponen
     ∃ C : ℝ≥0, ∀ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
     {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤ C * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
-  -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
-  -- matrices in `lintegral_pow_le_pow_lintegral_fderiv_aux`.
+  /- We reduce to the case where `E` is `ℝⁿ`, for which we have already proved the result using
+  an explicit basis in `MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux`.
+  This proof is not too hard, but takes quite some steps, reasoning about the equivalence
+  `e : E ≃ ℝⁿ`, relating the measures on each sides of the equivalence,
+  and estimating the derivative using the chain rule.
+  The constant `C` is determined by the ratio of the measures on `E` and `ℝⁿ` and
+  the operator norm of `e` (raised to suitable powers involving `p`). -/
   let ι := Fin (finrank ℝ E)
   have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
   have : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
@@ -434,6 +445,10 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
     ∃ C : ℝ≥0, ∀ (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
       {u : E → F'} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  /- Here we derive the GNS-inequality for `p ≥ 1` from the version with `p = 1`.
+  For `p > 1` we apply the previous version to the function `|u|^γ` for a suitably chosen `γ`.
+  The proof requires that `x ↦ |x|^p` is smooth in the codomain, so we require that it is a
+  Hilbert space. -/
   by_cases hp'0 : p' = 0
   · simp [hp'0]
   set n := finrank ℝ E
@@ -545,6 +560,9 @@ theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (
     (hn : 0 < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
     ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
     snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+  /- Here we derive the GNS-inequality with a Hilbert space as codomain to the case with a
+  finite-dimensional normed space as codomain, by transferring the result along the equivalence
+  `F ≃ ℝᵐ`. -/
   let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
   let e : F ≃L[ℝ] F' := toEuclidean
   let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊

From 7d32abaec819fcdaeb23a6c10872a561e14618d3 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 19:26:48 +0200
Subject: [PATCH 21/29] improve snorm_restrict_eq, modify proof

proof might be broken now
---
 Mathlib/MeasureTheory/Function/LpSpace.lean           |  7 +++++--
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 11 ++++-------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
index 633606bae47cb8..e5aa1ba3cddcd3 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -11,6 +11,7 @@ import Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
 import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
 import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 import Mathlib.MeasureTheory.Measure.OpenPos
+import Mathlib.MeasureTheory.Measure.Typeclasses
 import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
 import Mathlib.Topology.ContinuousFunction.Compact
 import Mathlib.Order.Filter.IndicatorFunction
@@ -674,10 +675,12 @@ theorem memℒp_indicator_iff_restrict (hs : MeasurableSet s) :
 
 /-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
 `μ.restrict s` are the same. -/
-theorem snorm_restrict_eq {s : Set α} (hs : MeasurableSet s) (hsf : f.support ⊆ s) :
+theorem snorm_restrict_eq [SFinite μ] {s : Set α} (hsf : f.support ⊆ s) :
     snorm f p (μ.restrict s) = snorm f p μ := by
+  replace hsf := hsf.trans <| subset_toMeasurable μ s
   simp_rw [Function.support_subset_iff', ← Set.indicator_apply_eq_self] at hsf
-  simp_rw [← snorm_indicator_eq_snorm_restrict hs, funext hsf]
+  simp_rw [← μ.restrict_toMeasurable_of_sFinite s,
+    ← snorm_indicator_eq_snorm_restrict (measurableSet_toMeasurable μ s), funext hsf]
 
 /-- If a function is supported on a finite-measure set and belongs to `ℒ^p`, then it belongs to
 `ℒ^q` for any `q ≤ p`. -/
diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 97ce318b2cb2ae..72e76d34633782 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -624,19 +624,16 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
   set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
   use t * C
   intro u hu h2u
-  let s' := toMeasurable μ s
-  have hs' : MeasurableSet s' := measurableSet_toMeasurable μ s
-  have hus' : support u ⊆ s' := h2u.trans <| subset_toMeasurable μ s
-  calc snorm u q μ = snorm u q (μ.restrict s') := by rw [snorm_restrict_eq hs' hus']
-    _ ≤ snorm u p' (μ.restrict s') * t := by
+  calc snorm u q μ = snorm u q (μ.restrict s) := by rw [snorm_restrict_eq h2u]
+    _ ≤ snorm u p' (μ.restrict s) * t := by
         convert snorm_le_snorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
         rw [← ENNReal.coe_rpow_of_nonneg]
-        · simp [s', ENNReal.coe_toNNReal hs.measure_lt_top.ne]
+        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
         · rw [one_div, one_div]
           norm_cast
           rw [hp']
           simpa using hpq
-    _ = snorm u p' μ * t := by rw [snorm_restrict_eq hs' hus']
+    _ = snorm u p' μ * t := by rw [snorm_restrict_eq h2u]
     _ ≤ (C * snorm (fderiv ℝ u) p μ) * t := by
         have h2u' : HasCompactSupport u := by
           apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure

From 13a1c65bb895b827ca7653629754e8d074ed0db5 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 19:27:23 +0200
Subject: [PATCH 22/29] fix

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 72e76d34633782..0c224a9da1db17 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -107,7 +107,8 @@ theorem T_insert_le_T_lmarginal_singleton (hp₀ : 0 ≤ p) (s : Finset ι)
   innermost integral. This is done in a single step with `MeasureTheory.lmarginal_insert'`,
   but in fact hides a repeated application of Fubini's theorem.
   The integrand is a product of `|s|+2` factors, in `|s|+1` of them we integrate over one
-  additional variable. We split of the factor that integrates over `xᵢ`, and apply Hölder's inequality to the remaining factors (whose powers sum exactly to 1).
+  additional variable. We split of the factor that integrates over `xᵢ`,
+  and apply Hölder's inequality to the remaining factors (whose powers sum exactly to 1).
   After reordering factors, and combining two factors into one we obtain the right-hand side. -/
   calc T μ p f (insert i s)
       = ∫⋯∫⁻_insert i s,

From fdf98f6526578ca85d8a49d306e6ad53fe1ea957 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 27 Jun 2024 23:21:37 +0200
Subject: [PATCH 23/29] remove 2 unused variables

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 0c224a9da1db17..b7a2fd97ac0b5a 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -340,7 +340,6 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace
 
 open FiniteDimensional
 
-variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
 with Haar measure. There exists a constant `C` depending only on `E`, such that the Lebesgue
@@ -412,7 +411,6 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponen
   rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, ← mul_assoc, ENNReal.coe_rpow_of_ne_zero hc.ne']
   exact this
 
-variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
 with Haar measure. There exists a constant `C` depending only on `E`, such that the `Lᵖ` norm of

From b68197ac8719161d31106204e597e12d2cbbd873 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 28 Jun 2024 15:52:53 +0200
Subject: [PATCH 24/29] separate the constants out as definitions

---
 .../Integral/SobolevInequality.lean           | 160 +++++++++++-------
 1 file changed, 103 insertions(+), 57 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index b7a2fd97ac0b5a..e8c43822d32fa1 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -32,13 +32,13 @@ inside. The Hölder's inequality step is done using `ENNReal.lintegral_mul_prod_
 ## Main results
 
 * `MeasureTheory.snorm_le_snorm_fderiv_of_eq`:
-  The bound holds for `1 ≤ p < n` and `q⁻¹ = p⁻¹ - n⁻¹`
+  The bound holds for `1 ≤ p`, `0 < n` and `q⁻¹ = p⁻¹ - n⁻¹`
 * `MeasureTheory.snorm_le_snorm_fderiv_of_le`:
   The bound holds when `1 ≤ p < n`, `0 ≤ q` and `p⁻¹ - n⁻¹ ≤ q⁻¹`.
   Note that in this case the constant depends on the support of `u`.
 
 Potentially also useful:
-* `MeasureTheory.snorm_le_snorm_fderiv_one`: this is the inequality for `p = 1`. In this version,
+* `MeasureTheory.snorm_le_snorm_fderiv_one`: this is the inequality for `q = 1`. In this version,
   the codomain can be an arbitrary Banach space.
 * `MeasureTheory.snorm_le_snorm_fderiv_of_eq_inner`: in this version the codomain is assumed to be
   a Hilbert space, without restrictions on its dimension.
@@ -340,15 +340,26 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace
 
 open FiniteDimensional
 
+/-- The constant factor occurring in the conclusion of `lintegral_pow_le_pow_lintegral_fderiv`.
+It only depends on `E`, `μ` and `p`. -/
+def lintegralPowLePowLIntegralFDerivConst (p : ℝ) : ℝ≥0 := by
+  let ι := Fin (finrank ℝ E)
+  have : finrank ℝ E = finrank ℝ (ι → ℝ) := by
+    rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]
+  let e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
+  let c := addHaarScalarFactor μ ((volume : Measure (ι → ℝ)).map e.symm)
+  exact (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹
+
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
 with Haar measure. There exists a constant `C` depending only on `E`, such that the Lebesgue
 integral of the pointwise expression `|u x| ^ (n / (n - 1))` is bounded above by `C` times the
 `n / (n - 1)`-th power of the Lebesgue integral of the Fréchet derivative of `u`. -/
-theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
-    ∃ C : ℝ≥0, ∀ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
-    {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
-    ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤ C * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
+theorem lintegral_pow_le_pow_lintegral_fderiv  {u : E → F}
+    (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
+    {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
+    ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤
+    lintegralPowLePowLIntegralFDerivConst μ p * (∫⁻ x, ‖fderiv ℝ u x‖₊ ∂μ) ^ p := by
   /- We reduce to the case where `E` is `ℝⁿ`, for which we have already proved the result using
   an explicit basis in `MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux`.
   This proof is not too hard, but takes quite some steps, reasoning about the equivalence
@@ -356,11 +367,11 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponen
   and estimating the derivative using the chain rule.
   The constant `C` is determined by the ratio of the measures on `E` and `ℝⁿ` and
   the operator norm of `e` (raised to suitable powers involving `p`). -/
+  set C := lintegralPowLePowLIntegralFDerivConst μ p
   let ι := Fin (finrank ℝ E)
   have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
-  have : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
   have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
-  have e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
+  let e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
   have : IsAddHaarMeasure ((volume : Measure (ι → ℝ)).map e.symm) :=
     (e.symm : (ι → ℝ) ≃+ E).isAddHaarMeasure_map _ e.symm.continuous e.symm.symm.continuous
   have hp : Real.IsConjExponent #ι p := by rwa [hιcard]
@@ -369,11 +380,9 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponen
   have hc : 0 < c := addHaarScalarFactor_pos_of_isAddHaarMeasure ..
   have h2c : μ = c • ((volume : Measure (ι → ℝ)).map e.symm) := isAddLeftInvariant_eq_smul ..
   have h3c : (c : ℝ≥0∞) ≠ 0 := by simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
-  have : ∃ C : ℝ≥0, C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
-    use (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹
-    rw [inv_mul_cancel_right₀]
-    exact (NNReal.rpow_pos hc).ne'
-  refine this.imp fun C hC F _ _ _ u hu h2u ↦ ?_
+  have hC : C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
+    rw [show C = (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹ from rfl,
+      inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
   rw [h2c, ENNReal.smul_def, lintegral_smul_measure, lintegral_smul_measure]
   let v : (ι → ℝ) → F := u ∘ e.symm
   have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
@@ -411,25 +420,33 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {p : ℝ} (hp : Real.IsConjExponen
   rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, ← mul_assoc, ENNReal.coe_rpow_of_ne_zero hc.ne']
   exact this
 
+/-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_one`.
+It only depends on `E`, `μ` and `p`. -/
+def snormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
+
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
 with Haar measure. There exists a constant `C` depending only on `E`, such that the `Lᵖ` norm of
 `u`, where `p := n / (n - 1)`, is bounded above by `C` times the `L¹` norm of the Fréchet derivative
 of `u`. -/
-theorem snorm_le_snorm_fderiv_one {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
-    ∃ C : ℝ≥0, ∀ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
-    {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
-    snorm u p μ ≤ C * snorm (fderiv ℝ u) 1 μ := by
+theorem snorm_le_snorm_fderiv_one  {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
+    {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
+    snorm u p μ ≤ snormLESNormFDerivOneConst μ p * snorm (fderiv ℝ u) 1 μ := by
   have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
-  obtain ⟨C, hC⟩ := lintegral_pow_le_pow_lintegral_fderiv μ hp.coe
-  use C ^ (p : ℝ)⁻¹
-  intro F _ _ _ u hu h2u
   rw [snorm_one_eq_lintegral_nnnorm,
     ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le,
-    ENNReal.coe_rpow_of_nonneg _ h0p.le, ← NNReal.rpow_mul,
+    ENNReal.coe_rpow_of_nonneg _ h0p.le, snormLESNormFDerivOneConst, ← NNReal.rpow_mul,
     snorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',
     inv_mul_cancel h0p.ne', NNReal.rpow_one]
-  exact hC hu h2u
+  exact lintegral_pow_le_pow_lintegral_fderiv μ hu h2u hp.coe
+
+/-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_of_eq_inner`.
+It only depends on `E`, `μ` and `p`. -/
+def snormLESNormFDerivOfEqInnerConst (p : ℝ) : ℝ≥0 :=
+  let n := finrank ℝ E
+  snormLESNormFDerivOneConst μ (NNReal.conjExponent n) * (p * (n - 1) / (n - p)).toNNReal
+
+variable {F' : Type*} [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
@@ -439,11 +456,11 @@ is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a Hilbert space.
 -/
-theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E)
+theorem snorm_le_snorm_fderiv_of_eq_inner  {u : E → F'}
+    (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
+    {p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E)
     (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
-    ∃ C : ℝ≥0, ∀ (F' : Type*) [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [CompleteSpace F']
-      {u : E → F'} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
-    snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+    snorm u p' μ ≤ snormLESNormFDerivOfEqInnerConst μ p * snorm (fderiv ℝ u) p μ := by
   /- Here we derive the GNS-inequality for `p ≥ 1` from the version with `p = 1`.
   For `p > 1` we apply the previous version to the function `|u|^γ` for a suitably chosen `γ`.
   The proof requires that `x ↦ |x|^p` is smooth in the codomain, so we require that it is a
@@ -465,12 +482,13 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
   have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
   rcases hp.eq_or_lt with rfl|hp
   -- the case `p = 1`
-  · obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one μ hn
-    refine ⟨C, @fun F _ _ _ u hu h2u ↦ ?_⟩
-    convert hC hu h2u
-    ext
-    rw [← inv_inj, hp']
-    field_simp [n', NNReal.conjExponent]
+  · convert snorm_le_snorm_fderiv_one μ hu h2u hn using 2
+    · suffices (p' : ℝ) = n' by simpa using this
+      rw [← inv_inj, hp']
+      field_simp [n', NNReal.conjExponent]
+    · norm_cast
+      simp_rw [snormLESNormFDerivOfEqInnerConst]
+      field_simp
   -- the case `p > 1`
   let q := Real.conjExponent p
   have hq : Real.IsConjExponent p q := .conjExponent hp
@@ -498,8 +516,8 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
     have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
     field_simp [this]; ring
   have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one μ hn
-  refine ⟨C * γ, @fun F _ _ _ u hu h2u ↦ ?_⟩
+  -- obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one μ hn
+  -- refine ⟨C * γ, @fun F _ _ _ u hu h2u ↦ ?_⟩
   by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
   · rw [snorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
   have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by
@@ -516,12 +534,13 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
   let v : E → ℝ := fun x ↦ ‖u x‖ ^ (γ : ℝ)
   have hv : ContDiff ℝ 1 v := hu.norm_rpow h1γ
   have h2v : HasCompactSupport v := h2u.norm.rpow_const h4γ
+  set C := snormLESNormFDerivOneConst μ n'
   have :=
   calc (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (n' : ℝ)) = snorm v n' μ := by
         rw [← h2γ, snorm_nnreal_eq_lintegral hn.symm.pos.ne']
         simp (discharger := positivity) [v, Real.nnnorm_rpow_of_nonneg, ENNReal.rpow_mul,
           ENNReal.coe_rpow_of_nonneg]
-    _ ≤ C * snorm (fderiv ℝ v) 1 μ := hC hv h2v
+    _ ≤ C * snorm (fderiv ℝ v) 1 μ := snorm_le_snorm_fderiv_one μ hv h2v hn
     _ = C * ∫⁻ x, ‖fderiv ℝ v x‖₊ ∂μ := by rw [snorm_one_eq_lintegral_nnnorm]
     _ ≤ C * γ * ∫⁻ x, ‖u x‖₊ ^ ((γ : ℝ) - 1) * ‖fderiv ℝ u x‖₊ ∂μ := by
       rw [mul_assoc, ← lintegral_const_mul γ]
@@ -535,7 +554,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
         convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ
           (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp) ?_ ?_ using 5
         · simp_rw [← ENNReal.rpow_mul, ← h3γ]
-        · borelize F
+        · borelize F'
           fun_prop
         · fun_prop
     _ = C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) *
@@ -544,9 +563,26 @@ theorem snorm_le_snorm_fderiv_of_eq_inner {p p' : ℝ≥0} (hp : 1 ≤ p) (hn :
     snorm u p' μ = (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := snorm_nnreal_eq_lintegral h0p'
     _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖₊ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) := by
       rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
-    _ = C * γ *  snorm (fderiv ℝ u) (↑p) μ := by rw [snorm_nnreal_eq_lintegral h0p]
+    _ = snormLESNormFDerivOfEqInnerConst μ p *  snorm (fderiv ℝ u) (↑p) μ := by
+      suffices (C : ℝ) * γ = snormLESNormFDerivOfEqInnerConst μ p by
+        rw [snorm_nnreal_eq_lintegral h0p]
+        congr
+        norm_cast at this ⊢
+      simp_rw [snormLESNormFDerivOfEqInnerConst, γ]
+      refold_let n n' C
+      rw [NNReal.coe_mul, NNReal.coe_mk, Real.coe_toNNReal', mul_eq_mul_left_iff, eq_comm,
+        max_eq_left_iff]
+      left
+      positivity
 
 variable (F) in
+/-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_of_eq`.
+It only depends on `E`, `F`, `μ` and `p`. -/
+def SNormLESNormFDerivOfEqConst [FiniteDimensional ℝ F] (p : ℝ) : ℝ≥0 :=
+  let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
+  let e : F ≃L[ℝ] F' := toEuclidean
+  ‖(e.symm : F' →L[ℝ] F)‖₊ * snormLESNormFDerivOfEqInnerConst μ p * ‖(e : F →L[ℝ] F')‖₊
+
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
 with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
@@ -555,23 +591,23 @@ is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 
 This is the version where the codomain of `u` is a finite dimensional normed space.
 -/
-theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (hp : 1 ≤ p)
-    (hn : 0 < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
-    ∃ C : ℝ≥0, ∀ {u : E → F} (_hu : ContDiff ℝ 1 u) (_h2u : HasCompactSupport u),
-    snorm u p' μ ≤ C * snorm (fderiv ℝ u) p μ := by
+theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F]
+    {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
+    {p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E)
+    (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
+    snorm u p' μ ≤ SNormLESNormFDerivOfEqConst F μ p * snorm (fderiv ℝ u) p μ := by
   /- Here we derive the GNS-inequality with a Hilbert space as codomain to the case with a
   finite-dimensional normed space as codomain, by transferring the result along the equivalence
   `F ≃ ℝᵐ`. -/
   let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
   let e : F ≃L[ℝ] F' := toEuclidean
   let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊
+  let C : ℝ≥0 := snormLESNormFDerivOfEqInnerConst μ p
   let C₂ : ℝ≥0 := ‖(e : F →L[ℝ] F')‖₊
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq_inner μ hp hn hp'
-  refine ⟨C₁ * C * C₂, @fun u hu h2u ↦ ?_⟩
   let v := e ∘ u
   have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
   have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
-  specialize hC F' hv h2v
+  have := snorm_le_snorm_fderiv_of_eq_inner μ hv h2v hp hn hp'
   have h4v : ∀ x, ‖fderiv ℝ v x‖ ≤ C₂ * ‖fderiv ℝ u x‖ := fun x ↦ calc
     ‖fderiv ℝ v x‖
       = ‖(fderiv ℝ e (u x)).comp (fderiv ℝ u x)‖ := by
@@ -591,6 +627,13 @@ theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F] {p p' : ℝ≥0} (
     _ = (C₁ * C * C₂ : ℝ≥0) * snorm (fderiv ℝ u) p μ := by push_cast; simp_rw [mul_assoc]
 
 variable (F) in
+/-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_of_le`.
+It only depends on `F`, `μ`, `s`, `p` and `q`. -/
+def snormLESNormFDerivOfLeConst [FiniteDimensional ℝ F] (s : Set E) (p q : ℝ≥0) : ℝ≥0 :=
+  let p' : ℝ≥0 := (p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹)⁻¹
+  (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ) * SNormLESNormFDerivOfEqConst F μ p
+
+
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
@@ -599,11 +642,14 @@ is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a finite dimensional normed space.
 -/
-theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (hp : 1 ≤ p) (hq : 0 < q)
-    (h2p : p < finrank ℝ E) (hpq : p⁻¹ - (finrank ℝ E : ℝ)⁻¹ ≤ (q : ℝ)⁻¹) {s : Set E}
+theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F]
+    {u : E → F} {s : Set E} (hu : ContDiff ℝ 1 u) (h2u : u.support ⊆ s)
+    {p q : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E)
+    (hpq : p⁻¹ - (finrank ℝ E : ℝ)⁻¹ ≤ (q : ℝ)⁻¹)
     (hs : Bornology.IsBounded s) :
-    ∃ C : ℝ≥0, ∀ (u : E → F) (_hu : ContDiff ℝ 1 u) (_h2u : u.support ⊆ s),
-    snorm u q μ ≤ C * snorm (fderiv ℝ u) p μ := by
+    snorm u q μ ≤ snormLESNormFDerivOfLeConst F μ s p q * snorm (fderiv ℝ u) p μ := by
+  by_cases hq0 : q = 0
+  · simp [hq0]
   let p' : ℝ≥0 := (p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹)⁻¹
   have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ := by
     rw [inv_inv, NNReal.coe_sub]
@@ -619,10 +665,11 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
         gcongr
       positivity
     · positivity
-  obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq F μ hp (mod_cast (zero_le p).trans_lt h2p) hp'
+  -- obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq F μ hp (mod_cast (zero_le p).trans_lt h2p) hp'
   set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
-  use t * C
-  intro u hu h2u
+  -- use t * C
+  -- intro u hu h2u
+  let C := SNormLESNormFDerivOfEqConst F μ p
   calc snorm u q μ = snorm u q (μ.restrict s) := by rw [snorm_restrict_eq h2u]
     _ ≤ snorm u p' (μ.restrict s) * t := by
         convert snorm_le_snorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
@@ -637,10 +684,9 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F] {p q : ℝ≥0} (h
         have h2u' : HasCompactSupport u := by
           apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
           exact h2u.trans subset_closure
-        rel [hC hu h2u']
+        rel [snorm_le_snorm_fderiv_of_eq μ hu h2u' hp (mod_cast (zero_le p).trans_lt h2p) hp']
     _ = (t * C) * snorm (fderiv ℝ u) p μ := by ring
 
-variable (F) in
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n`.
@@ -650,10 +696,10 @@ is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
 Note: The codomain of `u` needs to be a finite dimensional normed space.
 -/
 theorem snorm_le_snorm_fderiv [FiniteDimensional ℝ F]
-    {p : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) {s : Set E} (hs : Bornology.IsBounded s) :
-    ∃ C : ℝ≥0, ∀ (u : E → F) (_hu : ContDiff ℝ 1 u) (_h2u : u.support ⊆ s),
-    snorm u p μ ≤ C * snorm (fderiv ℝ u) p μ := by
-  refine snorm_le_snorm_fderiv_of_le F μ hp (zero_lt_one.trans_le hp) h2p ?_ hs
+    {u : E → F} {s : Set E} (hu : ContDiff ℝ 1 u) (h2u : u.support ⊆ s)
+    {p : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) (hs : Bornology.IsBounded s) :
+    snorm u p μ ≤ snormLESNormFDerivOfLeConst F μ s p p * snorm (fderiv ℝ u) p μ := by
+  refine snorm_le_snorm_fderiv_of_le μ hu h2u hp h2p ?_ hs
   norm_cast
   simp only [tsub_le_iff_right, le_add_iff_nonneg_right]
   positivity

From b3388ba766ccf8625efd23e7170093f3e3e0ea82 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 28 Jun 2024 15:58:50 +0200
Subject: [PATCH 25/29] fix docstrings

---
 .../Integral/SobolevInequality.lean           | 35 +++++++++----------
 1 file changed, 17 insertions(+), 18 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index e8c43822d32fa1..c7c7deb6b7a06e 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -341,7 +341,9 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace
 open FiniteDimensional
 
 /-- The constant factor occurring in the conclusion of `lintegral_pow_le_pow_lintegral_fderiv`.
-It only depends on `E`, `μ` and `p`. -/
+It only depends on `E`, `μ` and `p`.
+It is determined by the ratio of the measures on `E` and `ℝⁿ` and
+the operator norm of `e` (raised to suitable powers involving `p`).-/
 def lintegralPowLePowLIntegralFDerivConst (p : ℝ) : ℝ≥0 := by
   let ι := Fin (finrank ℝ E)
   have : finrank ℝ E = finrank ℝ (ι → ℝ) := by
@@ -352,9 +354,9 @@ def lintegralPowLePowLIntegralFDerivConst (p : ℝ) : ℝ≥0 := by
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
-with Haar measure. There exists a constant `C` depending only on `E`, such that the Lebesgue
-integral of the pointwise expression `|u x| ^ (n / (n - 1))` is bounded above by `C` times the
-`n / (n - 1)`-th power of the Lebesgue integral of the Fréchet derivative of `u`. -/
+with Haar measure. Then the Lebesgue integral of the pointwise expression
+`|u x| ^ (n / (n - 1))` is bounded above by a constant times the `n / (n - 1)`-th power of the
+Lebesgue integral of the Fréchet derivative of `u`. -/
 theorem lintegral_pow_le_pow_lintegral_fderiv  {u : E → F}
     (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
     {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
@@ -364,9 +366,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv  {u : E → F}
   an explicit basis in `MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux`.
   This proof is not too hard, but takes quite some steps, reasoning about the equivalence
   `e : E ≃ ℝⁿ`, relating the measures on each sides of the equivalence,
-  and estimating the derivative using the chain rule.
-  The constant `C` is determined by the ratio of the measures on `E` and `ℝⁿ` and
-  the operator norm of `e` (raised to suitable powers involving `p`). -/
+  and estimating the derivative using the chain rule. -/
   set C := lintegralPowLePowLIntegralFDerivConst μ p
   let ι := Fin (finrank ℝ E)
   have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
@@ -426,9 +426,8 @@ def snormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 := lintegralPowLePowLIntegral
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
-with Haar measure. There exists a constant `C` depending only on `E`, such that the `Lᵖ` norm of
-`u`, where `p := n / (n - 1)`, is bounded above by `C` times the `L¹` norm of the Fréchet derivative
-of `u`. -/
+with Haar measure. Then the `Lᵖ` norm of `u`, where `p := n / (n - 1)`, is bounded above by
+a constant times the `L¹` norm of the Fréchet derivative of `u`. -/
 theorem snorm_le_snorm_fderiv_one  {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
     {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
     snorm u p μ ≤ snormLESNormFDerivOneConst μ p * snorm (fderiv ℝ u) 1 μ := by
@@ -451,8 +450,8 @@ variable {F' : Type*} [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [Comple
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
 with Haar measure, let `1 ≤ p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
-There exists a constant `C` depending only on `E` and `p`, such that the `Lᵖ'` norm of `u`
-is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+Then the `Lᵖ'` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
+the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a Hilbert space.
 -/
@@ -586,8 +585,8 @@ def SNormLESNormFDerivOfEqConst [FiniteDimensional ℝ F] (p : ℝ) : ℝ≥0 :=
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
 with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
-There exists a constant `C` depending only on `E` and `p`, such that the `Lᵖ'` norm of `u`
-is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+Then the `Lᵖ'` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
+the Fréchet derivative of `u`.
 
 This is the version where the codomain of `u` is a finite dimensional normed space.
 -/
@@ -637,8 +636,8 @@ def snormLESNormFDerivOfLeConst [FiniteDimensional ℝ F] (s : Set E) (p q : ℝ
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
-There exists a constant `C` depending only on `E`, `s`, `p` and `q`, such that the `L^q` norm of `u`
-is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+Then the `L^q` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
+the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a finite dimensional normed space.
 -/
@@ -690,8 +689,8 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F]
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
 `n`, equipped with Haar measure, and let `1 < p < n`.
-There exists a constant `C` depending only on `E`, `s` and `p`, such that the `Lᵖ` norm of `u`
-is bounded above by `C` times the `Lᵖ` norm of the Fréchet derivative of `u`.
+Then the `Lᵖ` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
+the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a finite dimensional normed space.
 -/

From fa8e19d6e99d0389d382971599d2e23146c845e0 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 28 Jun 2024 16:01:55 +0200
Subject: [PATCH 26/29] add paragraph in module doc

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index c7c7deb6b7a06e..2215a1f830a002 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -29,6 +29,11 @@ In the formalization we use the operation `MeasureTheory.lmarginal` to work with
 integrals, and use `MeasureTheory.lmarginal_insert'` to conveniently push one of the integrals
 inside. The Hölder's inequality step is done using `ENNReal.lintegral_mul_prod_norm_pow_le`.
 
+The conclusions of the main results below are an estimation up to a constant multiple.
+We don't really care about this constant, other than that it only depends on some pieces of data,
+typically `E`, `μ`, `p` and sometimes also the codomain of `u` or the support of `u`.
+We state these constants as separate definitions.
+
 ## Main results
 
 * `MeasureTheory.snorm_le_snorm_fderiv_of_eq`:

From c4e9cb0d2031982192b605812d1b53ac4be089a8 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 28 Jun 2024 16:03:03 +0200
Subject: [PATCH 27/29] cleanup

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 2215a1f830a002..4a596e0682ad49 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -520,8 +520,6 @@ theorem snorm_le_snorm_fderiv_of_eq_inner  {u : E → F'}
     have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
     field_simp [this]; ring
   have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
-  -- obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_one μ hn
-  -- refine ⟨C * γ, @fun F _ _ _ u hu h2u ↦ ?_⟩
   by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
   · rw [snorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
   have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by
@@ -669,10 +667,7 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F]
         gcongr
       positivity
     · positivity
-  -- obtain ⟨C, hC⟩ := snorm_le_snorm_fderiv_of_eq F μ hp (mod_cast (zero_le p).trans_lt h2p) hp'
   set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
-  -- use t * C
-  -- intro u hu h2u
   let C := SNormLESNormFDerivOfEqConst F μ p
   calc snorm u q μ = snorm u q (μ.restrict s) := by rw [snorm_restrict_eq h2u]
     _ ≤ snorm u p' (μ.restrict s) * t := by

From 9d13e31b41b7803bfe634b789146d4be4092d3ff Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 28 Jun 2024 23:29:41 +0200
Subject: [PATCH 28/29] last review

---
 .../Integral/SobolevInequality.lean           | 26 ++++++++++++-------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 4a596e0682ad49..4f920558717855 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -348,8 +348,8 @@ open FiniteDimensional
 /-- The constant factor occurring in the conclusion of `lintegral_pow_le_pow_lintegral_fderiv`.
 It only depends on `E`, `μ` and `p`.
 It is determined by the ratio of the measures on `E` and `ℝⁿ` and
-the operator norm of `e` (raised to suitable powers involving `p`).-/
-def lintegralPowLePowLIntegralFDerivConst (p : ℝ) : ℝ≥0 := by
+the operator norm of a chosen equivalence `E ≃ ℝⁿ` (raised to suitable powers involving `p`).-/
+irreducible_def lintegralPowLePowLIntegralFDerivConst (p : ℝ) : ℝ≥0 := by
   let ι := Fin (finrank ℝ E)
   have : finrank ℝ E = finrank ℝ (ι → ℝ) := by
     rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]
@@ -362,7 +362,7 @@ compactly-supported function `u` on a normed space `E` of finite dimension `n 
 with Haar measure. Then the Lebesgue integral of the pointwise expression
 `|u x| ^ (n / (n - 1))` is bounded above by a constant times the `n / (n - 1)`-th power of the
 Lebesgue integral of the Fréchet derivative of `u`. -/
-theorem lintegral_pow_le_pow_lintegral_fderiv  {u : E → F}
+theorem lintegral_pow_le_pow_lintegral_fderiv {u : E → F}
     (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
     {p : ℝ} (hp : Real.IsConjExponent (finrank ℝ E) p) :
     ∫⁻ x, (‖u x‖₊ : ℝ≥0∞) ^ p ∂μ ≤
@@ -385,9 +385,10 @@ theorem lintegral_pow_le_pow_lintegral_fderiv  {u : E → F}
   have hc : 0 < c := addHaarScalarFactor_pos_of_isAddHaarMeasure ..
   have h2c : μ = c • ((volume : Measure (ι → ℝ)).map e.symm) := isAddLeftInvariant_eq_smul ..
   have h3c : (c : ℝ≥0∞) ≠ 0 := by simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
+  have h0C : C = (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹ := by
+    simp_rw [C, lintegralPowLePowLIntegralFDerivConst]
   have hC : C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
-    rw [show C = (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹ from rfl,
-      inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
+    rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
   rw [h2c, ENNReal.smul_def, lintegral_smul_measure, lintegral_smul_measure]
   let v : (ι → ℝ) → F := u ∘ e.symm
   have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
@@ -427,7 +428,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv  {u : E → F}
 
 /-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_one`.
 It only depends on `E`, `μ` and `p`. -/
-def snormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
+irreducible_def snormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
@@ -580,7 +581,7 @@ theorem snorm_le_snorm_fderiv_of_eq_inner  {u : E → F'}
 variable (F) in
 /-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_of_eq`.
 It only depends on `E`, `F`, `μ` and `p`. -/
-def SNormLESNormFDerivOfEqConst [FiniteDimensional ℝ F] (p : ℝ) : ℝ≥0 :=
+irreducible_def SNormLESNormFDerivOfEqConst [FiniteDimensional ℝ F] (p : ℝ) : ℝ≥0 :=
   let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
   let e : F ≃L[ℝ] F' := toEuclidean
   ‖(e.symm : F' →L[ℝ] F)‖₊ * snormLESNormFDerivOfEqInnerConst μ p * ‖(e : F →L[ℝ] F')‖₊
@@ -626,12 +627,16 @@ theorem snorm_le_snorm_fderiv_of_eq [FiniteDimensional ℝ F]
     _ ≤ C₁ * C * snorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
     _ ≤ C₁ * C * (C₂ * snorm (fderiv ℝ u) p μ) := by
       gcongr; exact snorm_le_nnreal_smul_snorm_of_ae_le_mul (eventually_of_forall h4v) p
-    _ = (C₁ * C * C₂ : ℝ≥0) * snorm (fderiv ℝ u) p μ := by push_cast; simp_rw [mul_assoc]
+    _ = SNormLESNormFDerivOfEqConst F μ p * snorm (fderiv ℝ u) p μ := by
+      simp_rw [SNormLESNormFDerivOfEqConst]
+      push_cast
+      simp_rw [mul_assoc]
+
 
 variable (F) in
 /-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_of_le`.
 It only depends on `F`, `μ`, `s`, `p` and `q`. -/
-def snormLESNormFDerivOfLeConst [FiniteDimensional ℝ F] (s : Set E) (p q : ℝ≥0) : ℝ≥0 :=
+irreducible_def snormLESNormFDerivOfLeConst [FiniteDimensional ℝ F] (s : Set E) (p q : ℝ≥0) : ℝ≥0 :=
   let p' : ℝ≥0 := (p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹)⁻¹
   (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ) * SNormLESNormFDerivOfEqConst F μ p
 
@@ -684,7 +689,8 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F]
           apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
           exact h2u.trans subset_closure
         rel [snorm_le_snorm_fderiv_of_eq μ hu h2u' hp (mod_cast (zero_le p).trans_lt h2p) hp']
-    _ = (t * C) * snorm (fderiv ℝ u) p μ := by ring
+    _ = snormLESNormFDerivOfLeConst F μ s p q * snorm (fderiv ℝ u) p μ := by
+      simp_rw [snormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 function `u` supported in a bounded set `s` in a normed space `E` of finite dimension

From 809a3c5646f0825a81b7c356ad279a3529de2111 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 28 Jun 2024 23:53:33 +0200
Subject: [PATCH 29/29] fix

---
 Mathlib/MeasureTheory/Integral/SobolevInequality.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
index 4f920558717855..12ea0661ce9d08 100644
--- a/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -428,7 +428,8 @@ theorem lintegral_pow_le_pow_lintegral_fderiv {u : E → F}
 
 /-- The constant factor occurring in the conclusion of `snorm_le_snorm_fderiv_one`.
 It only depends on `E`, `μ` and `p`. -/
-irreducible_def snormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
+irreducible_def snormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 :=
+  lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
 
 /-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped