Continuity of integral for a sub-sigma-field

Stream: Is there code for X?

[Vincent Beffara]

Do we have this?

example {α : Type*} {mα' mα : measurable_space α} {μ : measure α} {hm : mα' ≤ mα} :
  continuous (λ (x : Lp ℝ 1 (μ.trim hm)), integral μ ⇑x) :=
sorry

It looks like a composition of docs#measure_theory.continuous_integral with the fact that Lp of a sub-sigma-field is contained in Lp of the ambient sigma-field, but I am getting lost writing code like

noncomputable def ae_trim {α : Type*} {mα' mα : measurable_space α} {hm : mα' ≤ mα} {μ : measure α} :
  @ae_eq_fun α ℝ mα' _ (μ.trim hm) → @ae_eq_fun α ℝ mα _ μ :=
begin
  letI := @measure.ae_eq_setoid α ℝ mα _ μ,
  letI := @measure.ae_eq_setoid α ℝ mα' _ (μ.trim hm),
  refine quotient.lift _ _,
  { exact λ f, ⟦⟨f, ae_strongly_measurable_of_ae_strongly_measurable_trim hm f.prop⟩⟧ },
  { rintro f g hfg,
    rw [quotient.eq],
    exact ae_eq_of_ae_eq_trim hfg }
end

[Rémy Degenne]

I am not sure we have this one. I thought I wrote something like that but I can't find it: I might be thinking about docs#measure_theory.continuous_set_integral instead.
As you say, you should be able to get it from docs#measure_theory.continuous_integral and some functions to go from one Lp space to another: look at docs#measure_theory.Lp_meas_to_Lp_trim and what's around it. I am not sure but it might be what you need.

[Vincent Beffara]

Must have been in your induction principle with measurability constraints :-) I am trying to do something similar as a way to learn the API (it's going to take a while ...). Indeed docs#measure_theory.ae_strongly_measurable' feelt promising.

[Rémy Degenne]

The induction code is in PR #13129 if you want to have a look

[Vincent Beffara]

docs#measure_theory.Lp_meas_to_Lp_trim_lie (line 600 in this PR) is what I was looking for :-)

[Vincent Beffara]

Like this, it's not too bad in the end:

lemma ae_strongly_measurable.mono {m1 m2 : measurable_space α} {μ : measure α} (hm : m1 ≤ m2)
  {f : α → ℝ} :
  ae_strongly_measurable f (μ.trim hm) → ae_strongly_measurable f μ :=
by { rintro ⟨ff, h1, h2⟩, exact ⟨ff, h1.mono hm, ae_eq_of_ae_eq_trim h2⟩ }

noncomputable def Lp_trim_to_Lp {m1 m2 : measurable_space α} {μ : measure α} (hm : m1 ≤ m2) :
  Lp ℝ 1 (μ.trim hm) → Lp ℝ 1 μ :=
begin
  intro f,
  have hf := Lp.ae_strongly_measurable f,
  refine mem_ℒp.to_Lp f ⟨hf.mono hm, _⟩,
  rw ← snorm_trim_ae hm hf,
  exact Lp.snorm_lt_top f
end

lemma Lp_trim_to_Lp.ae_eq {m1 m2 : measurable_space α} {μ : measure α} {hm : m1 ≤ m2}
  {f : Lp ℝ 1 (μ.trim hm)} :
  Lp_trim_to_Lp hm f =ᵐ[μ] f :=
by simp [Lp_trim_to_Lp, mem_ℒp.coe_fn_to_Lp]

example {α : Type*} {mα' mα : measurable_space α} {μ : measure α} {hm : mα' ≤ mα} :
  continuous (λ (f : ↥(Lp ℝ 1 (μ.trim hm))), integral μ ⇑f) :=
begin
  have : ∀ {f : Lp ℝ 1 (μ.trim hm)}, integral μ f = integral (μ.trim hm) f := by {
    intro f,
    exact integral_trim_ae hm (Lp.ae_strongly_measurable f),
  },
  simp_rw this,
  exact continuous_integral
end

[Rémy Degenne]

your example does not use the two lemmas and the def, does it?

[Rémy Degenne]

Another way to define your Lp_trim_to_Lp would be to give it the value λ f, Lp_trim_to_Lp_meas ℝ ℝ 1 μ hm f (there is an implicit coercion to Lp in the end).

[Vincent Beffara]

No it doesn't use them in the end, but since the question of Lp_trim_to_Lp was raised above in the thread I kept it anyway for further reference.

[Vincent Beffara]

Yet another version:

noncomputable def Lp_trim_to_Lp' {m1 m2 : measurable_space α} {μ : measure α} (hm : m1 ≤ m2) :
  Lp ℝ 1 (μ.trim hm) → Lp ℝ 1 μ :=
λ f, (mem_ℒp_of_mem_ℒp_trim hm (Lp.mem_ℒp f)).to_Lp f

it's al the same under the hood anyway :-)