## Stream: new members

### Topic: calclucaltion in ennreal.of_real

#### Daniil Homza (Sep 16 2022 at 09:55):

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 (Sep 16 2022 at 09:58):

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

#### Daniil Homza (Sep 16 2022 at 10:38):

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 (Sep 16 2022 at 10:43):

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 (Sep 16 2022 at 10:44):

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 (Sep 16 2022 at 11:04):

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 (Sep 16 2022 at 11:08):

In that case you should decrease the depth, right?

#### Daniil Homza (Sep 16 2022 at 11:15):

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 (Sep 16 2022 at 11:44):

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 (Sep 16 2022 at 11:44):

congr' is like congr' infinity

#### Damiano Testa (Sep 16 2022 at 11:54):

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 (Sep 16 2022 at 11:56):

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

#### Daniil Homza (Sep 16 2022 at 13:52):

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

#### Kevin Buzzard (Sep 16 2022 at 18:35):

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

Last updated: Dec 20 2023 at 11:08 UTC