Kind of a vague question

Stream: new members

[Joe]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Joe]

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]

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

[Joe]

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

[Joe]

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]

Use nnnorm instead

[Joe]

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

[Joe]

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

[Mario Carneiro]

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

[Mario Carneiro]

this is a very common newbie mistake

[Mario Carneiro]

only unfold what you have to