equivalence between ℓp and Lp

Stream: maths

[Jireh Loreaux]

I was starting to implement the equivalence between lp and measure_theory.Lp (in the case of counting measure on full power set of the domain for functions α → E) in part as a way to teach myself the measure theory portion of the library. However, I immediately ran into issues and I need some questions answered:

1. Why is docs#measure_theory.snorm zero if p = 0? I would have expected something like μ (function.support f). This definition prohibits an equivalence in this case.
2. Will I need to restrict the domain α to be countable?

My concern in (2) is in the p = ∞ case. In particular, if the domain α was something like set.Icc (0 : ℝ) 1 and f : α → ℝ was given by f x = ↑x, then we would have mem_ℓp f ∞ but I don't think we would have measure_theory.mem_𝓛p f ∞, with the latter failing only because f is not a.e. strongly measurable (at least, I think it's not, but I would be content to be shown otherwise).

In case p < ∞, one should be able to show that the support of f is countable, and then one can show f is a pointwise limit of simple functions and hence is strongly measurable.

[Anatole Dedecker]

I would say the natural equivalence should be with Lp for the counting mesure on the measurable space $(X, \top)$ so measurability shouldn't be an issue

[Anatole Dedecker]

I mean, somehow this is the "natural" sigma algebra for the counting measure, right ?

[Jireh Loreaux]

Yes, I agree, but I think the f I described above is not docs#measure_theory.ae_strongly_measurable, which is a requirement for measure_theory.mem_𝓛p

[Jireh Loreaux]

I guess another way to ask this is: if α is equipped with ⊤ : measurable_space α, does that imply every function is strongly measurable?

[Anatole Dedecker]

Yes. For your example, docs#continuous.strongly_measurable should mean that it is trongly measurable right ? But that doesn't help with the general case

[Anatole Dedecker]

Oh wait maybe it does

[Anatole Dedecker]

Just put the discrete topology on the domain

[Anatole Dedecker]

But that shouldn't be the right way of doing it anyway

[Jireh Loreaux]

ummm... no? The discrete topology on an uncountable set is not a second countable topology.

[Jireh Loreaux]

Again, if that f I described above is strongly measurable, then what is the sequence of simple functions which converges to it pointwise?

[Anatole Dedecker]

Yes but you need only docs#second_countable_topology_either, so having a second countable codomain works right? This won't work in general though. Sorry if I'm saying stupid things, I should let someone who knows this better than me answer

[Jireh Loreaux]

Yeah, okay, but that's easy to break too (as you mentioned), just map instead into lp (lambda (_ : real), real) top

[Rémy Degenne]

The choice of snorm being uniformly 0 for p=0 is a bit of a junk value, but it makes many lemmas true for all p instead of 0 < p. Apart from that, it makes Lp E 0 μ equal to the space of ae_strongly_measurable functions (equivalence classes of), which corresponds to the usual L0 notation. That last point is not important: we don't use Lp E 0 μ for that space, we use measure_theory.ae_eq_fun.

I tried replacing the definition of snorm at 0 by μ (function.support f) and it looks like most lemmas used to compare snorm at different exponents now require an additional 0 < p. Also various other results now break at 0, like snorm (c • f) p μ = (∥c∥₊ : ℝ≥0∞) * snorm f p μ, or (∀ᵐ x ∂μ, ∥f x∥ ≤ c * ∥g x∥) → ∥f∥ ≤ c * ∥g∥.

In summary, Lp 0 was not considered a useful object, hence snorm at 0 was defined to be the junk value that makes as many lemmas true at 0 as possible. If you have a meaningful value for it that turns Lp E 0 μ into something useful, the slight inconvenience of a few 0 < p hypotheses could be worth it. Otherwise, I guess you can define your equivalence for 0 < p?