calclucaltion in ennreal.of_real

Stream: new members

[Daniil Homza]

Hi all!

I have easy statment for proof

ennreal.of_real (Var[(X 0)] / (c^2m))=ennreal.of_real(Var[(X 0)]m / (c*m) ^ 2)

where (X 0) just some r.v. So all i want is to reduce m from left side. However, some computational tactics like simp, ring_nf, norm_num, finish... do not help me at all(i think it is because of ennreal). Can someone suggest me some way to proof it? :smile:

[Riccardo Brasca]

You should write a #mwe, and don't forget to use #backticks for readability!

[Daniil Homza]

Thank you, I try to do it in this way but did not find how can i do it in zulip before

So, here is the #mwe

import tactic
import probability.notation
import probability.variance

open measure_theory

open_locale probability_theory ennreal

namespace probability_theory

variables {Ω : Type*} [measure_space Ω] [is_probability_measure (ℙ : measure Ω)][c:ℝ]



theorem eq1 {X : ℕ → Ω → ℝ}
(hint : integrable (X 0)) (hs : mem_ℒp (X 0) 2)(hc : 0 < c):
∀ (m:ℕ), (m>0) -> ennreal.of_real (Var[(X 0)] / (c^2*m))=ennreal.of_real(Var[(X 0)] *m/ (c*m) ^ 2):=
begin
intros m mp,

end
end probability_theory

I just want to solve this problem(there are no error in code). Thank you in advance

[Kevin Buzzard]

Thanks for the MWE! It makes it much easier to give a quick and useful answer.

This goal does not look true to me. You have an $m$ on one side of the equation and an $m^2$ on the other. Or am I missing something? If it's a slip on your part, can you edit the MWE? (you don't have to post it again, you can edit the original post)

[Kevin Buzzard]

If you believe me that there's a slip, then something like

begin
  intros m mp,
  congr' 2,
  ring,
  -- ⊢ ↑m * c ^ 2 = ↑m ^ 2 * c ^ 2
end

should get you close. The congr' tactic cancels all the stuff which is identical on both sides (the ennreal and the Var) and you're just left with the algebra.

[Daniil Homza]

Yes, you are right. I forgot about extra m in RHS . Now is correct in the above and the right statment will be

theorem eq1 {X : ℕ → Ω → ℝ}
(hint : integrable (X 0)) (hs : mem_ℒp (X 0) 2)(hc : 0 < c):
∀ (m:ℕ), (m>0) -> ennreal.of_real (Var[(X 0)] / (c^2*m))=ennreal.of_real((Var[(X 0)]* m) / (c*m) ^ 2):=
begin
intros m mp,
congr' 2,
ring,
  -- ⊢ ↑m * c ^ 2 = ↑m ^ 2 * c ^ 2

end

But congr' do not understand problem pretty well. Problem here is to reduce by m RHS. congr' try to show that the numerator and denominator on the left correspond to the numerator and denominator on the right, which is not true, I try to increase deepness of congr up to 4 but it do not help.

[Yaël Dillies]

In that case you should decrease the depth, right?

[Daniil Homza]

As I see in documentation of cong' is more aggressive than cong` 2. In my case decreasing entails spliting onto 3 goals, each of which is not correct :sweat_smile:

[Kevin Buzzard]

Yes, that's also what I did first :-) and then you just have to try numbers and keep making them smaller until all the goals are correct, or making them bigger until all the things you want to cancel, do cancel.

[Kevin Buzzard]

congr' is like congr' infinity

[Damiano Testa]

There is also congrm _ which allows you to replace the _ by a pattern-match. For instance, you can do this:

theorem eq1 {X : ℕ → Ω → ℝ}
(hint : integrable (X 0)) (hs : mem_ℒp (X 0) 2)(hc : 0 < c):
∀ (m:ℕ), (m>0) -> ennreal.of_real (Var[(X 0)] / (c^2*m))=ennreal.of_real((Var[(X 0)]* m) / (c*m) ^ 2):=
begin
intros m mp,
rw [← div_inv_eq_mul Var[X 0], div_div],
congrm ennreal.of_real (Var[X 0] / _),
  -- ⊢ c ^ 2 * ↑m = (↑m)⁻¹ * (c * ↑m) ^ 2

end

[Damiano Testa]

(In this specific case, you could also replace Var[X 0] with _, since the corresponding side-goal is solved by reflexivity.)

[Daniil Homza]

Thank you all :smiley: :tada: now it is work

[Kevin Buzzard]

Note how posting the mwe enabled very efficient progress on your question!