diff --git a/Mathlib.lean b/Mathlib.lean
index 3adb89d9ccd8c0..811ea8ed77bfb5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3047,6 +3047,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/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
index 6e220092ae991a..5c7b844e018184 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 5dc427d77ecec6..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
@@ -672,6 +673,15 @@ 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 [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 [← μ.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`. -/
 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
new file mode 100644
index 00000000000000..12ea0661ce9d08
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/SobolevInequality.lean
@@ -0,0 +1,713 @@
+/-
+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.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
+
+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.
+
+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`.
+
+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`:
+  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 `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.
+-/
+
+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
+  /- 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
+          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
+          -- 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]
+          · 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 ↦ ?_)
+  -- The remainder of the computation happens within an `|s|`-fold iterated integral
+  simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
+  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 (X t) := hf.comp <| measurable_update _
+  let k : ℝ := s.card
+  have hk' : 0 ≤ 1 - k * p := by linarith only [hp]
+  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 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 -/
+
+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
+`ι → ℝ` 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
+  /- 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
+    have hι : (2:ℝ) ≤ #ι := by exact_mod_cast hp.one_lt
+    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)
+  -- we estimate |u x| using the fundamental theorem of calculus.
+  gcongr with x i
+  calc (‖u x‖₊ : ℝ≥0∞)
+      = (‖∫ xᵢ in Iic (x i), deriv (u ∘ update x i) xᵢ‖₊ : ℝ≥0∞) := by
+        -- apply the half-infinite fundamental theorem of calculus
+        have h3u : ContDiff ℝ 1 (u ∘ update x i) := hu.comp (by convert contDiff_update 1 x i)
+        have h4u : HasCompactSupport (u ∘ update x i) :=
+          h2u.comp_closedEmbedding (closedEmbedding_update x i)
+        simp [HasCompactSupport.integral_Iic_deriv_eq h3u h4u (x i)]
+    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖₊ :=
+        ennnorm_integral_le_lintegral_ennnorm _ -- apply the triangle inequality
+    _ ≤ ∫⁻ xᵢ, (‖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
+
+/-- 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 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)]
+  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. 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) :
+    ∫⁻ 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
+  `e : E ≃ ℝⁿ`, relating the measures on each sides of the equivalence,
+  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)
+  have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
+  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]
+  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 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 [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
+  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
+
+/-- 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⁻¹
+
+/-- 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. 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
+  have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
+  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, snormLESNormFDerivOneConst, ← NNReal.rpow_mul,
+    snorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',
+    inv_mul_cancel h0p.ne', NNReal.rpow_one]
+  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
+with Haar measure, let `1 ≤ p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
+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.
+-/
+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 : ℝ)⁻¹) :
+    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
+  Hilbert space. -/
+  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
+  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`
+  · 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
+  have h0p : p ≠ 0 := zero_lt_one.trans hp |>.ne'
+  have h1p : (p : ℝ) ≠ 1 := hq.one_lt.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'
+  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γ
+  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 μ := 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 γ]
+      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]
+    _ = 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`. -/
+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')‖₊
+
+/-- 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⁻¹`.
+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.
+-/
+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')‖₊
+  let v := e ∘ u
+  have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
+  have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
+  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
+      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
+    _ = 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`. -/
+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
+
+
+/-- 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 : ℝ)⁻¹)⁻¹`.
+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.
+-/
+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) :
+    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]
+    · 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
+  set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
+  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
+        rw [← ENNReal.coe_rpow_of_nonneg]
+        · 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 h2u]
+    _ ≤ (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 [snorm_le_snorm_fderiv_of_eq μ hu h2u' hp (mod_cast (zero_le p).trans_lt h2p) hp']
+    _ = 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
+`n`, equipped with Haar measure, and let `1 < p < n`.
+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.
+-/
+theorem snorm_le_snorm_fderiv [FiniteDimensional ℝ F]
+    {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
+
+end MeasureTheory