Measurable set of function that maps to inequalities

Stream: new members

[Josha Dekker]

I am trying to establish the following result in Lean, which I need to introduce some useful results for the Gamma distribution, but I cannot fill in one of the sorry's (the one that is followed by "I cannot finish up this step", the other ones are omitted for brevity of the MWE and I can send a complete version if preferred). I have to establish that a certain set is measurable, but I'm not sure if that is possible or whether my approach is incorrect... I'm hoping that someone can point out what I'm doing wrong/how I should proceed/what would be a better approach!

import Mathlib.Analysis.SpecialFunctions.Gaussian
import Mathlib.Probability.Notation
import Mathlib.Probability.Cdf

open scoped ENNReal NNReal Real
open MeasureTheory Real Set Filter Topology

lemma lintegral_eq_lintegral_Ici_add_Iio (f : ℝ → ℝ≥0∞) (c : ℝ) :
    ∫⁻ x, f x = (∫⁻ x in Ici c, f x) + ∫⁻ x in Iio c, f x := by sorry

noncomputable
def gammaPdfReal (a r x : ℝ) : ℝ :=
  if 0 ≤ x then r^a/(Real.Gamma a) * (↑x)^(a-1) * Real.exp (-(r * ↑x)) else 0

/-- The PDF of the gamma Distribution on the extended real Numbers-/
noncomputable
def gammaPdf (a r x : ℝ) : ℝ≥0∞ := ENNReal.ofReal (gammaPdfReal a r x)

/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function. -/
lemma pow_exp_integral_Ioi_insert_1 {a r : ℝ} (ha : a > 0) (hr : r > 0) :
    ∫ (t : ℝ) in Ioi 0, (r ^ a / Gamma a) * t ^ (a - 1) * rexp (-(r * t))
    = 1 := by sorry

lemma integral_gammaPdf_eq_one (a r : ℝ) (ha : 0 < a) (hr : 0 < r) : ∫⁻ x, gammaPdf a r x = 1 := by
  rw [lintegral_eq_lintegral_Ici_add_Iio (gammaPdf a r) 0, ← ENNReal.toReal_eq_one_iff]
  have leftSide : ∫⁻ x in Iio 0, gammaPdf a r x = 0 := by sorry -- Proof steps removed for brevity
  have rightSide :
      ∫⁻ x in Ici 0, gammaPdf a r x = ∫⁻ x in Ici 0, ENNReal.ofReal (r^a/(Real.Gamma a) * x^(a-1) * rexp (-(r * x))) := sorry -- Proof steps removed for brevity
  simp only [leftSide, add_zero]
  rw [rightSide]
  rw [← integral_eq_lintegral_of_nonneg_ae]
  · rw [MeasureTheory.integral_Ici_eq_integral_Ioi, pow_exp_integral_Ioi_insert_1 ha hr]
  · unfold EventuallyLE
    simp only [Pi.zero_apply]
    rw [ae_restrict_iff]
    simp only [mem_Ici]
    · sorry -- Proof steps removed for brevity
    · apply Measurable.setOf
      sorry -- I cannot finish up this step!
  · sorry -- Proof steps removed for brevity

[Yaël Dillies]

What's the goal state? (I'm currently stuck compiling all of mathlib)

[Josha Dekker]

This is the state at the sorry:

ar: ℝ
ha: 0 < a
hr: 0 < r
leftSide: ∫⁻ (x : ℝ) in Iio 0, gammaPdf a r x = 0
rightSide: ∫⁻ (x : ℝ) in Ici 0, gammaPdf a r x =
  ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ Measurable fun a_1 => 0 ≤ r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1))

[Yaël Dillies]

Does measurability do it?

[Josha Dekker]

And this is the state just before rw [ae_restrict_iff]

ar: ℝ
ha: 0 < a
hr: 0 < r
leftSide: ∫⁻ (x : ℝ) in Iio 0, gammaPdf a r x = 0
rightSide: ∫⁻ (x : ℝ) in Ici 0, gammaPdf a r x =
  ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ici 0), 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

[Josha Dekker]

Yaël Dillies said:

Does measurability do it?

No, "tactic 'aesop' failed, failed to prove the goal after exhaustive search."

[Yaël Dillies]

Try adding Measurable (· ^ (a - 1) : ℝ → ℝ) to the context and run measurability again.

[Josha Dekker]

Like this?

apply Measurable.setOf
      have : Measurable (· ^ (a - 1) : ℝ → ℝ) := sorry
      measurability

That did not work

[Josha Dekker]

I think the problem is that the function actually maps a_1 to an inequality, so I'm not sure if measurability (or at least I) have a clear picture of how to deal with that...

[Yaël Dillies]

Wait what do you mean?

[Josha Dekker]

This line from the state, it maps a_1 to 0 <= ..., right?

Measurable fun a_1 => 0 ≤ r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1))

[Yaël Dillies]

I see a function of the form fun x ↦ constant * x ^ positive_constant * something_continuous

[Yaël Dillies]

Yeah well that's because you use docs#Measurable.setOf

[Yaël Dillies]

This is to translate between measurability of predicates and measurability of their associated sets.

[Yaël Dillies]

What's the goal state just before Measurable.setOf?

[Josha Dekker]

⊢ MeasurableSet {x | 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))}

[Yaël Dillies]

That looks great! Have you tried applying docs#MeasurableSet.preimage ?

[Josha Dekker]

Yaël Dillies said:

This is to translate between measurability of predicates and measurability of their associated sets.

Thank you, I misinterpreted that one!

[Yaël Dillies]

You will want docs#measurableSet_Ici

[Josha Dekker]

Thank you! Now I just have to establish measurability of the function, that part should be fine!

[Rémy Degenne]

I investigated a bit: apparently measurability fails to show Measurable fun x => r * x. It should be smarter than that.

import Mathlib.Analysis.SpecialFunctions.Gaussian
import Mathlib.Probability.Notation
import Mathlib.Probability.Cdf

open scoped ENNReal NNReal Real
open MeasureTheory Real Set Filter Topology

lemma lintegral_eq_lintegral_Ici_add_Iio (f : ℝ → ℝ≥0∞) (c : ℝ) :
    ∫⁻ x, f x = (∫⁻ x in Ici c, f x) + ∫⁻ x in Iio c, f x := by sorry

noncomputable
def gammaPdfReal (a r x : ℝ) : ℝ :=
  if 0 ≤ x then r^a/(Real.Gamma a) * (↑x)^(a-1) * Real.exp (-(r * ↑x)) else 0

/-- The PDF of the gamma Distribution on the extended real Numbers-/
noncomputable
def gammaPdf (a r x : ℝ) : ℝ≥0∞ := ENNReal.ofReal (gammaPdfReal a r x)

/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function. -/
lemma pow_exp_integral_Ioi_insert_1 {a r : ℝ} (ha : a > 0) (hr : r > 0) :
    ∫ (t : ℝ) in Ioi 0, (r ^ a / Gamma a) * t ^ (a - 1) * rexp (-(r * t))
    = 1 := by sorry

lemma integral_gammaPdf_eq_one (a r : ℝ) (ha : 0 < a) (hr : 0 < r) : ∫⁻ x, gammaPdf a r x = 1 := by
  rw [lintegral_eq_lintegral_Ici_add_Iio (gammaPdf a r) 0, ← ENNReal.toReal_eq_one_iff]
  have leftSide : ∫⁻ x in Iio 0, gammaPdf a r x = 0 := by sorry -- Proof steps removed for brevity
  have rightSide :
      ∫⁻ x in Ici 0, gammaPdf a r x = ∫⁻ x in Ici 0, ENNReal.ofReal (r^a/(Real.Gamma a) * x^(a-1) * rexp (-(r * x))) := sorry -- Proof steps removed for brevity
  simp only [leftSide, add_zero]
  rw [rightSide]
  rw [← integral_eq_lintegral_of_nonneg_ae]
  · rw [MeasureTheory.integral_Ici_eq_integral_Ioi, pow_exp_integral_Ioi_insert_1 ha hr]
  · unfold EventuallyLE
    simp only [Pi.zero_apply]
    rw [ae_restrict_iff]
    simp only [mem_Ici]
    · sorry -- Proof steps removed for brevity
    · refine measurableSet_le measurable_const ?_
      refine Measurable.mul ?_ ?_
      · measurability
      · apply (Measurable.neg ?_).exp
        -- measurability still fails here
        exact measurable_id.const_mul _
  · sorry -- Proof steps removed for brevity

[Josha Dekker]

Thank you, that closes up my argument!