chore: weaken definiteness assumptions for Real interpolation (#532)

The main theorem still requires it; a number of intermediate lemmas can
be weakened.

Author: grunweg

Carleson/ToMathlib/BoundedCompactSupport.lean

@@ -124,15 +124,15 @@ theorem restrict {s : Set X} (hf : BoundedCompactSupport f μ) :
 end ContinuousENorm
 
 
-section  ENormedAddCommMonoid
-variable [TopologicalSpace E] [ENormedAddCommMonoid E]
+section ESeminormedAddCommMonoid
+variable [TopologicalSpace E] [ESeminormedAddCommMonoid E]
 
 /-- Bounded compactly supported functions are in all `Lᵖ` spaces. -/
 theorem memLp [IsFiniteMeasureOnCompacts μ] (hf : BoundedCompactSupport f μ) (p : ℝ≥0∞) :
     MemLp f p μ :=
   hf.boundedFiniteSupport.memLp p
 
-end ENormedAddCommMonoid
+end ESeminormedAddCommMonoid
 
 section NormedAddCommGroup
 

Carleson/ToMathlib/BoundedFiniteSupport.lean

@@ -54,15 +54,15 @@ theorem eLpNorm_lt_top : eLpNorm f ∞ μ < ∞ := bfs.memLp_top.eLpNorm_lt_top
 
 end Includebfs
 
-section  ENormedAddMonoid
-variable [TopologicalSpace E] [ENormedAddMonoid E]
+section ESeminormedAddMonoid
+variable [TopologicalSpace E] [ESeminormedAddMonoid E]
 
 /-- Bounded finitely supported functions are in all `Lᵖ` spaces. -/
 theorem memLp (hf : BoundedFiniteSupport f μ) (p : ℝ≥0∞) : MemLp f p μ :=
   hf.memLp_top.mono_exponent_of_measure_support_ne_top
     (fun _ ↦ notMem_support.mp) hf.measure_support_lt.ne le_top
 
-end ENormedAddMonoid
+end ESeminormedAddMonoid
 
 section NormedAddCommGroup
 

Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean

@@ -74,21 +74,20 @@ lemma eLorentzNorm_eq_zero_of_ae_enorm_zero [ESeminormedAddMonoid ε] {f : α 
   intro p_ne_top
   exact eLorentzNorm'_eq_zero_of_ae_enorm_zero h p_ne_zero p_ne_top
 
-lemma eLorentzNorm'_eq_zero_of_ae_zero [ENormedAddMonoid ε] {f : α → ε}
-  (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (h : f =ᵐ[μ] 0) :
+lemma eLorentzNorm'_eq_zero_of_ae_zero [ESeminormedAddMonoid ε] {f : α → ε}
+    (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (h : f =ᵐ[μ] 0) :
     eLorentzNorm' f p q μ = 0 := by
   apply eLorentzNorm'_eq_zero_of_ae_enorm_zero _ p_ne_zero p_ne_top
   filter_upwards [h]
-  simp
+  simp +contextual
 
-lemma eLorentzNorm_eq_zero_of_ae_zero [ENormedAddMonoid ε] {f : α → ε} (h : f =ᵐ[μ] 0) :
+lemma eLorentzNorm_eq_zero_of_ae_zero [ESeminormedAddMonoid ε] {f : α → ε} (h : f =ᵐ[μ] 0) :
     eLorentzNorm f p q μ = 0 := by
   apply eLorentzNorm_eq_zero_of_ae_enorm_zero
   filter_upwards [h]
-  simp
-
+  simp +contextual
 
-section ENormedAddMonoid
+section ENormedAddMonoid -- TODO: do all of these results require positive definiteness?
 
 variable {ε : Type*} [TopologicalSpace ε] [ENormedAddMonoid ε]
 

Carleson/ToMathlib/RealInterpolation/Main.lean

@@ -38,8 +38,8 @@ variable {α α' ε E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Mea
   {p p' q p₀ q₀ p₁ q₁ : ℝ≥0∞}
   {C₀ C₁ : ℝ≥0} {μ : Measure α} {ν : Measure α'}
   [TopologicalSpace E] [TopologicalSpace E₁] [TopologicalSpace E₂] [TopologicalSpace E₃]
-  [ENormedAddCommMonoid E]
-  [ENormedAddCommMonoid E₁] [ENormedAddCommMonoid E₂] [ENormedAddCommMonoid E₃]
+  [ESeminormedAddCommMonoid E]
+  [ESeminormedAddCommMonoid E₁] [ESeminormedAddCommMonoid E₂] [ESeminormedAddCommMonoid E₃]
   [MeasurableSpace E] [BorelSpace E]
   [MeasurableSpace E₃] [BorelSpace E₃]
   {f : α → E₁} {t : ℝ≥0∞}
@@ -50,13 +50,11 @@ variable {α α' ε E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Mea
 ## Definitions -/
 namespace MeasureTheory
 
-variable {ε₁ ε₂ : Type*} [TopologicalSpace ε₁] [ENormedAddMonoid ε₁] [TopologicalSpace ε₂] [ENormedAddMonoid ε₂]
+variable {ε₁ ε₂ : Type*} [TopologicalSpace ε₁] [ESeminormedAddMonoid ε₁] [TopologicalSpace ε₂] [ESeminormedAddMonoid ε₂]
 
 def Subadditive [ENorm ε] (T : (α → ε₁) → α' → ε) : Prop :=
   ∃ A ≠ ⊤, ∀ (f g : α → ε₁) (x : α'), ‖T (f + g) x‖ₑ ≤ A * (‖T f x‖ₑ + ‖T g x‖ₑ)
 
--- TODO: generalise `trunc` and `truncCompl` take allow an ENormedAddMonoid as codomain,
--- then generalise this definition also
 def Subadditive_trunc [ENorm ε] (T : (α → ε₁) → α' → ε) (A : ℝ≥0∞) (f : α → ε₁) (ν : Measure α') :
     Prop :=
   ∀ a : ℝ≥0∞, 0 < a → ∀ᵐ y ∂ν,
@@ -70,7 +68,7 @@ def AESubadditiveOn [ENorm ε] (T : (α → ε₁) → α' → ε) (P : (α →
 
 namespace AESubadditiveOn
 
-variable [TopologicalSpace ε] [ENormedAddMonoid ε] {ν : Measure α'}
+variable [TopologicalSpace ε] [ESeminormedAddMonoid ε] {ν : Measure α'}
   {u : α → ε₁} {T : (α → ε₁) → α' → ε₂}
 
 lemma antitone {T : (α → ε₁) → α' → ε} {P P' : (α → ε₁) → Prop}
@@ -273,7 +271,7 @@ variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Measur
 -/
 namespace MeasureTheory
 
-variable {ε₁ ε₂ : Type*} [TopologicalSpace ε₁] [ENormedAddMonoid ε₁] [TopologicalSpace ε₂] [ENormedAddMonoid ε₂]
+variable {ε₁ ε₂ : Type*} [TopologicalSpace ε₁] [ESeminormedAddMonoid ε₁] [TopologicalSpace ε₂] [ESeminormedAddMonoid ε₂]
 
 /-- Proposition that expresses that the map `T` map between function spaces preserves
     AE strong measurability on L^p. -/
@@ -292,7 +290,7 @@ lemma estimate_distribution_Subadditive_trunc {f : α → ε₁} {T : (α → ε
   exact h a ha
 
 lemma rewrite_norm_func {q : ℝ} {g : α' → E}
-    [TopologicalSpace E] [ENormedAddCommMonoid E] (hq : 0 < q) {A : ℝ≥0} (hA : 0 < A)
+    [TopologicalSpace E] [ESeminormedAddCommMonoid E] (hq : 0 < q) {A : ℝ≥0} (hA : 0 < A)
     (hg : AEStronglyMeasurable g ν) :
     ∫⁻ x, ‖g x‖ₑ ^ q ∂ν =
     ENNReal.ofReal ((2 * A) ^ q * q) * ∫⁻ s,
@@ -323,7 +321,7 @@ lemma rewrite_norm_func {q : ℝ} {g : α' → E}
     rw [ENNReal.ofReal_rpow_of_pos ha, ENNReal.ofReal_mul (by positivity)]
 
 lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁}
-    [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] [TopologicalSpace E₂] [ENormedAddCommMonoid E₂]
+    [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] [TopologicalSpace E₂] [ESeminormedAddCommMonoid E₂]
     (hq : 0 < q) (tc : StrictRangeToneCouple) {A : ℝ≥0} (hA : 0 < A)
     (ht : Subadditive_trunc T A f ν) (hTf : AEStronglyMeasurable (T f) ν) :
   ∫⁻ x : α', ‖T f x‖ₑ ^ q ∂ν ≤
@@ -338,7 +336,7 @@ lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁}
 
 -- TODO: the infrastructure can perhaps be improved here
 @[measurability, fun_prop]
-theorem ton_measurable_eLpNorm_trunc [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (tc : ToneCouple) :
+theorem ton_measurable_eLpNorm_trunc [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (tc : ToneCouple) :
     Measurable (fun x ↦ eLpNorm (trunc f (tc.ton x)) p₁ μ) := by
   change Measurable ((fun t : ℝ≥0∞ ↦ eLpNorm (trunc f t) p₁ μ) ∘ (tc.ton))
   have tone := tc.ton_is_ton
@@ -414,7 +412,7 @@ lemma simplify_factor_rw_aux₁ (a b c d e f : ℝ≥0∞) :
     a * b * c * d * e * f = c * (a * e) * (b * f * d) := by ring_nf
 
 lemma simplify_factor₀ {D : ℝ≥0∞}
-    [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hq₀' : q₀ ≠ ⊤)
+    [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (hq₀' : q₀ ≠ ⊤)
     (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁)
     (ht : t ∈ Ioo 0 1)
     (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
@@ -469,7 +467,7 @@ lemma simplify_factor₀ {D : ℝ≥0∞}
   · exact Or.inr (d_ne_zero_aux₀ hF)
 
 lemma simplify_factor₁ {D : ℝ≥0∞}
-    [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hq₁' : q₁ ≠ ⊤)
+    [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (hq₁' : q₁ ≠ ⊤)
     (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁)
     (ht : t ∈ Ioo 0 1)
     (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
@@ -799,7 +797,7 @@ lemma combine_estimates₁ {A : ℝ≥0} (hA : 0 < A)
       exact ofReal_toReal_eq_iff.mpr q_ne_top
     · rw [toReal_inv, ENNReal.rpow_inv_rpow q'pos.ne']
 
-lemma simplify_factor₃ [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hp₀ : 0 < p₀) (hp₀' : p₀ ≠ ⊤) (ht : t ∈ Ioo 0 1)
+lemma simplify_factor₃ [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (hp₀ : 0 < p₀) (hp₀' : p₀ ≠ ⊤) (ht : t ∈ Ioo 0 1)
     (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hp₀p₁ : p₀ = p₁) :
     C₀ ^ q₀.toReal * (eLpNorm f p μ ^ p.toReal) ^ (q₀.toReal / p₀.toReal) =
     (↑C₀ * eLpNorm f p μ) ^ q₀.toReal := by
@@ -808,7 +806,7 @@ lemma simplify_factor₃ [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hp
   · exact (toReal_pos hp₀.ne' hp₀').ne'
   positivity
 
-lemma simplify_factor_aux₄ [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hq₀' : q₀ ≠ ⊤)
+lemma simplify_factor_aux₄ [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (hq₀' : q₀ ≠ ⊤)
     (hp₀ : p₀ ∈ Ioc 0 q₀) (ht : t ∈ Ioo 0 1)
     (hp₀p₁ : p₀ = p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
     (hF : eLpNorm f p μ ∈ Ioo 0 ⊤) :
@@ -836,7 +834,7 @@ lemma simplify_factor_aux₄ [TopologicalSpace E₁] [ENormedAddCommMonoid E₁]
   · exact hp' ▸ d_pos_aux₀ hF |>.ne'
   · exact hp' ▸ d_ne_top_aux₀ hF
 
-lemma simplify_factor₄ {D : ℝ≥0∞} [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hq₀' : q₀ ≠ ⊤)
+lemma simplify_factor₄ {D : ℝ≥0∞} [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (hq₀' : q₀ ≠ ⊤)
     (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1)
     (hp₀p₁ : p₀ = p₁)
     (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
@@ -852,7 +850,7 @@ lemma simplify_factor₄ {D : ℝ≥0∞} [TopologicalSpace E₁] [ENormedAddCom
   rw [simplify_factor₀ (ht := ht) (hD := hD)] <;> assumption
 
 
-lemma simplify_factor₅ {D : ℝ≥0∞} [TopologicalSpace E₁] [ENormedAddCommMonoid E₁] (hq₁' : q₁ ≠ ⊤)
+lemma simplify_factor₅ {D : ℝ≥0∞} [TopologicalSpace E₁] [ESeminormedAddCommMonoid E₁] (hq₁' : q₁ ≠ ⊤)
     (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁)
     (ht : t ∈ Ioo 0 1)
     (hp₀p₁ : p₀ = p₁)