Can't calc with expectations

Stream: new members

[Duncan Skahan]

Why does

import Mathlib

noncomputable section

open MeasureTheory ProbabilityTheory

variable {Ω: Type*} [mΩ: MeasurableSpace Ω]
variable {P: Measure Ω}

theorem zero_mean {X : Ω → ℝ} (mX: Measurable X) :
  P[X] = 0 := by
  calc
    P[X] = 0 := by sorry

give
invalid 'calc' step, failed to synthesize `Trans` instance Trans Eq Eq ?m.2997 Additional diagnostic information may be available using the `set_option diagnostics true` command.?

[Ruben Van de Velde]

You should not assume single line calc blocks will work, but (0 : ℝ) might get you closer

[Duncan Skahan]

That does fix it. Do you know why it is needed?

[Duncan Skahan]

Also how can I make this work when both sides of the equation include expectations. For example:

import Mathlib

noncomputable section

open MeasureTheory ProbabilityTheory

variable {Ω: Type*} [mΩ: MeasurableSpace Ω]
variable {P: Measure Ω}

theorem rfl_mean {X : Ω → ℝ} :
  P[X] = P[X] + 0 := by
  calc
    P[X] = P[X] + 0 := by simp

gives the same error.

[Ruben Van de Velde]

Oh, I think there's something off with the P[X] notation, this works:

import Mathlib

noncomputable section

open MeasureTheory ProbabilityTheory

variable {Ω: Type*} [mΩ: MeasurableSpace Ω]
variable {P: Measure Ω}

theorem rfl_mean {X : Ω → ℝ} :
    P[X] = P[X] + 0 := by
  calc
    ∫ (x : Ω), X x ∂P = ∫ (x : Ω), X x ∂P + 0 := by simp

[Duncan Skahan]

Thanks. Is this a bug or just a limitation of how notation can be defined in Lean?

[Yaël Dillies]

Looks like a bug to me. The notation seems to have the wrong precedence EDIT: Nope

[Duncan Skahan]

Though putting P[X] in brackets doesn't fix it.

[Yaël Dillies]

It looks like it's some kind of wrong elaboration order: This fixes it:

import Mathlib

open scoped ProbabilityTheory

variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : MeasureTheory.Measure Ω}

theorem rfl_mean {X : Ω → ℝ} :
  P[X] = P[X] + 0 := by
  calc
    P[X] = P[X] + (0 : ℝ) := by simp

[Yaël Dillies]

The 0 is being interpreted as a Nat and is pushing for X to be Nat-valued. Instead we would expect that X being Real-valued should push the 0 to be interpreted as a Real.

[Ruben Van de Velde]

Btw, putting exact before calc gives other error messages