Zulip Chat Archive

Stream: new members

Topic: Kind of a vague question


view this post on Zulip Joe (May 10 2019 at 01:46):

I've already done all of these, but I'm not sure if I'm on the right track: this never occurs when I do math. So I'll ask for opinions.

Let's say we have a normed_field K and a normed space γ over K. Let f : α → γ be an integrable function, which means ∫ ∥f x∥ dx < ∞. Then the l1-norm of f is usually defined as ∫ ∥f x∥ dx.

However (called lintegral in library) has type (α → ennreal) → ennreal, thus to define the norm of f, we first need to write ∥f x∥ : ℝ as metric_space.edist (f x) 0 : ennreal, then integrate, then turn it back to real

∥f∥ := ennreal.to_real (lintegral (λ x, metric_space.edist (f x) 0))

For example, if I want to do the following reasoning

∫ ∥c • (f x)∥ dx = ∫ ∥c∥ * ∥f x∥ dx

where c : K and f x : γ. This should be killed easily by norm_smul : ∥s • x∥ = ∥s∥ * ∥x∥. But we cannot do that. Because what we need to prove is

lintegral (λ x, metric_space.edist (c • (f x)) 0) = lintegral (λ x, (metric_space.edist c 0) * (metric_space.edist (f x) 0))

And to prove this, I have to first prove an "extended" version of norm_smul:

metric_space.edist (s • x) 0 = (metric_space.edist s 0) * (metric_space.edist x 0)

I need other "extended" version of norm lemmas, like

∥x + y∥ ≤ ∥x∥ + ∥y∥
metric_space.edist (x + y) 0 ≤ metric_space.edist x 0 + metric_space.edist y 0

etc.

If this has to be the case, I guess I'll just prove those "extended" version of norm lemmas and put them somewhere? If not, then I'm not sure how to modify the definition of integral.

view this post on Zulip Mario Carneiro (May 10 2019 at 02:02):

At least metric_space.edist s 0 is unnecessary, because it's always finite (it's a normed field not a enormed field)

view this post on Zulip Mario Carneiro (May 10 2019 at 02:03):

But there should also be a definition of enorm so you don't need all these dist 0 things

view this post on Zulip Mario Carneiro (May 10 2019 at 02:04):

wait, isn't the norm of f also always finite?

view this post on Zulip Mario Carneiro (May 10 2019 at 02:04):

so doesn't lintegral (λ x, ∥c • (f x)∥) = lintegral (λ x, ∥c∥ * ∥f x∥) work?

view this post on Zulip Joe (May 10 2019 at 02:19):

I think this does't type check, because λ x : α, ∥f x∥ is of type α → ℝ, while lintegral expects a α → ennreal. Though when I tried to check the type of lintegral (λ x : α, ∥f x∥), the error message is maximum class-instance

view this post on Zulip Joe (May 10 2019 at 02:21):

#check lintegral (λ x : α, metric_space.edist (f x) 0) easily type checks.

view this post on Zulip Joe (May 10 2019 at 02:21):

#check lintegral (λ x : α, ∥f x∥) fails.

view this post on Zulip Joe (May 10 2019 at 02:22):

with

variables {α : Type u} [measure_space α]
variables {K : Type*} [normed_field K]
   {γ : Type*}  [normed_space K γ] [second_countable_topology γ] [topological_add_group γ]
variables {c : K} {f : α → γ}

view this post on Zulip Mario Carneiro (May 10 2019 at 02:37):

Use nnnorm instead

view this post on Zulip Joe (May 10 2019 at 02:44):

Yeah, this type checks. But I don't know. The problem is that metric_space.edist just appears.

view this post on Zulip Joe (May 10 2019 at 02:45):

It appears in proofs after I unwrap all the subtypes and quotients and definitions.

view this post on Zulip Mario Carneiro (May 10 2019 at 02:47):

then don't unwrap all the subtypes and quotients and definitions

view this post on Zulip Mario Carneiro (May 10 2019 at 02:48):

this is a very common newbie mistake

view this post on Zulip Mario Carneiro (May 10 2019 at 02:48):

only unfold what you have to


Last updated: May 16 2021 at 05:21 UTC