nat powers of probabilities

Stream: Is there code for X?

[Stuart Presnell]

Does mathlib already know that the real interval [0,1] is closed under powers of natural numbers? (So that, for example, given a probability 0 ≤ p ≤ 1 its power 0 ≤ p^n ≤ 1 is also a probability.)

I have the following:

variables (p : Icc (0:ℝ) 1)

#check p^2  -- Fails:   "failed to synthesize type class instance for `has_pow ↥(Icc 0 1) ℕ`"

def prob_pow_Icc {α : Type*} [ordered_semiring α] (p : Icc (0:α) 1) (n : ℕ) : (Icc (0:α) 1) :=
begin
  rcases p with ⟨p, ⟨hp0, hp1⟩⟩,
  refine ⟨p^n, ⟨pow_nonneg hp0 n, pow_le_one n hp0 hp1⟩⟩,
end

instance {α : Type*} [ordered_semiring α] : has_pow (Icc (0:α) 1) ℕ := ⟨prob_pow_Icc⟩

#check p^2  -- This works now:  "p ^ 2 : ↥(Icc 0 1)"

Is this the right way to go about things? Is it worth PRing this instance (and if so, where)?

[Yaël Dillies]

This looks a bit like it

lemma maps_to_bit0_zero_compl {n : ℕ} (hn : n ≠ 0) : maps_to (λ x : ℝ, x ^ bit0 n) {0}ᶜ (Ioi 0) :=
λ x hx, (pow_bit0_pos_iff _ hn).2 hx

lemma maps_to_sq_zero_compl : maps_to (λ x : ℝ, x ^ 2) {0}ᶜ (Ioi 0) :=
maps_to_bit0_zero_compl one_ne_zero

[Kevin Buzzard]

I think that in general it's not advisable to make definitions in tactic mode: this might be better-behaved for when you start proving theorems about p^n:

def prob_pow_Icc {α : Type*} [ordered_semiring α] (p : Icc (0:α) 1) (n : ℕ) : (Icc (0:α) 1) :=
begin
  rcases p with ⟨p, ⟨hp0, hp1⟩⟩,
  refine ⟨p^n, ⟨pow_nonneg hp0 n, pow_le_one n hp0 hp1⟩⟩,
end

#print prob_pow_Icc -- subtype.cases_on blah

def prob_pow_Icc' {α : Type*} [ordered_semiring α] (p : Icc (0:α) 1) (n : ℕ) : (Icc (0:α) 1) :=
⟨p^n, ⟨pow_nonneg p.2.1 n, pow_le_one n p.2.1 p.2.2⟩⟩

#print prob_pow_Icc' -- looks far less scary

[Yaël Dillies]

What you really should do is provide comm_monoid_with_zero (Icc 0 1). Then you'll get powers for free.

[Yaël Dillies]

You can also do comm_semigroup_with_zero (Ico 0 1), comm_monoid (Ioc 0 1), comm_semigroup (Ioo 0 1), comm_monoid_with_zero (Icc (-1) 1), comm_monoid_with_zero (Ioc (-1) 1), comm_semigroup_with_zero (Ioo (-1) 1), and also provide has_distrib_neg instances where applicable.

[Stuart Presnell]

Ok, I'll try that. Where should these instances be put? In data/set/intervals/basic?

[Stuart Presnell]

Or would it be better to start a new file data/set/intervals/instances, since .../basic is already 1460 lines?

[Scott Morrison]

1000 lines is a good rule of thumb :-)

[Damiano Testa]

What about the neglected half-infinite interval? :stuck_out_tongue_wink:

[Stuart Presnell]

You mean the one that goes a quarter of the way out to infinity in either direction?

[Damiano Testa]

I meant ˋIci 1ˋ and ˋIoi 1ˋ, one being a comm monoid, the other a comm semigroup. I hope that this is correct!

[Damiano Testa]

In fact, I think that ˋIci aˋ, for ˋ1 ≤ aˋ is also a comm semigroup, but I am not sure that you can make an instance for that.

[Damiano Testa]

(sorry, my backticks do not appear to work today)

[Yaël Dillies]

docs#nnreal :stuck_out_tongue:

[Damiano Testa]

Yaël, is that for me? I meant the interval [1,infinity), not [0,infinity). Maybe I am misunderstanding.

[Yaël Dillies]

Ah, right

[Yaël Dillies]

Although arguably that's multiplicative nnreal

[Damiano Testa]

I'm also sure that, with enough patience, we'd be able to get to_additive to prove the instance for all cases, from just one of them! :rofl:

[Stuart Presnell]

I have a draft of the instances for 0-1 intervals at #14288. I'd appreciate any feedback, as I'm sure there must be nicer ways to do much of this. In particular I couldn't figure out how to golf away the begin ... end blocks in comm_monoid_with_zero (Icc (0:α) 1).

[Eric Wieser]

I added some comments; you can make it a lot shorter with docs#function.injective.monoid and friends

[Stuart Presnell]

Thanks!

[Eric Wieser]

It turns out we already have lots of instances on docs#set.Icc0 1 (on the reals; see the list of instances in the docs) under the name docs#unit_interval