Bochner/Interval Integrals and Type Casts

Stream: new members

[Alvan Arulandu]

I'm having trouble proving the following goal:

(∫ (x : ℝ) in 0 ..1, ↑x ^ (↑a - 1) * (1 - ↑x) ^ (↑b - 1)).re = ∫ (x : ℝ) in Ioc 0 1, x ^ (a - 1) * (1 - x) ^ (b - 1)

the first issue being the up-casting from reals to complex numbers and second being the conversion of a interval integral to a Bochner integral. What tools are available to resolve this? I'm quite new to Lean, so I really appreciate the patience

[Alvan Arulandu]

Part of the reason I need this is to prove a positivity claim, which I'm trying to do by showing that the integrand is positive in the interior. Here's the positivity goal:

∫ (x : ℝ) in Ioc 0 1, x ^ (a - 1) * (1 - x) ^ (b - 1) > 0

For both of these, a, b are non-negative reals

[Alvan Arulandu]

From what I understand, I'd have to prove 3 things.

1. (upcasts to complex integral).re = real integral [interval]
2. real integral [interval] = real bochner integral
3. positivity of real integral [interval]
   i believe the rest should follow?

[Yaël Dillies]

Do you know how to look for the lemmas you need?

[Alvan Arulandu]

I've been trying to look through the mathlib 4 api docs, but I'm not sure how to reason with these integrals and cast?

[Etienne Marion]

It looks like there's not much about real parts and integrals in the library...

[Etienne Marion]

You can try building on this:

import Mathlib

open MeasureTheory Complex

example {X : Type*} [MeasurableSpace X] (μ : Measure X) {f : X → ℂ} (hf : Integrable f μ) :
    ∫ x, (f x).re ∂μ = (∫x, f x ∂μ).re := by
  rw [← fun z ↦ congrFun RCLike.re_eq_complex_re z, ← integral_re hf]
  rfl

[Alvan Arulandu]

I was able to make some progress with Complex.ofReal and MeasureTheory's integral_ofReal. But intervalIntegral.integral_ofReal only works for closed endpoints not open? I also don't see anyway to manipulate integrability.

lemma betaIntegral_ofReal_interval {a b : ℝ} (ha : 0 < a) (hb : 0 < b):
Complex.re (∫ (x : ℝ) in (0)..1, ↑x ^ (↑a - 1:ℂ) * (1 - ↑x) ^ (↑b - 1:ℂ)) =
∫ (x : ℝ) in (0)..1, x ^ (a - 1) * (1 - x) ^ (b - 1) := by
  sorry

lemma betaPDF_integrable_cast {a b : ℝ} :
@IntervalIntegrable ℂ Complex.instNormedAddCommGroup
(fun x ↦ ↑x ^ (↑a - 1:ℂ) * (1 - ↑x) ^ (↑b - 1:ℂ)) ℙ 0 1
= @IntervalIntegrable ℝ normedAddCommGroup
(fun x ↦ x ^ (a - 1) * (1 - x) ^ (b - 1)) ℙ 0 1 := by
sorry

Kinda stuck :face_with_diagonal_mouth:

[Etienne Marion]

import Mathlib

open MeasureTheory Complex Set

lemma Complex.integral_re {X : Type*} [MeasurableSpace X] (μ : Measure X) {f : X → ℂ} (hf : Integrable f μ) :
    ∫ x, (f x).re ∂μ = (∫x, f x ∂μ).re := _root_.integral_re hf

lemma Complex.setIntegral_re {X : Type*} [MeasurableSpace X] (μ : Measure X) {s : Set X} {f : X → ℂ} (hf : IntegrableOn f s μ) :
    ∫ x in s, (f x).re ∂μ = (∫x in s, f x ∂μ).re := Complex.integral_re _ hf.integrable

lemma integrable_iff_ofReal {X : Type*} [MeasurableSpace X] {μ : Measure X}
    {f : X → ℝ} : Integrable f μ ↔ Integrable (fun x ↦ (f x : ℂ)) μ := ⟨fun hf ↦ hf.ofReal, fun hf ↦ hf.re⟩

lemma integrableOn_iff_ofReal {X : Type*} [MeasurableSpace X] {μ : Measure X} {s : Set X}
    {f : X → ℝ} : IntegrableOn f s μ ↔ IntegrableOn (fun x ↦ (f x : ℂ)) s μ := integrable_iff_ofReal

lemma betaPDF_integrable_cast {a b : ℝ} :
    IntervalIntegrable (fun x ↦ (x : ℂ) ^ (↑a - 1:ℂ) * (1 - ↑x) ^ (↑b - 1:ℂ)) ℙ 0 1 ↔
    IntervalIntegrable (fun x ↦ x ^ (a - 1) * (1 - x) ^ (b - 1)) ℙ 0 1 := by
  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by norm_num),
    intervalIntegrable_iff_integrableOn_Ioc_of_le (by norm_num),
    integrableOn_iff_ofReal]
  refine integrableOn_congr_fun (fun x hx ↦ ?_) measurableSet_Ioc
  rw [mem_Ioc] at hx
  norm_cast
  rw [← ofReal_cpow, ← ofReal_cpow]
  simp
  any_goals linarith

lemma betaIntegral_ofReal_interval {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    (∫ (x : ℝ) in (0)..1, (x : ℂ) ^ (↑a - 1:ℂ) * (1 - ↑x) ^ (↑b - 1:ℂ)).re =
      ∫ (x : ℝ) in (0)..1, x ^ (a - 1) * (1 - x) ^ (b - 1) := by
  rw [intervalIntegral.integral_of_le (by norm_num), intervalIntegral.integral_of_le (by norm_num),
    ← Complex.setIntegral_re]
  refine setIntegral_congr (measurableSet_Ioc) fun x hx ↦ ?_
  rw [mem_Ioc] at hx
  norm_cast
  rw [← ofReal_cpow, ← ofReal_cpow]
  simp
  any_goals linarith
  sorry

This should help

[Alvan Arulandu]

thank you so much!!! this was enough for me to figure out the rest, all goals solved! beta distribution now formalized #16773