-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(normed_space/inner_product): euclidean_space.norm_eq #6744
Conversation
pechersky
commented
Mar 17, 2021
Can we try to do this by fixing the diamond? I think that's the more natural approach. |
I'm only adding the lemma that expands out the norm for a term of the |
Ah, I see. Can you please give this lemma for |
@@ -229,6 +229,11 @@ lemma norm_eq {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*} | |||
[∀i, normed_group (α i)] (f : pi_Lp p hp α) : | |||
∥f∥ = (∑ (i : ι), ∥f i∥ ^ p) ^ (1/p) := rfl | |||
|
|||
lemma norm_eq_of_nat {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*} |
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.
I added this lemma because of the notational confusion between ^
when encoding rpow
or monoid.pow
. For working with nat
powers, this will allow for cleaner rewrites, with easy discharging with norm_num
. I couldn't figure out how to use . tactic.norm_num
as the out_param there.
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.
I added this lemma because of the notational confusion between
^
when encodingrpow
ormonoid.pow
. For working withnat
powers, this will allow for cleaner rewrites, with easy discharging withnorm_num
. I couldn't figure out how to use. tactic.norm_num
as the out_param there.
This seems reasonable to me, but I'd like someone like @sgouezel who's been involved in the design of the L^p spaces to decide about this, in case there's a reason we haven't had lemmas like this already.
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
bors r+ |
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>