-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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 by Bors] - feat(measure_theory/lp_space): extend the definition of Lp seminorm to p ennreal #5808
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks great, thanks!
src/measure_theory/lp_space.lean
Outdated
⟨ae_measurable.const_smul hf.1 c, | ||
lt_of_le_of_lt (le_of_eq (snorm_const_smul hf.1 c)) (ennreal.mul_lt_top ennreal.coe_lt_top hf.2)⟩ | ||
|
||
lemma snorm'_smul_le_mul_snorm' [measurable_space 𝕜] [opens_measurable_space 𝕜] {q r : ℝ} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This one probably has an snorm
version, but this can wait for later.
bors r+ |
…o p ennreal (#5808) Rename the seminorm with real exponent to `snorm'`, introduce `snorm_ess_sup` for `L\infty`, equal to the essential supremum of the norm.
Pull request successfully merged into master. Build succeeded: |
Rename the seminorm with real exponent to
snorm'
, introducesnorm_ess_sup
forL\infty
, equal to the essential supremum of the norm.