Skip to content

chore: weaken definiteness assumptions for Real interpolation #532

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fpvandoorn merged 1 commit into from
Jan 28, 2026
Merged

chore: weaken definiteness assumptions for Real interpolation #532

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Carleson/ToMathlib/BoundedCompactSupport.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 3 additions & 3 deletions Carleson/ToMathlib/BoundedFiniteSupport.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
13 changes: 6 additions & 7 deletions Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ε]

Expand Down
30 changes: 14 additions & 16 deletions Carleson/ToMathlib/RealInterpolation/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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∞}
Expand All @@ -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
Copy link
Collaborator Author

@grunweg grunweg Jan 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This TODO is obsolete for some time now.

def Subadditive_trunc [ENorm ε] (T : (α → ε₁) → α' → ε) (A : ℝ≥0∞) (f : α → ε₁) (ν : Measure α') :
Prop :=
∀ a : ℝ≥0∞, 0 < a → ∀ᵐ y ∂ν,
Expand All @@ -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}
Expand Down Expand Up @@ -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. -/
Expand All @@ -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,
Expand Down Expand Up @@ -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 ∂ν ≤
Expand All @@ -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
Expand Down Expand Up @@ -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₁⁻¹)
Expand Down Expand Up @@ -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₁⁻¹)
Expand Down Expand Up @@ -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
Expand All @@ -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 ⊤) :
Expand Down Expand Up @@ -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₁⁻¹)
Expand All @@ -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₁)
Expand Down
Loading