# Zulip Chat Archive

## Stream: new members

### Topic: Kind of a vague question

#### 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.

#### 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)

#### 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

#### Mario Carneiro (May 10 2019 at 02:04):

wait, isn't the norm of `f`

also always finite?

#### Mario Carneiro (May 10 2019 at 02:04):

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

work?

#### 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

#### Joe (May 10 2019 at 02:21):

`#check lintegral (λ x : α, metric_space.edist (f x) 0)`

easily type checks.

#### Joe (May 10 2019 at 02:21):

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

fails.

#### 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 : α → γ}

#### Mario Carneiro (May 10 2019 at 02:37):

Use `nnnorm`

instead

#### 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.

#### Joe (May 10 2019 at 02:45):

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

#### Mario Carneiro (May 10 2019 at 02:47):

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

#### Mario Carneiro (May 10 2019 at 02:48):

this is a very common newbie mistake

#### Mario Carneiro (May 10 2019 at 02:48):

only unfold what you have to

Last updated: May 16 2021 at 05:21 UTC