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