ISO help with theorem using MemLp and IdentDistrib

Stream: new members

[Becker A.]

I'm trying to solve this extracted goal:

-- import Mathlib.Topology.Basic

-- #check TopologicalSpace

import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Moments.Basic
import Mathlib.MeasureTheory.Function.L1Space.Integrable
import Mathlib.Data.Finset.Range

open Finset MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal

example
  {Ω : Type u_1} [m : MeasurableSpace Ω]
  {n : ℕ}
  {X : Fin (n + 1) → Ω → ℝ}
  {P : Measure Ω} [inst : IsProbabilityMeasure P]
  (hX : ∀ (i : Fin (n + 1)), MemLp (X i) 2 P)
  (hXIndep : iIndepFun X P)
  (hXIdent : ∀ (i j : Fin (n + 1)), IdentDistrib (X i) (X j) P P)
  (i : Fin (n + 1))
  (hi : i ∈ univ)
  (j : Fin (n + 1))
  (hj : j ∈ univ)
  : MemLp (X i * X j) 1 P
  := sorry

I've solved something similar so far, namely MemLp (X i ^ 2) 1 P, and I was hoping to reduce the above problem to this solved goal using the IdentDistrib input hXIdent. but I haven't found any mathlib theorem that would help me do that.

any advice/solutions? i.e., can I solve this with the given inputs or do I need extra things? thanks!

[Rémy Degenne]

You can prove it with rw [memLp_one_iff_integrable]; exact MemLp.integrable_mul (hX _) (hX _)
The main takeaway is that the standard way to spell MemLp X 1 P is Integrable X P.

[Becker A.]

gotcha, yeah I actually started with Integrable and called rw [<- memLp_one_iff_integrable] before extracting the goal. oops :upside_down:

thanks for the manual search help! :folded_hands:

[Becker A.]

followup problem, similar vibe:

import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Moments.Basic
import Mathlib.MeasureTheory.Function.L1Space.Integrable
import Mathlib.Data.Finset.Range

import SampleVariance.MomentsOfSums
import SampleVariance.SampleStatisticsDefs

open Finset MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal


theorem moment_2_biased_svar.extracted_1_1.{u_1}
  {Ω : Type u_1} [m : MeasurableSpace Ω]
  {n : ℕ}
  {X : Fin (n + 1) → Ω → ℝ}
  {P : Measure Ω} [inst : IsProbabilityMeasure P]
  (hX : ∀ (i : Fin (n + 1)), MemLp (X i) 4 P)
  (hXIndep : iIndepFun X P)
  (hXIdent : ∀ (i j : Fin (n + 1)), IdentDistrib (X i) (X j) P P)
  (i : Fin (n + 1))
  (hi : i ∈ univ)
  (j : Fin (n + 1))
  (hj : j ∈ univ)
  : Integrable (fun a ↦ (X i ^ 2 * X j ^ 2) a) P
  := by
  sorry

tried apply MemLp.integrable_mul, got an error and I don't know if its fixable:

failed to synthesize
  ENNReal.HolderTriple ?p ?q 1

thanks!

[Aaron Liu]

you can do refine MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_

[Becker A.]

cool I'll try it, thanks!

...wait is (p := 2) syntax for specifying implicit variables manually?

[Aaron Liu]

yes

[Becker A.]

oh very cool! I've been curious about that for a while but never found any documentation on it. thanks for the cool trick!