tactic 'apply' failed, failed to unify probability example

Stream: new members

[Michael Kane]

In the following code, I want to provide a simple extension to monotone property of a probability measure. However, I'm getting a "failed to unify" error. Is there another tactic that would be more efficient? Is it clear to someone who is more literate in lean 4 what the issue is? Thanks.

import Mathlib

open MeasureTheory
open NNReal

variable {Ω : Type u1} [MeasurableSpace Ω]
variable {μ : ProbabilityMeasure Ω}
variable {s₁ s₂ : Set Ω}
variable {a : NNReal}

#check (μ s₁)
#check a

example (h0: a ≤ 1) (h1 : s₁ ⊆ s₂) : a * μ s₁ ≤ μ s₂ := by
  have h3 : μ s₁ ≤ μ s₂ := by
    apply μ.apply_mono h1
  have h4 : a * μ s₁ ≤ 1 * μ s₁ := by
    apply mul_le_mul_of_le_of_le h0 h3
  sorry
/-
tactic 'apply' failed, failed to unify
  (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁ * a ≤ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₂ * 1
with
  a * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ 1 * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁
-/

[Rémy Degenne]

Can you please read #backticks are format your post in a more readable way?

[Rémy Degenne]

Thanks!

[Ruben Van de Velde]

The error seems to explain how they don't match? Your multiplications seem to be flipped

[Rémy Degenne]

I opened that code in the editor and no, it's not flipped there. The error is

tactic 'apply' failed, failed to unify
  a * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ 1 * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₂
with
  a * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ 1 * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁

[Kevin Buzzard]

The relevant part of the error in the code is not what your comment says, it's

tactic 'apply' failed, failed to unify
  a * (fun s ↦ ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ 1 * (fun s ↦ ENNReal.toNNReal (↑↑↑μ s)) s₂
with
  a * (fun s ↦ ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ 1 * (fun s ↦ ENNReal.toNNReal (↑↑↑μ s)) s₁

and you can see the difference right there at the end, an s2 not an s1.

[Rémy Degenne]

Oh I see it: the first line has a s2 on the right

[Rémy Degenne]

A general remark on working with probability measures: you probably want to use {μ : Measure Ω} [IsProbabilityMeasure Ω] and not {μ : ProbabilityMeasure Ω}. ProbabilityMeasure is there for when you want to work on the space of probability measures, with a topology, etc. If you just want one probability measure, the first method works best.

[Michael Kane]

OK. Undestood. However, I'm still having trouble understanding what the tactics expect to be able to fulfull the goals. If I try to apply mul_le_mul_of_le_of_le to h0 and (\mu s\1) then I get

/-
application type mismatch
  mul_le_mul_of_le_of_le h0 ((fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁)
argument
  (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁
has type
  ℝ≥0 : Type
but is expected to have type
  ?m.738 ≤ ?m.739 : Prop
-/

Does the tactic need a hypothesis as an argument? If the answer is RTFM, could you please point me to which manual?

[Rémy Degenne]

The manual is docs#mul_le_mul_of_le_of_le . The explicit arguments of the lemma are inequalities. The error tells you that the second explicit argument should be an inequality, but what you provided is a number.

[Michael Kane]

OK. This is plenty for me to proceed. Thanks very much for your patience. This is very helpful.

[Rémy Degenne]

In VSCode, you can also put your mouse over a lemma name to make a tooltip appear, where you can see the arguments. you can also ctrl+click to jump to the statement of the lemma.

[Michael Kane]

Rémy Degenne said:

A general remark on working with probability measures: you probably want to use {μ : Measure Ω} [IsProbabilityMeasure Ω] and not {μ : ProbabilityMeasure Ω}. ProbabilityMeasure is there for when you want to work on the space of probability measures, with a topology, etc. If you just want one probability measure, the first method works best.

If I do this:

variable {Ω : Type u1} [MeasurableSpace Ω]
variable {μ : Measure Ω} [IsProbabilityMeasure Ω]

then I get the following message. Have I declared the type of \Omega incorrectly? The solutions doesn't seem to be setting it to a more specific type, the reals for example.

/-
application type mismatch
  IsProbabilityMeasure Ω
argument
  Ω
has type
  Type u1 : Type (u1 + 1)
but is expected to have type
  Measure ?m.84133 : Type ?u.84132
-/

[Ruben Van de Velde]

Should be IsProbabilityMeasure μ

[Sebastien Gouezel]

You want [IsProbabilityMeasure μ].

[Rémy Degenne]

Sorry for the typo!

[Rémy Degenne]

By the way: the error message tells you that it expected a measure where I wrote Omega.

[Michael Kane]

OK, when I make the change I get the following error. Is it correct that I need to cast to a ProbabilityMeasure? I searched for "toProbabilityMeasure" in the docs but I'm coming up empty.

invalid field 'apply_mono', the environment does not contain 'MeasureTheory.Measure.apply_mono'

[Michael Kane]

Nevermind. I found measure_mono.

[Ruben Van de Velde]

Yeah, that just means "wrong name"

[Michael Kane]

OK, now I'm running into the following error. The variable is of type NNReal. What does the up arrow mean? The complete code snippet is below the error.

/-
application type mismatch
  mul_le_of_le_one_left h3 h0
argument
  h0
has type
  a ≤ 1 : Prop
but is expected to have type
  ↑a ≤ 1 : Prop
-/

import Mathlib

open MeasureTheory
open ProbabilityMeasure
open NNReal

variable {Ω : Type u1} [MeasurableSpace Ω]
variable {μ : Measure Ω} [IsProbabilityMeasure μ]
variable {s₁ s₂ : Set Ω}
variable (a : NNReal)

#check (μ s₁)
#check a

example (h0: a ≤ 1) (h1 : s₁ ⊆ s₂) : a * μ s₁ ≤ μ s₂ := by
  have h2 : μ s₁ ≤ μ s₂ := by
    exact measure_mono h1
  have h3 : 0 ≤ μ s₁ := by
    exact zero_le (μ s₁)
  have h4 : a * μ s₁ ≤ μ s₁ := by
    exact mul_le_of_le_one_left h3 h0
  sorry

[Ruben Van de Velde]

That's a coercion

[Ruben Van de Velde]

mul_le_of_le_one_left needs an inequality of ENNReals here, but h0 is about NNReals

[Rémy Degenne]

You can solve many of those coercion issues with norm_cast or exact_mod_cast:

import Mathlib

open MeasureTheory
open ProbabilityMeasure
open NNReal

variable {Ω : Type u1} [MeasurableSpace Ω]
variable {μ : Measure Ω} [IsProbabilityMeasure μ]
variable {s₁ s₂ : Set Ω}
variable (a : NNReal)

#check (μ s₁)
#check a

example (h0: a ≤ 1) (h1 : s₁ ⊆ s₂) : a * μ s₁ ≤ μ s₂ := by
  have h2 : μ s₁ ≤ μ s₂ := by
    exact measure_mono h1
  have h3 : 0 ≤ μ s₁ := by
    exact zero_le (μ s₁)
  have h4 : a * μ s₁ ≤ μ s₁ := by
    refine mul_le_of_le_one_left h3 ?_
    exact_mod_cast h0 -- or `norm_cast`
  sorry

[Rémy Degenne]

But if you can avoid coercions, do it. You could have a : ENNReal, since values of measures are in ENNReal.

[Michael Kane]

OK, now how do I finish the example? I have h4 and h2 implies the result. Is there a tactic or function for that?

[Kevin Buzzard]

linarith?

[Rémy Degenne]

You want to apply transitivity of ≤: you can write exact le_trans h4 h2, or exact h4.trans h2.

[Rémy Degenne]

linarith does not like ENNReal and fails here

[Rémy Degenne]

I feel like it's a good opportunity to introduce calc proofs:

example (h0: a ≤ 1) (h1 : s₁ ⊆ s₂) : a * μ s₁ ≤ μ s₂ := by
  calc a * μ s₁ ≤ μ s₁ := mul_le_of_le_one_left (zero_le (μ s₁)) h0
  _ ≤ μ s₂ := measure_mono h1

[Rémy Degenne]

docs#calc

[Michael Kane]

What does the underscore denote here?

[Rémy Degenne]

According to the doc at docs#calc, "Instead of repeating the right-hand sides, subsequent left-hand sides can be replaced with _."
That underscore is just shorthand for the right-hand side of the previous step.

[Michael Kane]

Nevermind, I see it's the placeholder for the left side of the inequality. Thanks again.