Declaring an Instance?

Stream: new members

[Dominic Steinitz]

I declare an instance of a class and then use #synth to check which says it is not an instance of the class. I am scratching my head on this one.

import Mathlib

open MeasureTheory ProbabilityTheory NNReal Real Filter Finset

variable
(m : ℝ)
(v : ℝ≥0)
(hv : v ≠ 0)

noncomputable
def f := (λ x => ENNReal.ofReal (gaussianPDFReal m v x))

noncomputable
def ν : Measure ℝ := volume.withDensity (f m v)

open MeasureTheory

instance : IsProbabilityMeasure (ν m v) := by
  have h1 : (volume.withDensity (f m v)) = ν m v := rfl
  have h2 : (volume.withDensity (f m v)) Set.univ = ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume := by
    rw [MeasureTheory.withDensity_apply _ MeasurableSet.univ]
    rw [MeasureTheory.Measure.restrict_univ]
    congr
  have h7 : ν m v Set.univ =  ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume := by
    rw [<-h1]
    exact h2

  have h7z : 0 ≤ᶠ[ae ℙ] gaussianPDFReal m v := by
    apply Eventually.of_forall
    exact gaussianPDFReal_nonneg m v

  have h8 : ENNReal.ofReal (∫ (a : ℝ), gaussianPDFReal m v a ∂volume) =
            ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume := by
    apply MeasureTheory.ofReal_integral_eq_lintegral_ofReal (ProbabilityTheory.integrable_gaussianPDFReal m v) h7z

  have h9 : ∫ (a : ℝ), gaussianPDFReal m v a ∂volume = 1 := integral_gaussianPDFReal_eq_one m hv

  have h10 : ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume = 1 := by
    rw [← h8]
    rw [h9]
    rw [ENNReal.ofReal_one]

  apply IsProbabilityMeasure.mk
  show (ν m v) Set.univ = 1
  rw [h7]
  exact h10

#synth IsProbabilityMeasure (ν m v)

[Kevin Buzzard]

Put #lint after your code and you'll see

/- The `impossibleInstance` linter reports:
SOME INSTANCES HAVE ARGUMENTS THAT ARE IMPOSSIBLE TO INFER
These are arguments that are not instance-implicit and do not appear in
another instance-implicit argument or the return type. -/
#check instIsProbabilityMeasureRealν /- argument 3 hv : v ≠ 0 -/

Because ≠ is not a class, and hv does not appear in the type of the term, typeclass inference won't be able to find it.

[Dominic Steinitz]

That makes sense thanks very much - what is less clear is why we have this condition at all - it comes from this in Mathlib

ProbabilityTheory.integral_gaussianPDFReal_eq_one (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) : ∫ (x : ℝ), gaussianPDFReal μ v x = 1

But I would interpret a Gaussian with zero variance as having all the mass concentrated at 0 and which would still integrate to 1.

Can I make my h9 into a sort of case statement (I am not sure what these things are called in Lean)?

[Edward van de Meent]

Dominic Steinitz said:

But I would interpret a Gaussian with zero variance as having all the mass concentrated at 0 and which would still integrate to 1.

i'm guessing the issue with that is the fact that that function cannot be expressed as a function Real -> Real

[Edward van de Meent]

currently, gaussianPDFReal is defined as constantly 0 for v=0, so the statement is not true for such values. i seem to recall that there are some formalisms where you can make such a formalism (like the dirac delta) make sense, but right now that's not in mathlib, afaik

[Dominic Steinitz]

I will look more closely - I was probably thinking distributions rather than functions

[Dominic Steinitz]

But I am down a few rabbit holes at the moment - is there a way to convince Lean that my measure is a probability measure?

[Edward van de Meent]

you have convinced lean; the issue is that there is no way for instance search to find this. i think i'd personally give the instance a name and try and specify each time?

[Dominic Steinitz]

I didn't know instances could be given names - I will go look at the docs - thanks very much

[Edward van de Meent]

same with any declaration. you can just do instance foo (x:bla) : Class x := sorry

[Edward van de Meent]

alternatively, you can use the Fact pattern, although i'm not sure if this is a good place to use it, someone else might be able to make that judgement

[Rémy Degenne]

Are you trying to define a Gaussian measure on the real line? Why not simply use ProbabilityTheory.gaussianReal ?

[Dominic Steinitz]

I am trying to refactor some code where someone has written their own version of the Gaussian CDF

def gaussian_cdf (μ : ℝ) (v : ℝ≥0) (x : ℝ) :=
  ∫ t in (Iic x), gaussianPDFReal μ v t ∂volume

with the version provided by Mathlib

def f := (λ x => ENNReal.ofReal (gaussianPDFReal m v x))

def ν : Measure ℝ := volume.withDensity (f m v)

def my_gaussian_cdf (μ : ℝ) (v : ℝ≥0) (x : ℝ) : ℝ :=
  cdf (ν μ v) x

So I am trying to prove

lemma gaussian_cdf_eq_my_gaussian_cdf (μ : ℝ) (v : ℝ≥0) (x : ℝ) :
  gaussian_cdf μ v x = my_gaussian_cdf μ v x := by

At some point Lean told me that (ν μ v) was not a probability measure so I thought I had better prove it was.

[Kyle Miller]

(In case it's helpful in the future, sometimes I hover over instance to see the actual inferred type of an instance. That saves needing to name the instance for a later #check, or for being able to hover over the name to get the hover. Looking at the type of an instance is my first step when it doesn't seem to apply.)

[Kyle Miller]

By the way, it's possible to do case-based reasoning inside the instance, but as Edward pointed out, the v = 0 case reduces to the goal ⊢ IsProbabilityMeasure 0.

import Mathlib

open MeasureTheory ProbabilityTheory NNReal Real Filter Finset

variable
(m : ℝ)
(v : ℝ≥0)
--(hv : v ≠ 0)

noncomputable
def f := (λ x => ENNReal.ofReal (gaussianPDFReal m v x))

noncomputable
def ν : Measure ℝ := volume.withDensity (f m v)

open MeasureTheory

instance : IsProbabilityMeasure (ν m v) := by
  by_cases hv : v = 0
  · subst v
    unfold ν f
    simp
    -- ⊢ IsProbabilityMeasure 0
    sorry
  have h1 : (volume.withDensity (f m v)) = ν m v := rfl
  have h2 : (volume.withDensity (f m v)) Set.univ = ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume := by
    rw [MeasureTheory.withDensity_apply _ MeasurableSet.univ]
    rw [MeasureTheory.Measure.restrict_univ]
    congr
  have h7 : ν m v Set.univ =  ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume := by
    rw [<-h1]
    exact h2

  have h7z : 0 ≤ᶠ[ae ℙ] gaussianPDFReal m v := by
    apply Eventually.of_forall
    exact gaussianPDFReal_nonneg m v

  have h8 : ENNReal.ofReal (∫ (a : ℝ), gaussianPDFReal m v a ∂volume) =
            ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume := by
    apply MeasureTheory.ofReal_integral_eq_lintegral_ofReal (ProbabilityTheory.integrable_gaussianPDFReal m v) h7z

  have h9 : ∫ (a : ℝ), gaussianPDFReal m v a ∂volume = 1 := integral_gaussianPDFReal_eq_one m hv

  have h10 : ∫⁻ (a : ℝ), ENNReal.ofReal (gaussianPDFReal m v a) ∂volume = 1 := by
    rw [← h8]
    rw [h9]
    rw [ENNReal.ofReal_one]

  apply IsProbabilityMeasure.mk
  show (ν m v) Set.univ = 1
  rw [h7]
  exact h10

[Edward van de Meent]

Edward van de Meent said:

[...] there are some formalisms where you can make such a formalism (like the dirac delta) make sense, but right now that's not in mathlib, afaik

I could very well be wrong about this, so do check yourself

[Daniel Weber]

Just a note that there is docs#NeZero which is a typeclass

[Kevin Buzzard]

Aah this is probably the simplest approach then.