# Zulip Chat Archive

## 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^2*m))=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