Stating theorem about memorylessness

Stream: new members

[Matthias Liesenfeld]

I have a definition

def isMemoryless (P : Measure ℕ) [IsProbabilityMeasure P] : Prop :=
  ∀ (n m : ℕ), P[{k | k > n + m} | {k | k ≥ n}] = P {k | k > m}

and a theorem

theorem geometricMeasure_iff_memoryless {P : Measure ℕ} [IsProbabilityMeasure P]
  (hp_pos : 0 < ENNReal.toReal (P {0}))
  (hp_le_one : ENNReal.toReal (P {0}) ≤ 1) :
    P = geometricMeasure hp_pos hp_le_one
  ↔ isMemoryless P.

But it should rather be like

theorem geometricMeasure_iff_memoryless' {P : Measure ℕ} [IsProbabilityMeasure P]
    P = geometricMeasure (hp_pos : 0 < ENNReal.toReal (P {0}))
        (hp_le_one : ENNReal.toReal (P {0}) ≤ 1 := by sorry)
  ↔ isMemoryless P.

That is, the prop hp_pos follows from isMemoryless P and it always holds hp_le_one. I don't know the syntax for introducing and using a prop at once.

[Kenny Lau]

what is the mathematical statement (in latex)?

[Matthias Liesenfeld]

I think it would be something like $P \sim \text{Geo}(P \{0\}) \Leftrightarrow P \text{ is memoryless}$ where Geo is the Geometric distribution on $\{0, 1, \ldots \}$ .

[Kenny Lau]

right, but Lean requires 0 < x <= 1 whenever you talk about Geo, and you have omitted those in your latex

[Matthias Liesenfeld]

Then it would rather be:
$0 < P \{0\} \le 1 \;\wedge\; P = \text{Geo}(P\{0\}) \Leftrightarrow P \text{ is memoryless}.$

[Robin Arnez]

So

theorem isMemoryless_iff_eq_geometricMeasure {P : Measure ℕ} [IsProbabilityMeasure P] :
    isMemoryless P ↔ ∃ hp_pos hp_le_one, P = geometricMeasure hp_pos hp_le_one := by ...

would be the right theorem statement

[Matthias Liesenfeld]

Robin Arnez schrieb:

So

theorem isMemoryless_iff_eq_geometricMeasure {P : Measure ℕ} [IsProbabilityMeasure P] :
    isMemoryless P ↔ ∃ hp_pos hp_le_one, P = geometricMeasure hp_pos hp_le_one := by ...

would be the right theorem statement

Not only does it hold that $P = Geo(p)$ for some $0<p\le 1$ but it must specifically hold $p=P \{0\}.$ I think this theorem statement doesn't account for that. Am I mistaken?

[Kenny Lau]

P = geometricMeasure hp_pos hp_le_one would imply p = P{0} right

[Robin Arnez]

Ah so perhaps:

theorem isMemoryless_iff_eq_geometricMeasure {P : Measure ℕ} [IsProbabilityMeasure P] :
    isMemoryless P ↔ ∃ hp_pos hp_le_one, P = geometricMeasure (p := (P {0}).toReal) hp_pos hp_le_one := by
  sorry

[Etienne Marion]

You don't need hp_le_one:

import Mathlib

open MeasureTheory ProbabilityTheory

def isMemoryless (P : Measure ℕ) [IsProbabilityMeasure P] : Prop := sorry

theorem isMemoryless_iff_eq_geometricMeasure {P : Measure ℕ} [IsProbabilityMeasure P] :
    isMemoryless P ↔ ∃ hp_pos, P = geometricMeasure (p := (P {0}).toReal) hp_pos measureReal_le_one := by
  sorry