Proving statement for elements of [0,1]

Stream: new members

[Matthias Liesenfeld]

I want to show that for $a, b$ in $[0,1]$ it holds $a * (1 - b) = a - a * b$.
For $a,b$ in the Reals one can write:

example (a b : ℝ) : a * (1 - b) = a - a * b := mul_one_sub a b

How can one prove

example (a b : Set.Icc (0 : ℝ) 1) : a * (1 - b) = a - a * b?

[Aaron Liu]

does this work

import Mathlib

example (a b : unitInterval) : a * (1 - b : ℝ) = a - a * b :=
  mul_one_sub (a : ℝ) b

[Notification Bot]

This topic was moved here from #mathlib4 > Proving statement for elements of [0,1] by Patrick Massot.

[Patrick Massot]

Matthias, the answer is that you should try to do that. You’ll be fighting the system and get very frustrated. The idiomatic statement would look like

import Mathlib

open Set

example (a b : ℝ)(ha : a ∈ Icc 0 1)  (hb : b ∈ Icc 0 1) : a * (1 - b) = a - a * b := by
  ring

[Patrick Massot]

But in this case it looks very weird since the assumptions are useless. We may be able to help you more if you post a more realistic example.

[Matthias Liesenfeld]

Thanks for all the very fast and insightful answers :)

@Patrick Massot Did you have a typo and were saying I should not try to do that?

The context is, I want to prove that the geometric distribution is characterized by a memoryless property. Doing so at some point I want to prove

example (P : Measure ℕ) [IsProbabilityMeasure P] (n : ℕ) (h : P {n} = P {k | k ≥ n} - P {k | k ≥ n} * P {k | k > 0}) :
    P {n} = P {k | k ≥ n} * (1 - P {k | k > 0})

The measure P maps to type \ENNReal. But, since IsProbabilityMeasure P, we know that actually P of something is an element of [0,1] in the Reals (mathematically speaking). Is there an ideomatic way of handling that problem?

[Kenny Lau]

probability stuff is a known pain-point if that makes you feel better

[Rémy Degenne]

Working with ENNReal is not that bad (although it's much less automated than in Real):

import Mathlib
open MeasureTheory

example (P : Measure ℕ) [IsProbabilityMeasure P] (n : ℕ)
    (h : P {n} = P {k | k ≥ n} - P {k | k ≥ n} * P {k | k > 0}) :
    P {n} = P {k | k ≥ n} * (1 - P {k | k > 0}) := by
  rwa [ENNReal.mul_sub (by simp), mul_one]

But if you want to work in Real you could prove statements about docs#MeasureTheory.Measure.real :

import Mathlib
open MeasureTheory

example (P : Measure ℕ) [IsProbabilityMeasure P] (n : ℕ)
    (h : P.real {n} = P.real {k | k ≥ n} - P.real {k | k ≥ n} * P.real {k | k > 0}) :
    P.real {n} = P.real {k | k ≥ n} * (1 - P.real {k | k > 0}) := by
  ring_nf
  exact h

[Patrick Massot]

Sorry, there was a typo indeed.

[Matthias Liesenfeld]

Thanks a lot :)

[Alex Meiburg]

I have a lot of similar stuff here: https://github.com/Timeroot/Lean-QuantumInfo/blob/main/ClassicalInfo/Prob.lean
If you "believe" that Set.Icc (0 : ℝ) 1 should be its own type with its own semantics, then this is a reasonable way to proceed. (Indeed, as Aaron Liu pointed out, we have docs#unitInterval in Mathlib. But this is generally used as a 'topological' interval, not a 'probability' interval.)

When you write (a : Set.Icc (0 : ℝ) 1), Lean transparently interprets this as a being a docs#Subtype of the reals, that happens to obey a ∈ Icc 0 1. Then when you write a * _, 1 - b, or an equality, it tries to infer the appropriate relations from Subtype. For equality, this is easy to define: the subtypes are equal if their values are equal.

You can access this by rewriting with Subtype.eq_iff. But, it isn't "obvious" the same way that there's a well-defined notion of multiplication, subtraction, or "1" on this subtype. (Consider: what if it was Set.Icc 5 13 instead, how should multiplication work? Or, what should the value of 0 - 1 be?) You'd have to define these in an appropriate way. For unitInterval, there is a defined meaning of "0" and "1" (the standard real value, together with the proof that it belongs to the set). But there's no multiplication or subtraction defined, because as I said, it's "generally" a topological sense of the interval.

[Alex Meiburg]

https://github.com/Timeroot/Lean-QuantumInfo/blob/0a2d1075d5e6b2013b4e0e3ca1e77ed7cc2cd189/ClassicalInfo/Prob.lean#L41 shows how you can set up your own multiplication on the type, if you want. It obeys the real multiplication, and then everything works "nicely".

https://github.com/Timeroot/Lean-QuantumInfo/blob/0a2d1075d5e6b2013b4e0e3ca1e77ed7cc2cd189/ClassicalInfo/Prob.lean#L153 defines subtraction. It's more unpleasant, because it's truncating subtraction (much like Nat subtraction in core), so 0.5 - 0.7 = 0. It has to be defined as _the maximum of the real subtraction, or zero_, and then you still need to prove that this is always less than 1.

Accordingly, the theorems about it are messier.