feat: drop sfiniteness in a lemma on L^p norm for a restricted measure (#14289)

Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: sgouezel

Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

@@ -673,7 +673,7 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F]
     · 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]
+  calc snorm u q μ = snorm u q (μ.restrict s) := by rw [snorm_restrict_eq_of_support_subset 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]
@@ -682,7 +682,7 @@ theorem snorm_le_snorm_fderiv_of_le [FiniteDimensional ℝ F]
           norm_cast
           rw [hp']
           simpa using hpq
-    _ = snorm u p' μ * t := by rw [snorm_restrict_eq h2u]
+    _ = snorm u p' μ * t := by rw [snorm_restrict_eq_of_support_subset h2u]
     _ ≤ (C * snorm (fderiv ℝ u) p μ) * t := by
         have h2u' : HasCompactSupport u := by
           apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure

Mathlib/MeasureTheory/Function/EssSup.lean

@@ -304,4 +304,28 @@ theorem coe_essSup {f : α → ℝ≥0} (hf : IsBoundedUnder (· ≤ ·) (ae μ)
       simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]; rfl
 #align ennreal.coe_ess_sup ENNReal.coe_essSup
 
+lemma essSup_restrict_eq_of_support_subset {s : Set α} {f : α → ℝ≥0∞} (hsf : f.support ⊆ s) :
+    essSup f (μ.restrict s) = essSup f μ := by
+  apply le_antisymm (essSup_mono_measure' Measure.restrict_le_self)
+  apply le_of_forall_lt (fun c hc ↦ ?_)
+  obtain ⟨d, cd, hd⟩ : ∃ d, c < d ∧ d < essSup f μ := exists_between hc
+  let t := {x | d < f x}
+  have A : 0 < (μ.restrict t) t := by
+    simp only [Measure.restrict_apply_self]
+    rw [essSup_eq_sInf] at hd
+    have : d ∉ {a | μ {x | a < f x} = 0} := not_mem_of_lt_csInf hd (OrderBot.bddBelow _)
+    exact bot_lt_iff_ne_bot.2 this
+  have B : 0 < (μ.restrict s) t := by
+    have : μ.restrict t ≤ μ.restrict s := by
+      apply Measure.restrict_mono _ le_rfl
+      apply subset_trans _ hsf
+      intro x (hx : d < f x)
+      exact (lt_of_le_of_lt bot_le hx).ne'
+    exact lt_of_lt_of_le A (this _)
+  apply cd.trans_le
+  rw [essSup_eq_sInf]
+  apply le_sInf (fun b hb ↦ ?_)
+  contrapose! hb
+  exact ne_of_gt (B.trans_le (measure_mono (fun x hx ↦ hb.trans hx)))
+
 end ENNReal

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -629,6 +629,24 @@ lemma snorm_restrict_le (f : α → F) (p : ℝ≥0∞) (μ : Measure α) (s : S
     snorm f p (μ.restrict s) ≤ snorm f p μ :=
   snorm_mono_measure f Measure.restrict_le_self
 
+/-- 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_of_support_subset {s : Set α} {f : α → F} (hsf : f.support ⊆ s) :
+    snorm f p (μ.restrict s) = snorm f p μ := by
+  by_cases hp0 : p = 0
+  · simp [hp0]
+  by_cases hp_top : p = ∞
+  · simp only [hp_top, snorm_exponent_top, snormEssSup]
+    apply ENNReal.essSup_restrict_eq_of_support_subset
+    apply Function.support_subset_iff.2 (fun x hx ↦ ?_)
+    simp only [ne_eq, ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
+    exact Function.support_subset_iff.1 hsf x hx
+  · simp_rw [snorm_eq_snorm' hp0 hp_top, snorm']
+    congr 1
+    apply setLIntegral_eq_of_support_subset
+    have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top
+    simpa [this] using hsf
+
 theorem Memℒp.restrict (s : Set α) {f : α → E} (hf : Memℒp f p μ) : Memℒp f p (μ.restrict s) :=
   hf.mono_measure Measure.restrict_le_self
 #align measure_theory.mem_ℒp.restrict MeasureTheory.Memℒp.restrict

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -673,15 +673,6 @@ 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

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -850,6 +850,16 @@ theorem lintegral_indicator_const {s : Set α} (hs : MeasurableSet s) (c : ℝ
   lintegral_indicator_const₀ hs.nullMeasurableSet c
 #align measure_theory.lintegral_indicator_const MeasureTheory.lintegral_indicator_const
 
+lemma setLIntegral_eq_of_support_subset {s : Set α} {f : α → ℝ≥0∞} (hsf : f.support ⊆ s) :
+    ∫⁻ x in s, f x ∂μ = ∫⁻ x, f x ∂μ := by
+  apply le_antisymm (setLIntegral_le_lintegral s fun x ↦ f x)
+  apply le_trans (le_of_eq _) (lintegral_indicator_le _ _)
+  congr with x
+  simp only [indicator]
+  split_ifs with h
+  · rfl
+  · exact Function.support_subset_iff'.1 hsf x h
+
 theorem setLIntegral_eq_const {f : α → ℝ≥0∞} (hf : Measurable f) (r : ℝ≥0∞) :
     ∫⁻ x in { x | f x = r }, f x ∂μ = r * μ { x | f x = r } := by
   have : ∀ᵐ x ∂μ, x ∈ { x | f x = r } → f x = r := ae_of_all μ fun _ hx => hx