Assumptions for continuity in Lp

Stream: maths

[Yury G. Kudryashov]

I want to prove that docs#DomMulAct action on Lp is a docs#ContinuousSMul action. It suffices to show that indicator (c • s) is continuous in c for all measurable s. What should I assume about the action, topology, and measure for it to be true?

[Yury G. Kudryashov]

Formally, I want to have

import Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
import Mathlib.MeasureTheory.Function.ContinuousMapDense
import Mathlib.Topology.Algebra.Constructions.DomAct

variable {X M E : Type _}
  [TopologicalSpace X]
  [MeasurableSpace X] [BorelSpace X]
  [Monoid M] [TopologicalSpace M] [MeasurableSpace M] [BorelSpace M]
  [MulAction M X] [ContinuousSMul M X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [SecondCountableTopologyEither X E]
  {μ : Measure X} [SMulInvariantMeasure M X μ] [MoreAssumptions]
  [Fact (1 ≤ p)] [hp : Fact (p ≠ ∞)]

instance : ContinuousSMul Mᵈᵐᵃ (Lp E p μ)

[Yury G. Kudryashov]

It looks like for a group action, [IsRegular] should be enough.

[Antoine Chambert-Loir]

I'd rather test on compactly supported cobtinuous functions, and then it seems that Lebesgue dominated convergence does the job.

[Anatole Dedecker]

This only works for Radon measures right? Is this what you meant by IsRegular Yury?(docs#MeasureTheory.Measure.Regular)

[Anatole Dedecker]

(this is the only thing that matches so probably yes)

[Yury G. Kudryashov]

Yes, I always forget which predicates have Is

[Yury G. Kudryashov]

Do we have dominated convergence in Lp?

[Sebastien Gouezel]

I don't think so. What version of the theorem are you thinking of?

[Yury G. Kudryashov]

I don't think I'll use it now but I was thinking about "if $F_n\in L_p$ tends to $f$ a.e. everywhere and all $F_n$ are dominated by $g\in L_p$, then $F_n$ tends to $f$ in $L_p$". Probably, with different versions for $f \in L_p$ as an assumption or as another conclusion.

[Rémy Degenne]

You can get the Lp convergence from a uniform integrability assumption with Vitali's convergence theorem, docs#MeasureTheory.tendstoInMeasure_iff_tendsto_Lp and surrounding results.

[Rémy Degenne]

docs#MeasureTheory.tendsto_Lp_of_tendsto_ae has docstring "A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp."

[Yury G. Kudryashov]

Thank you!