Lifting real to complex

Stream: new members

[Josha Dekker]

In a review of a PR, it was suggested to me to extend the following result to the complex numbers. I have tried doing so, but I find the coercions hard to work with; the last three steps of my proof currently are invalid over the complex numbers, while I would assume that most steps of the proof should carry over for complex numbers, as it is all written in terms of Bochner integrals... is it a matter of putting coercion arrows everywhere? As of now, every step in the Calc proof but the second is raising an error...

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

open scoped ENNReal NNReal

open MeasureTheory Real Set Filter Topology
open Measure


/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function. -/
lemma pow_exp_integral_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Real.exp (-(r * t))
    = (1 / r) ^ a * Real.Gamma (a) := by
  have hri : 0 < 1/r := by positivity
  calc ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Real.exp (-(r * ↑t))
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a-1) * (r * ↑t) ^ (a - 1) * Real.exp (-(r * t)) := by
      apply MeasureTheory.set_integral_congr
      · simp
      · intro x (hx : 0 < x)
        simp_rw [mul_eq_mul_right_iff]
        rw [mul_rpow hr.le hx.le]
        simp_rw [← mul_assoc, ← mul_rpow hri.le hr.le,
          mul_comm (1 / r), mul_div, mul_one, div_self hr.ne', one_rpow, one_mul, true_or]
    _ =  |1 / r| * ∫ (t : ℝ) in Ioi (r * 0), (1 / r) ^ (a-1) * t ^ (a - 1) * Real.exp (-t) := by
      rw [integral_comp_mul_left_Ioi (fun t ↦ (1 / r) ^ (a-1) * t ^ (a - 1) * exp (-t)) (0 : ℝ) hr]
      simp
    _ =  1 / r * ∫ (t : ℝ) in Ioi 0, ↑(1 / r) ^ (a-1) • t ^ (a - 1) * Real.exp (-t) := by
      have : Ioi (r * 0) = Ioi 0 := by refine Ioi_inj.mpr (by simp)
      rw [this, abs_of_nonneg hri.le]
      rfl
    _ =  1 / r * ∫ (t : ℝ) in Ioi 0, ↑(1 / r) ^ (a-1) • (t ^ (a - 1) * Real.exp (-t)) := by
      congr
      ext x
      exact smul_mul_assoc _ _ _
    _ =  1 / r * ↑(1 / r) ^ (a-1) • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Real.exp (-t)) := by
      rw [integral_smul]
    _ = ↑(1 / r) ^ a • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Real.exp (-t)) := by
      have : (1 / r) ^ a = 1 / r * (1 / r)^(a-1) := by
        nth_rewrite 2 [← rpow_one (1 / r)]
        rw [← rpow_add]
        simp only [one_div, add_sub_cancel'_right]
        exact hri
      rw [this, smul_eq_mul, smul_eq_mul, mul_assoc]
    _ = (1 / r) ^ a * Real.Gamma (a) := by
      rw [Gamma_eq_integral ha]
      congr
      ext x
      group

open Complex

/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function,
for complex a. -/
lemma pow_exp_integral_Ioi_complex {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t))
    = (1 / r) ^ a * Complex.Gamma (a) := by
  have hri : 0 < 1/r := by positivity
  calc ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t))
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a-1) * (r * t) ^ (a - 1) * Complex.exp (-(r * t)) := by
      apply MeasureTheory.set_integral_congr
      · simp
      · intro x (hx : 0 < x)
        simp_rw [mul_eq_mul_right_iff]
        have := mul_rpow hr.le hx.le
        rw [this]
        simp_rw [← mul_assoc, ← mul_rpow hri.le hr.le,
          mul_comm (1 / r), mul_div, mul_one, div_self hr.ne', one_rpow, one_mul, true_or]
    _ =  |1 / r| * ∫ (t : ℝ) in Ioi (r * 0), (1 / r) ^ (a-1) * t ^ (a - 1) * Complex.exp (-t) := by
      have : ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * (↑r * ↑t) ^ (a - 1) * cexp (-(↑r * ↑t)) =
        ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑(r * t) ^ (a - 1) * cexp (-↑(r * t)) := by simp
      rw [this, integral_comp_mul_left_Ioi (fun x ↦ (1 / r) ^ (a - 1) * x ^ (a - 1) * Complex.exp (-x)) (0 : ℝ) hr]
    _ =  (1 / r) * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a-1) * t ^ (a - 1) * Complex.exp (-t) := by
      have : Ioi (r * 0) = Ioi 0 := by refine Ioi_inj.mpr (by simp)
      rw [this, _root_.abs_of_nonneg hri.le]
      simp
    _ =  1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a-1) * (t ^ (a - 1) * Complex.exp (-t)) := by
      congr
      ext x
      rw [mul_assoc, ← smul_eq_mul]
    _ =  1 / r * (1 / r) ^ (a-1) • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-t)) := by
      rw [integral_smul]
    _ = (1 / r) ^ a • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-t)) := by
      have : (1 / r) ^ a = 1 / r * (1 / r)^(a-1) := by
        nth_rewrite 2 [← rpow_one (1 / r)]
        rw [← rpow_add]
        simp only [one_div, add_sub_cancel'_right]
        exact hri
      rw [this, smul_eq_mul, smul_eq_mul, mul_assoc]
    _ = (1 / r) ^ a * Complex.Gamma (a) := by
      rw [Complex.Gamma_eq_integral ha]
      congr
      ext x
      group

[Josha Dekker]

The second step in the calc proof is very ugly right now, I was hoping to rewrite the necessary coe terms, but it is not very successful so far...

[Josha Dekker]

Some general pointers are much appreciated!

[Josha Dekker]

I can fill in the second part, but it is very ugly and deals with manipulating the coercions directly, I feel like it should be possible in an easier way...

[Josha Dekker]

This is what I have now for the second step, but the 'have' statement feels like it should be replaceable?

_ =  |1 / r| * ∫ (t : ℝ) in Ioi (r * 0), (1 / r) ^ (a-1) * t ^ (a - 1) * Complex.exp (-t) := by
      have : ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * (↑r * ↑t) ^ (a - 1) * cexp (-(↑r * ↑t)) =
        ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑(r * t) ^ (a - 1) * cexp (-↑(r * t)) := by simp
      rw [this, integral_comp_mul_left_Ioi (fun x ↦ (1 / r) ^ (a - 1) * x ^ (a - 1) * Complex.exp (-x)) (0 : ℝ) hr]

[Josha Dekker]

What is mainly the problem is the following line:

    _ =  1 / r * (1 / r) ^ (a-1) • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-t)) := by

Which produces "failed to synthesize instance
HPow ℝ ℂ ?m.293008"

[Josha Dekker]

This problem disappears when I replace the \smul with *, but then I cannot call integral_smul, which I need

[Patrick Massot]

Guessing is too hard for Lean here.

[Patrick Massot]

import Mathlib

variable (x : ℝ) (z w : ℂ)

#check x^z * w --works
#check x^z • w -- fails
#check (x^z : ℂ) • w -- works
#check (x : ℂ)^z • w -- works

[Josha Dekker]

Oops, forgot I could just do that! Thanks!

[Patrick Massot]

The issue is having too many types to guess simultaneously.

[Josha Dekker]

Okay, if you don't mind me asking one more thing: how do I prove the following? r and x are real, so I'd expect nothing funny to happen here:

a: ℂ
r: ℝ
ha: 0 < a.re
hr: 0 < r
hri: 0 < 1 / r
x: ℝ
hx: 0 < x
⊢ ↑x ^ (a - 1) = (1 / ↑r) ^ (a - 1) * (↑r * ↑x) ^ (a - 1)

[Josha Dekker]

Made a MWE in context, the sorry followed by "this fails" is the problem: I used to have mul_rpow there, but that cannot be used anymore.

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

open scoped ENNReal NNReal

open MeasureTheory Real Set Filter Topology
open Measure

open Complex

/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function,
for complex a. -/
lemma pow_exp_integral_Ioi_complex {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t))
    = (1 / r) ^ a * Complex.Gamma (a) := by
  have hri : 0 < 1/r := by positivity
  calc ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t))
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a-1) * (r * t) ^ (a - 1) * Complex.exp (-(r * t)) := by
      apply MeasureTheory.set_integral_congr
      · simp
      · intro x (hx : 0 < x)
        simp_rw [mul_eq_mul_right_iff]
        apply Or.inl
        have := mul_rpow hr.le hx.le -- this fails!
        rw [this]
        simp_rw [← mul_assoc, ← mul_rpow hri.le hr.le,
          mul_comm (1 / r), mul_div, mul_one, div_self hr.ne', one_rpow, one_mul]
    _ =  |1 / r| * ∫ (t : ℝ) in Ioi (r * 0), (1 / r) ^ (a-1) * t ^ (a - 1) * Complex.exp (-t) := by
      sorry
    _ =  (1 / r) * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a-1) * t ^ (a - 1) * Complex.exp (-t) := by
      sorry
    _ =  1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r : ℂ) ^ (a-1) • (t ^ (a - 1) * Complex.exp (-t)) := by
      sorry
    _ =  1 / r * (1 / r : ℂ) ^ (a-1) • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-t)) := by
      sorry
    _ = (1 / r : ℂ) ^ a • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-t)) := by
      sorry
    _ = (1 / r) ^ a * Complex.Gamma (a) := by
      sorry

[Patrick Massot]

You hope that Mario or I will find time to PR the rpow_simp tactic that we wrote at https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/Tactic/RPowSimp.lean

[Josha Dekker]

that would've been very nice, but I guess I should just get my hands dirty and work out the multiplication here from the definition then, for the time being!

[Kevin Buzzard]

rw [← mul_cpow_ofReal_nonneg] is what you need.

I found this by hovering over ^ in the goal, then hovering over instHPow then contol-clicking on instPowComplex(where the definition of ^ is) and then just reading the lemmas in the file until I found the one you needed. I think that an experience loogler could have found it in a more efficient way.

[Josha Dekker]

Kevin Buzzard said:

rw [← mul_cpow_ofReal_nonneg] is what you need.

I found this by hovering over ^ in the goal, then hovering over instHPow then contol-clicking on instPowComplex(where the definition of ^ is) and then just reading the lemmas in the file until I found the one you needed. I think that an experience loogler could have found it in a more efficient way.

Thank you, I tried loogle and moogle but didn’t find a good fit! I’ll experiment with control-clicking to the definitions!

[Kevin Buzzard]

        rw [← mul_cpow_ofReal_nonneg (by positivity) (by positivity)]
        congr
        norm_cast
        field_simp
        ring

I prefer using the more high-powered tactics because I'm too old to learn all this mul_div, div_self, one_rpow stuff.

[David Loeffler]

Kevin Buzzard said:

I prefer using the more high-powered tactics because I'm too old to learn all this mul_div, div_self, one_rpow stuff.

Not sure I would agree with Kevin there. In this sort of stuff (manipulating real / complex exponentials and powers), the automated machinery often gets stuck in blind alleys, since it's not algorithmically obvious which direction is the "simpler" one to rewrite in. So you have to give it a hint occasionally – exactly as Kevin did by performing a "backwards" rewrite rw [← mul_cpow_ofReal_nonneg] – hence it is worth learning how to operate the manual controls!

(That said, it's very possible that the automated machinery is a lot better now than it was in 2021 when I wrote most of the Gamma stuff.)

[Josha Dekker]

I still had to fight a bit with Lean to get all the terms right, but all of your suggestions have helped me a great deal! This result is now added to #9408 for feedback, I'll try and see where it would fit in the files for the Gamma function!

[Josha Dekker]

I think Analysis/SpecialFunctions/Gamma/Basic would be a good place, I've put it at the end of that file for now!

[Josha Dekker]

The conversion to the real case should be easy, but I'm having a hard time getting rid of all the coercions in that case, while everything is supposed to be real, so I'm probably overlooking some basic functionality; I'll take another good look

[Josha Dekker]

I've tried several things, but I cannot really manage to relate the equation for the reals to the one already established for the complexes. The concern is with the second lemma, the first one has been proven.

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

open scoped ENNReal NNReal

open MeasureTheory Real Set Filter Topology
open Measure

open Complex

/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function,
for complex a. -/
lemma integral_cpow_mul_exp_neg_mul_Ioi {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t))
    = (1 / r) ^ a * Complex.Gamma (a) := by sorry

open Real
/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function. -/
lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))
    = (1 / r) ^ a * Real.Gamma (a) := by
  have hac : 0 < (a : ℂ).re := ha
  have := integral_cpow_mul_exp_neg_mul_Ioi hac hr
  sorry

[Josha Dekker]

I end up with the following state, where I want to 'get rid of the coercions', because all quantities involved are real-valued anyway:

ar: ℝ
ha: 0 < a
hr: 0 < r
hac: 0 < (↑a).re
this: ∫ (t : ℝ) in Ioi 0, ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t)) = (1 / ↑r) ^ ↑a * Complex.Gamma ↑a
⊢ ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t)) = (1 / r) ^ a * Real.Gamma a

[Ruben Van de Velde]

Closer:

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

open scoped ENNReal NNReal

open MeasureTheory Real Set Filter Topology
open Measure

open Complex

/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function,
for complex a. -/
lemma integral_cpow_mul_exp_neg_mul_Ioi {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t))
    = (1 / r) ^ a * Complex.Gamma (a) := by sorry

open Real
/-- Expresses the integral over Ioi 0 of t^(a-1) * exp(-r*t) in terms of the Gamma function. -/
lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))
    = (1 / r) ^ a * Real.Gamma (a) := by
  have hac : 0 < (a : ℂ).re := ha
  apply_fun Complex.ofReal' using ofReal_injective
  convert integral_cpow_mul_exp_neg_mul_Ioi hac hr
  · trans ∫ (t : ℝ) in Ioi 0, ((t ^ (a - 1) * rexp (-(r * t)) : ℝ) : ℂ)
    · sorry -- does this need some integrability condition?
    · refine integral_congr_ae ?_
      refine EqOn.eventuallyEq_of_mem ?_ (self_mem_ae_restrict measurableSet_Ioi)
      intro x hx
      simp at hx
      simp only
      norm_cast
      rw [← ofReal_cpow hx.le, ← ofReal_mul]
  · norm_cast
    simp only [Complex.Gamma_ofReal]
    rw [← ofReal_cpow, ← ofReal_mul]
    positivity

[Josha Dekker]

Thanks! I can't imagine that that needs an integrability condition though

[Josha Dekker]

integral_ofReal does the trick

[Josha Dekker]

I think that completes #9408, thank you for all your input!

[Kevin Buzzard]

The impossible instance linter apparently thinks otherwise ;-)

[Josha Dekker]

Yes, I noticed… let me check what went wrong there

[Kevin Buzzard]

The point is that the way typeclass inference works, instIsProbabilityMeasureGamma can never fire, because < is not a class, so the input 0 < a can never be found by the algorithm which typeclass inference runs. If we had a type pReal of positive reals then you could make a and r terms of this type and then the instance would be OK. An easy fix is just to make this a def not an instance.

[Josha Dekker]

Thank you, that explains the error. I guess this is why Probability/Distributions/Exponential uses Fact (0 < r) for instIsProbabilityMeasureExponential, but I was asked to get rid of that. I used the following now:

def instIsProbabilityMeasureGamma {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    IsProbabilityMeasure (gammaMeasure a r) where
  measure_univ := by simp [gammaMeasure, lintegral_gammaPdf_eq_one a r ha hr]

[Ruben Van de Velde]

That's also not going to work as an instance

[Ruben Van de Velde]

You either need Fact for both ha and hr or use def

[Ruben Van de Velde]

def is probably better

[Josha Dekker]

yeah, I wrote the wrong one, I switched it to def
changed the message

[Josha Dekker]

okay, great! does the current def look good?

[Ruben Van de Velde]

I guess you should now remove the inst from the name

[Josha Dekker]

Will do, so should it be a lemma or a def then?

[Ruben Van de Velde]

Without knowing the background, it looks sensible enough now

[Josha Dekker]

Great, I'll PR it and see what the reviewer thinks! Thanks!

[Ruben Van de Velde]

Oh yes, lemma would be better

[Ruben Van de Velde]

(Messages crossed there)

[Josha Dekker]

Changed it, awesome!

Also, if you don't mind me asking: does the failure in https://github.com/leanprover-community/mathlib4/pull/9200 come from a cache issue, or should I check my math?

[Josha Dekker]

(or perhaps I messed up a branch-thing there as well?)

[Ruben Van de Velde]

That's a cache issue, yeah. The following should help:

git checkout JADekker_filter_from_prop
git merge origin/master
git push origin JADekker_filter_from_prop

[Josha Dekker]

okay, now 'lake exe cache get' is no longer working...

[Kevin Buzzard]

This is expected. The orange circle

orange.png

next to a890ae5 means "continuous integration is making your cache right now". It will eventually change into either a green tick (success) or a red cross (failure).

[Josha Dekker]

Oh, I didn't know that! Thank you! Now time to fix the mess I made (again)

[Kevin Buzzard]

Is there a mess? It's now a green tick. Are the changes here what you expect (7 files changed)?

[Josha Dekker]

My local version became a mess, as I was doing some stuff to "fix" that lake exe cache get wasn't working (which was apparently wrong). I've managed to fix that now due to comments in another thread! Thank you very much for clarifying, sorry for the confusion!

[Josha Dekker]

Kevin Buzzard said:

Is there a mess? It's now a green tick. Are the changes here what you expect (7 files changed)?

yes, the Github version is fine!

[Kevin Buzzard]

Then you just wait until it's merged, delete your local branch and just go back to master :-)