Skip to content

[Merged by Bors] - refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/LpSeminorm/Basic #38455

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

Closed
yuanyi-350 wants to merge 1 commit into from
+7 −19
Closed

[Merged by Bors] - refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/LpSeminorm/Basic #38455

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
26 changes: 7 additions & 19 deletions Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -278,12 +278,8 @@ lemma eLpNorm'_mono_enorm_ae {f : α → ε} {g : α → ε'} (hq : 0 ≤ q) (h
gcongr

lemma eLpNorm'_mono_nnnorm_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
eLpNorm' f q μ ≤ eLpNorm' g q μ := by
simp only [eLpNorm'_eq_lintegral_enorm]
gcongr ?_ ^ (1 / q)
refine lintegral_mono_ae (h.mono fun x hx => ?_)
dsimp [enorm]
gcongr
eLpNorm' f q μ ≤ eLpNorm' g q μ :=
eLpNorm'_mono_enorm_ae hq <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx

theorem eLpNorm'_mono_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) :
eLpNorm' f q μ ≤ eLpNorm' g q μ :=
Expand Down Expand Up @@ -327,12 +323,8 @@ theorem eLpNorm_mono_enorm_ae {f : α → ε} {g : α → ε'} (h : ∀ᵐ x ∂
· exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h

theorem eLpNorm_mono_nnnorm_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
eLpNorm f p μ ≤ eLpNorm g p μ := by
simp only [eLpNorm]
split_ifs
· exact le_rfl
· exact essSup_mono_ae (h.mono fun x hx => ENNReal.coe_le_coe.mpr hx)
· exact eLpNorm'_mono_nnnorm_ae ENNReal.toReal_nonneg h
eLpNorm f p μ ≤ eLpNorm g p μ :=
eLpNorm_mono_enorm_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx

theorem eLpNorm_mono_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) :
eLpNorm f p μ ≤ eLpNorm g p μ :=
Expand Down Expand Up @@ -401,13 +393,9 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM

theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by
rcases eq_zero_or_neZero μ with rfl | hμ
· simp
by_cases hp : p = 0
· simp [hp]
have : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖(C : ℝ)‖₊ := hfC.mono fun x hx => hx.trans_eq C.nnnorm_eq.symm
refine (eLpNorm_mono_ae this).trans_eq ?_
rw [eLpNorm_const _ hp (NeZero.ne μ), C.enorm_eq, one_div, ENNReal.smul_def, smul_eq_mul]
simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using
(eLpNorm_le_of_ae_enorm_bound (f := f) (C := (C : ℝ≥0∞))
(hfC.mono fun _ hx => by simpa using hx))

theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C := by
Expand Down
Loading