Invalid field notation

Stream: new members

[Lucas Viana]

Here Lean complains invalid field notation, function 'measure_theory.measure_space.μ' does not have explicit argument with type (measure_theory.measure_space ...)

import measure_theory.measure_space

open measure_theory set

variables {α : Type*} [measure_space α]

structure dynamic (α : Type*) extends measure_space α :=
(f : α → α)

def dynamic.invariant (d : dynamic α) (b : set α)  := image d.f b = b

def ergodic (d : dynamic α) :=
   ∀ (b) (b_measurable : is_measurable b) (b_invariant : d.invariant b),
   d.μ b = 0 ∨ d.μ b = 1

I think I don't understand how extending a class works. How would I use the measure of the dynamic inherited from the measure_space?

[Lucas Viana]

(deleted)

[Sam Lichtenstein]

I think so. The measure_space class that you extended includes a choice of measure on the measurable space α, and volume refers to this choice of measure (at least in the version of mathlib that I am looking at at the moment).

[Sam Lichtenstein]

I think if you want to work explicitly with the μ component of the measure space class, you can also do:

variables {α : Type*} [measure_space α]
variables (b : set α)[is_measurable b]
#check @measure_space.μ α _ b  -- the underscore corresponds to the choice of [measure_space α] instance, which Lean infers from context
``

[Sam Lichtenstein]

Or just measure_space.μ b. Since b is a subset of α, Lean will look for the measure space instance on α that you declared and use that

[Magalame]

I'm having trouble with accessing fields within extended records, the following code ( _inst_1 has type inner_product_space ℂ H)

import analysis.inner_product_space.basic

variables {H : Type} [inner_product_space ℂ H] [complete_space H] [finite_dimensional ℂ H]
variables {x : H}

def norm2 (x : H) : ℝ := _inst_1.to_normed_group.to_has_norm.norm x

outputs

invalid field notation, function 'has_norm.norm' does not have explicit argument with type (has_norm ...)

while if I erase the x after .norm Lean only complains that an argument is missing

type mismatch, term
  norm
has type
  H → ℝ
but is expected to have type
  ℝ

[Eric Wieser]

Is there a reason you're not just writing norm?

[Magalame]

oh thank you it works! I had no idea it'd be straightforward. Is there any reason why what I tried does not though?

[Eric Wieser]

I think there are some weird rules about how dot notation works on typeclasses that don't quite follow the usual pattern.

[Kyle Miller]

I think the main rule is that when resolving dot notation, first the elaborator tries to resolve it as a projection (navigating the whole extends hierarchy) and then it falls back to extended dot notation. For projections, Lean will always use the first argument after all the type parameters, but for dot notation it will use the first explicit argument with the right type. The function 'has_norm.norm' does not have explicit argument with type (has_norm ...) means it's trying for extended dot notation.

[Kyle Miller]

There's also a bug in dot notation that seems to be affecting this.

noncomputable
def norm2 (x : H) : ℝ :=
let f := _inst_1.to_normed_group.to_has_norm.norm
in f x

[Kyle Miller]

It has to do with a difference between how dot notation is elaborated in the presence of arguments vs no arguments. I have a patch for it I've been meaning to polish and PR... (though I don't know if it fixes this particular error.)

[Junyan Xu]

Some code with explanation along the lines above: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Pi.20type.2Finvalid.20field.20notation/near/179611847