Comparing indicator with real

Stream: new members

[Michael Kane]

I would like to show a deterministic version of the Markov inequality. If x and a in the reals with a greater than zero, then the indicator for x ≥ a is less than x / a. My attempt is below

import Mathlib
open Set

variable (a x: ℝ)

example (h0 : a ≥ 0) : {a | x ≥ a} ≤ x / a := by
  sorry

and I'm getting the error message:

type mismatch
  x / a
has type
  ℝ : outParam Type
but is expected to have type
  Set ℝ : Type

I think the problem is that left side of the inequality is being seen as a set, rather than either the value zero or one. However, I'm not sure how to proceed. Would someone please provide a hint?

[Kevin Buzzard]

in Lean if you write a <= b then for this to make sense a and b have to have the same "Type", i.e. they have to "be the same kind of thing". In your example you seem to be claiming that a set of reals is <= a real number, and these have different types, so Lean is complaining that one it read last (the real number) doesn't have the type it expected.

So what actually do you mean by the question? I don't know this area at all but I do understand why Lean doesn't understand what you're writing,

[Michael Kane]

OK, I want a and x to be numbers in the set of real, not the entire set. I'm expecting that if x \ge a then the set indicator will return 1, which will be less than or equal to x / a.

If I revise to:

import Mathlib
open Set

example (h0 : a ≥ 0) (h1 : a ∈ ℝ) (h2 : x ∈ ℝ) : { x ≥ a} : ≤ x / a := by
  sorry

then I end up with the syntax error:

unexpected token ':'; expected ':=', 'where' or '|'

I'm still missing something.

[Richard Copley]

Like the message says, the immediate problem is the unexpected colon.

example (h0 : a ≥ 0) (h1 : a ∈ ℝ) (h2 : x ∈ ℝ) : { x ≥ a} : ≤ x / a := by
--                                                   here ^

Beyond that, I don't think the "set indicator" notation you're alluding to exists. I could be wrong.
Also, ℝ is not a set and does not have members (∈). It is a type, and you use the colon (:) to introduce variables of that type and to ascribe the type to values.
Finally, I don't think the thing you want to prove is true in Lean, without a slightly stronger hypothesis.

import Mathlib
import Mathlib.Tactic
open Set

set_option pp.coercions false in
example : ¬ (∀ (a x : ℝ) (h0 : a ≥ 0), (if a ≤ x then 1 else 0) ≤ x / a) := by
  intro h
  specialize h 0 1 (Eq.ge rfl)
  simp? at h says simp only [zero_le_one, ite_true, div_zero] at h
  exact not_le.mpr Real.zero_lt_one h

[Michael Kane]

This is super helpful. Can you tell me how to read the second colon in the example? Before I was reading everything after the colon as the statement of the proposition. This tells me I need to revise.

Thanks for the clarification on ℝ.

Can you tell me what the set_option line does?

Also, can you help me parse the example? I don't understand what is being negated with ¬ .

Thanks very much.

[Michael Kane]

One more thing, is there a way to denote the set of reals less than a constant a? The indicator functions in the Set module do not behave as I would expect them to.

[Kevin Buzzard]

I think you might find it even more super helpful to read the first few sections of #mil so you understand the basics of how to write mathematics in lean. That will answer your question above and probably many others that you'll have

[Kevin Buzzard]

The set is { x | x < a }.

[Eric Wieser]

If you want the "set indicator", that's docs#Set.indicator

[Richard Copley]

Michael Kane said:

This is super helpful. Can you tell me how to read the second colon in the example? Before I was reading everything after the colon as the statement of the proposition. This tells me I need to revise.

The second colon being the one in "(a x : ℝ)"? You read it as "is of type" or "has type". It says that the type of each of the variables a and x is ℝ.

Thanks for the clarification on ℝ.

Can you tell me what the set_option line does?

I'm sorry, I should have deleted that. It influences the pretty-printing in the infoview window. It isn't something I intended to introduce to you now.

Also, can you help me parse the example? I don't understand what is being negated with ¬ .

The thing being negated is the thing inside the (matching) parentheses after the not sign, that is, ∀ (a x : ℝ) (h0 : a ≥ 0), (if a ≤ x then 1 else 0) ≤ x / a which says, roughly, "for all $a$ and $x$ of type $ℝ$, for all h0 of type a ≥ 0 (namely for all proofs "h0" of the proposition $a ≥ 0$), the value of the expression (if a ≤ x then 1 else 0) is less than or equal to $x/a$".
I should not have written it that way. It is confusing. A better rendition, using the "→" to denote implication, would have been: ∀ (a x : ℝ), a ≥ 0 → (if a ≤ x then 1 else 0) ≤ x / a. The reason that these are in fact the same is fundamental to the way Lean works, but I daresay it's not the most important thing to understand in the beginning.

Thanks very much.

You're welcome. Good luck and have fun! I agree with @Kevin Buzzard that it is a good idea to use introductory material from a book such as #mil to get started.

[Michael Kane]

Thanks very much Richard. I will take a closer look.

@Eric Wieser I did try the indicator but I don't understand how it is parameterized. I want to be able to say:

import Mathlib.Tactic
open MeasureTheory
open Set

variable (a x: ℝ)

example (h0 : a ≥ 0) : indicator {x | x ≥ a} ≤ x / a := by
  sorry

but this gives the error

typeclass instance problem is stuck, it is often due to metavariables
  LE ((ℝ → ?m.62) → ℝ → ?m.62)

From the documentation, the indicator function takes 3 parameters, a set a function, and an argument to the function. The set specification of a set that I have provided is not correct but I don't know what the indicator function is expecting.

[Eric Wieser]

Like you said: the documentation says it takes 3 arguments. You passed one so got a completely nonsensical error message!

[Eric Wieser]

If you have a function foo that takes three arguments, but you only know the first one, write foo x _ _ not foo x; lean will give you a much more helpful error

[Michael Kane]

Unfortunately, it only gives a different error:

failed to synthesize instance
  Zero (Sort ?u.1691)

[Eric Wieser]

Can you show what you wrote and the full error?

[Michael Kane]

Certainly. Note the error occurs in the example.

import Mathlib
open Set

variable (a x: ℝ)

#check indicator _ _ _

example (h0 : a ≥ 0) : indicator {x | x ≥ a} _ _ :=
  sorry

I did try

variable {b : Set ℝ}
#check indicator b (· ≥ a) _

thinking maybe the set it wants is the domain and the function is the boolean. It gives the error:

failed to synthesize instance
  Zero Prop

Based on the documentation, I'm not sure what a Zero Prop is.

[Eric Wieser]

Your first example fails because you forgot the RHS of the inequality that you previously had

[Eric Wieser]

It's like trying to prove example : 37 := sorry; 37 is not a type so it doesn't make any sense to put it (by itself) after a colon

[Matt Diamond]

I'm expecting that if x \ge a then the set indicator will return 1, which will be less than or equal to x / a.

Apologies if I'm misunderstanding, but are you just trying to prove something like this?

import Mathlib

example (a x : ℝ) (h0 : a ≥ 0) (h1 : x ≥ a) : 1 ≤ x / a := by
  sorry

because if that's the case, there's no reason to involve sets here.

[Michael Kane]

Sorry, that was my mistake. Now the message is:

don't know how to synthesize placeholder for argument 'x'
context:

ax: ℝ
h0: a ≥ 0
⊢ ℝ

when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

My guess is that first argument is the domain. When I try the following:

import Mathlib
open Set

variable (a x: ℝ)
variable (R : Set ℝ)

example (h0 : a ≥ 0) : (indicator R (· ≥ a) x) ≤ x /  a := by
  sorry

I get

failed to synthesize instance
  Zero Prop

again.

[Michael Kane]

@Matt Diamond That is right. The reason I want to do this with the indicator functions is that eventually want x to be a measurable set I use with probability measures.

[Michael Kane]

Indicators essentially make it easier to prove probability inequalities over the reals.

[Matt Diamond]

Someone else should step in here because I'm not familiar with this domain, but I'm going to guess you're trying to do this:

import Mathlib
open Set

variable (a x: ℝ)

example (h0 : a > 0) : indicator {k | k ≥ a} 1 x ≤ x / a := by
  sorry

[Matt Diamond]

The second argument to indicator is the function that determines the result when x is in the set { k | k ≥ a } (i.e. when x ≥ a). It sounded like you wanted the indicator to return 1 when the value is in the set, and I think you can get away with just passing in 1 as the "function", as I believe Lean will coerce that to a constant function that returns 1.

[Michael Kane]

OK. This makes sense. One question about your code, you used k as the set indicator parameter. If I call it x, do you know if it is explicitly bound to the x variable defined above or should it be thought of as a "dummy" variable, that is parameterized by the third parameter of the indicator function?

[Matt Diamond]

If I understand you correctly, k should be understood as a dummy variable, in the sense that it doesn't reference anything outside of the set definition. If you changed it to x, it wouldn't be bound to the other x value.

[Michael Kane]

Got it. Thanks very much.

[Matt Diamond]

No problem!

[Matt Diamond]

@Michael Kane BTW, @Richard Copley had a good point... you should probably strengthen your hypothesis from a ≥ 0 to a > 0 or else you'll end up trying to prove something that isn't actually true (which can lead to some frustration).

[Michael Kane]

Good point. Thanks again. I'll try to finish this up tomorrow, post, and mark as resolved.

Once again, this has been extremely helpful.

[Ruben Van de Velde]

(Please don't mark zulip threads as resolved)

[Matt Diamond]

@Ruben Van de Velde I thought thread resolution was common here... is this behavior discouraged? It seems like a good way to mark which threads no longer need attention.

[Jireh Loreaux]

@Matt Diamond it happens, but we discourage it because it breaks links to the thread, which is annoying. We would turn the feature off, but that's unfortunately not an option we can toggle.

[Kyle Miller]

My experience is that when people mark threads as being resolved, it makes them re-appear on the "recent conversations" list, leading to more attention rather than less.

Usually it's clear when someone's question has been answered in a thread, and if there's been discussion but no resolution, someone can keep the discussion going with a followup question -- which is good because it helps everyone who might want to help know the current context. I myself don't take whether a thread is "resolved" into account to determine whether it's resolved.

Sometimes people mark a thread as resolved if they answer their own question, but it's better if they explain what they figured out rather that end the thread with the low-information-content "resolved".

[Kyle Miller]

The "resolved" feature appeared one day, and there is no way to disable it.

[Matt Diamond]

Got it, good to know!

[Kyle Miller]

No problem! (And of course these are my own opinions. I only speak for the community as far as no one responds with a counter-argument for why they actually like "resolved" :smile:)

[Kyle Miller]

(@Jireh Loreaux I thought I might have heard that Zulip fixed the breaking links problem, but I haven't looked into it. If you've noticed broken links in the last couple months, then I don't know what I was remembering.)

[Jireh Loreaux]

Ah, I have not checked in recent months, I'm just regurgitating the prior wisdom.

[Michael Kane]

In case it is helpful, the solution to the problem described above is shown below. I don't claim it is the best solution or that it makes the best use of mathlib4.

import Mathlib
open Set

variable (a x: ℝ)

theorem is_div_ge_one (h1 : x ≥ a ) (h2 : a > 0) : x / a ≥ 1 := by
  have h3 : x ≥ 0 := by linarith
  have h4 : a ≥ a := by linarith
  have h5 : a ≠ 0 := by linarith
  calc
    x / a ≥ a / a := by exact div_le_div h3 h1 h2 h4
    _ = 1 := by exact div_self h5

theorem ind_x_ge_a  (h1 : a > 0) (h2 : x ≥ a): (indicator { k | k ≥ a } 1 x) ≤ x / a := by
  calc
    indicator {k | k ≥ a} 1 x = 1 := by exact indicator_of_mem h2 1
    _ ≤ x / a := by exact is_div_ge_one a x h2 h1

theorem is_div_lt_one (h1 : x ≥ 0 ) (h2 : ¬ (x ≥ a) ) : x / a ≥ 0  := by
  have h3 : a ≥ 0 := by linarith
  calc
    0 ≤ x / a := by exact div_nonneg h1 h3

theorem ind_not_x_ge_a (h1 : ¬ x ≥ a) (h3 : x ≥ 0): (indicator { k | k ≥ a } 1 x) ≤ x / a := by
  calc
    indicator {k | k ≥ a} 1 x = 0 := by exact indicator_of_not_mem h1 1
    _ ≤ x / a := by exact is_div_lt_one a x h3 h1

theorem deterministic_markov_inequality (h1 : a > 0) (h3 : x ≥ 0): (indicator { k | k ≥ a } 1 x) ≤ x / a := by
  if hp: x ≥ a then
    exact ind_x_ge_a a x h1 hp
  else
    exact ind_not_x_ge_a a x hp h3

[Eric Wieser]

Kyle Miller said:

(Jireh Loreaux I thought I might have heard that Zulip fixed the breaking links problem, but I haven't looked into it. If you've noticed broken links in the last couple months, then I don't know what I was remembering.)

I think thread links are still broken, but those are useless anyway as they go to the end of the thread. Message links definitely work correctly despite resolution or renaming

[Matt Diamond]

@Michael Kane FYI you can delete every by exact you've written in that proof, as it's unnecessary. by takes you into tactic mode and exact takes you right back out of it. by exact X is the same thing as just X.