Integrable function??

Stream: general

[MohanadAhmed]

In the code below, lean is not satisfied with the lemma provided and replies with the nice looking but useless message (shown below the code). Using the option set_option pp.all true produces the scarier but probably more informative message beneath it. So I have two questions:

1. I understand the goals are somehow not identical? How do I fix this
2. Is it possible that to change the error messages to shows the second scarier message when the original ones look identical because unable to match a to a is just plain confusing

Code with error in last Line

import Mathlib

open MeasureTheory

-- set_option pp.notation false
example : Integrable (fun x => Real.exp (-2 * x ^ 2)) := by
  simp only [Real.rpow_two]
  refine integrable_exp_neg_mul_sq (zero_lt_two' ℝ)

noncomputable def gaussianMeasure2 : Measure ℝ := by
  let g := fun (u : Set ℝ) (hu : MeasurableSet u) =>
    ENNReal.ofReal (∫ (x : ℝ) in u, Real.exp (-2*x^2))
  apply MeasureTheory.Measure.ofMeasurable g
  sorry
  intros s hs hs_disjoint
  dsimp
  rw [MeasureTheory.integral_iUnion hs, ENNReal.ofReal_tsum_of_nonneg]
  intro n;  apply (integral_nonneg (le_of_strongLT _))
  sorry; sorry; sorry
  rw [IntegrableOn]
  simp only [Real.rpow_two]
  refine integrable_exp_neg_mul_sq ?_

The nice error message. (But confusing!!)

type mismatch
  integrable_exp_neg_mul_sq ?m.2235
has type
  Integrable fun x => rexp (-2 * x ^ 2) : Prop
but is expected to have type
  Integrable fun x => rexp (-2 * x ^ 2) : Prop

Using set_option.pp all true gives the scarier (but perhaps more informative)

type mismatch
  @integrable_exp_neg_mul_sq ?m.2234 ?m.2235
has type
  @MeasureTheory.Integrable.{0, 0} Real Real.normedAddCommGroup Real
    (@MeasureTheory.MeasureSpace.toMeasurableSpace.{0} Real Real.measureSpace)
    (fun (x : Real) =>
      Real.exp
        (@HMul.hMul.{0, 0, 0} Real Real Real (@instHMul.{0} Real Real.instMulReal)
          (@Neg.neg.{0} Real Real.instNegReal ?m.2234)
          (@HPow.hPow.{0, 0, 0} Real Nat Real (@instHPow.{0, 0} Real Nat (@Monoid.Pow.{0} Real Real.instMonoidReal)) x
            (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))))
    (@MeasureTheory.MeasureSpace.volume.{0} Real Real.measureSpace) : Prop
but is expected to have type
  @MeasureTheory.Integrable.{0, 0} Real Real.normedAddCommGroup Real Real.measurableSpace
    (fun (x : Real) =>
      Real.exp
        (@HMul.hMul.{0, 0, 0} Real Real Real (@instHMul.{0} Real Real.instMulReal)
          (@Neg.neg.{0} Real Real.instNegReal
            (@OfNat.ofNat.{0} Real 2
              (@instOfNat.{0} Real 2 Real.natCast
                (@instAtLeastTwoHAddNatInstHAddInstAddNatOfNat (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))))))
          (@HPow.hPow.{0, 0, 0} Real Nat Real (@instHPow.{0, 0} Real Nat (@Monoid.Pow.{0} Real Real.instMonoidReal)) x
            (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))))
    (@MeasureTheory.Measure.restrict.{0} Real Real.measurableSpace
      (@MeasureTheory.MeasureSpace.volume.{0} Real Real.measureSpace)
      (@Set.iUnion.{0, 1} Real Nat fun (i : Nat) => s i)) : Prop

[Sebastien Gouezel]

I'm not answering your question, but if you're seeking to define the Gaussian measure you should definitely have a look at docs#MeasureTheory.Measure.withDensity, which will build the measure for you without having to mess with too much measure theory.

[Ruben Van de Velde]

I think this is the HPow issue again, where the exponent 2 is a Real when it probably should be a Nat

[Ruben Van de Velde]

Try putting the following incantation after your imports:

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220

[Alexander Bentkamp]

No, I think it's the last argument that's not defeq:

(@MeasureTheory.MeasureSpace.volume.{0} Real Real.measureSpace)

vs

(@MeasureTheory.Measure.restrict.{0} Real Real.measurableSpace
      (@MeasureTheory.MeasureSpace.volume.{0} Real Real.measureSpace)
      (@Set.iUnion.{0, 1} Real Nat fun (i : Nat) => s i))

[Alexander Bentkamp]

I don't even think that you can prove that these are equal in your context.

[Floris van Doorn]

One big issue here is that the last argument of Integrable is treated as an implicit argument in the pretty printer. I don't think that should be the case for auto-param arguments. Note that the type of Integrable is

def Integrable {α} {_ : MeasurableSpace α} (f : α → β) (μ : Measure α := by volume_tac)

[Yury G. Kudryashov]

Who can implement an option that makes the pretty printer treat auto-params as normal arguments?

[Floris van Doorn]

@MohanadAhmed: if you just want to continue with your proof, then replace the rw [IntegrableOn] by refine Integrable.integrableOn ?_ (but @Sebastien Gouezel's suggestion to use withDensity is of course better).