Passing typeclass instances

Stream: new members

[Antonetta Bado]

import Mathlib

noncomputable section

open MeasureTheory

def f {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] := 0

example
  {Ω : Type*} [MeasurableSpace Ω]
  {P : Measure Ω} [IsProbabilityMeasure P] {X : Ω → ℕ} {X_meas : Measurable X}
  -- need to pass the typeclass instance isProbabilityMeasure_map X_meas.aemeasurable
  : f (P.map X) = 0 := sorry

I get the error failed to synthesize IsProbabilityMeasure (Measure.map X P). Is there a way to manually pass the typeclass instance isProbabilityMeasure_map X_meas.aemeasurable?

[Vlad]

https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean/#named-arguments

[Antonetta Bado]

But the parameter has no name. It is just declared as [IsProbabilityMeasure P].

[Vlad]

def f ⋯ [inst : IsProbabilityMeasure P] := 0

example ⋯ : f (P.map X) (inst := ⋯) = 0 := ⋯

[Antonetta Bado]

I don't like the idea of changing the definition just so I can pass a typeclass instance. Is there another way to do this?

[Kyle Miller]

Using haveI in theorem statements is a way to locally add a definition and have it inline itself immediately. It works for instances too, like this:

import Mathlib

noncomputable section

open MeasureTheory

def f {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] := 0

example
  {Ω : Type*} [MeasurableSpace Ω]
  {P : Measure Ω} [IsProbabilityMeasure P] {X : Ω → ℕ} {X_meas : Measurable X} :
  haveI := isProbabilityMeasure_map (X_meas.aemeasurable (μ := P))
  f (P.map X) = 0 := sorry