Real interpolation theorem

Stream: Carleson

[Jim Portegies]

Just a heads up about an extra assumption in the Real Interpolation Theorem: Part of what one needs to prove is that the map T preserves strong measurability on L^p, where L^p is the interpolated space. However, I think this is something one cannot prove but needs to assume, because a quasilinear map seems to give a lot of flexibility to artificially bring in some non-measurability. In the references that I find, the assumption is usually that T preserves measurability on L^p0 + L^p1, but currently I'm leaning towards just assuming the preservation of measurability on L^p directly; I think that may be enough.

[Floris van Doorn]

The assumptions as currently stated have (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) which implies measurability of T f for f in L^p0 or L^p1. From that you should be able to conclude that it preserves measurability on L^p, right? It would be very nice if we don't need to add an additional assumption.

[Jim Portegies]

I think I have a counterexample to that

[Jim Portegies]

If T were linear, then I believe preservation of measurability on L^p0 and L^p1 is enough, but if not, we can take an f in L^p\ L^p1 and g in L^p\L^p0 and just define T(f + g) as something like 1 plus delta times the indicator of a non-measurable set. I believe you can set this up in such a way that T is quasilinear, but it doesn't preserve measurability this way.

[Jim Portegies]

Am I missing something?

[Floris van Doorn]

Oh, I see what you mean. Yes, you're right, I implicitly used linearity. So please add an additional measurability condition. If you think the measurability on L^p is enough, then that's great. Measurability of L^p0 + L^p1 is definitely also fine.

[Jim Portegies]

I have a question about the variables in RealInterpolation.lean. The typeclass resolution fails, when I try to use distribution_smul_left from WeakType.lean. I lack full understanding, but I think it has some trouble understanding that 𝕜 in the one file and ℝ in the other file are the same (in fact when I debug with set_option trace.Meta.synthInstance true it seems to say at some point that [NormedSpace ℝ E₂] = [NormedSpace ℝ E₂] fails). I get it to work if I remove the variable [NontriviallyNormedField ℝ] mentioned in the beginning of the file. Is this ok? Or is there another solution here?

[Ruben Van de Velde]

Jim Portegies said:

variable [NontriviallyNormedField ℝ]

This should not exist in any code

[Jim Portegies]

Thanks! I'll remove it then

[Edward van de Meent]

indeed. this leads to multiple (possibly non-identical) definitions for multiplication, addition, etc., and there is no proof at all that these might be related, let alone that they distribute over one-another.

[Floris van Doorn]

Oops! Originally that field was a 𝕜, but I forgot to remove that extra type-class. My bad!

[Floris van Doorn]

@Jim Portegies I realized that the Subadditive hypothesis is too strong: we want to only assume this for functions that are in $L^{p_1} + L^{p_2}$. I changed the statement in the repository (and I apologize for any merge conflicts).

[Jim Portegies]

Thanks for letting me know, I think my proof so far doesn't use anything beyond this