Inequality with ennreal type

Stream: new members

[Daniil Homza]

Hi All!

I came to the last stage of the proof of the Weak Law but I have big troubles with it. Namely, I try to proof inequality below in ennreal terms, which will be close my proof since of chebyshev inequality.

import tactic
import probability.ident_distrib
import probability.notation
import probability.integration
import probability.variance
import topology.metric_space.basic
import algebra.order.floor


open measure_theory filter finset

open_locale topological_space big_operators measure_theory probability_theory ennreal nnreal

namespace probability_theory


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





theorem weak_law {X : ℕ → Ω → ℝ} (hc : 0 < c):
tendsto (λ (n : ℕ), ℙ {ω | c*n ≤|(∑ i in range n, X i ) ω - n*𝔼[(X 0)]|}) at_top (𝓝 0) :=
begin
rw ennreal.tendsto_at_top_zero,
intros e ep,
let N:= nat.ceil(Var[(X 0)]/(c^2*(ennreal.to_real(e)))),
use N,
intros n n_more_N,

have A: ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e,
    have C: Var[(X 0)]/(c^2*(ennreal.to_real(e)))≤nat.ceil(Var[(X 0)]/(c^2*(ennreal.to_real(e)))),
    simp only[nat.le_ceil],

end

end probability_theory

I am trying to get rid of the ennreal part and transform the expression using assumptions on n, but all I can do is to rid of integer part. Maybe some suggestion what can I do? Thank you :smile:

[Kevin Buzzard]

Your code has two unsolved goals. Which step do you have a problem with? Can you just present me with the goal you want closed, and with the hypotheses which justify the claim mathematically?

[Daniil Homza]

Ineq.pdf
Dear Kevin,

Yes, sure, I just try to leave this inequality in context. Here is a goal which I want to proof and assumption which we can use

import tactic
import probability.notation
import probability.integration
import probability.variance
import algebra.order.floor


open measure_theory filter finset

open_locale topological_space big_operators measure_theory probability_theory ennreal nnreal

namespace probability_theory


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





theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
(c:ℝ)(hc : 0 < c)
(e:ℝ≥0∞)(e_pos: e > 0)
(N: ℕ := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊)
(n: ℕ)(n_pos: n ≥ N):
 ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin


end

end probability_theory

As well I am sending overleaf version of theorem. Proof is naive in sense of math but if you want I can sent you proof too.

[Eric Wieser]

Note you can write $\LaTeX$ directly into Zulip between double dollars, no need to link to overleaf (at least, for short-ish things)

[Daniil Homza]

Eric Wieser said:

Note you can write $\LaTeX$ directly into Zulip between double dollars, no need to link to overleaf (at least, for short-ish things)

Zulip is so smart, I did not expect this. Thank you so much!

[Eric Wieser]

Your theorem is false, because (N: ℕ := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊) doesn't say what you think it does

[Eric Wieser]

That says "let N be any natural. If the user chooses not to provide one, then pick this one for them"

[Eric Rodriguez]

has mathlib ever used opt_param?

[Yaël Dillies]

Yes, for proof arguments to data functions like docs#finset.disj_union.

[Daniil Homza]

Eric Wieser said:

That says "let N be any natural. If the user chooses not to provide one, then pick this one for them"

Eric, Thank you for your comment. In a first section (were my actual statment is) I introduce N with function let. Is it correct form of introducing N. By the way, I will be very happy if you share how I can introduce N in assumption.

[Eric Wieser]

In this particular case I'd recommend just not doing so:

theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
  (c:ℝ)(hc : 0 < c)
  (e:ℝ≥0∞)(e_pos: e > 0)
  (n: ℕ) (n_pos: n ≥ ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊):
  ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin
end

[Eric Wieser]

But you could also write

theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
  (c:ℝ)(hc : 0 < c)
  (e:ℝ≥0∞)(e_pos: e > 0)
  (n: ℕ) (n_pos: let N := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊ in n ≥ N):
  ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin
end

[Daniil Homza]

Okay, I see, Thank You very much!

[Eric Wieser]

Or even

theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
  (c:ℝ)(hc : 0 < c)
  (e:ℝ≥0∞)(e_pos: e > 0) :
  let N := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊ in ∀ (n: ℕ) (n_pos : n ≥ N),
    ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin
end

[Daniil Homza]

Eric Wieser said:

Or even

theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
  (c:ℝ)(hc : 0 < c)
  (e:ℝ≥0∞)(e_pos: e > 0) :
  let N := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊ in ∀ (n: ℕ) (n_pos : n ≥ N),
    ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin
end

Thank you, I have changed it in my last code!

[Kevin Buzzard]

theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
  (c:ℝ)(hc : 0 < c)
  (e:ℝ≥0∞)(e_pos: e > 0) :
  let N := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊ in ∀ (n: ℕ) (n_pos : n ≥ N),
    ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin
  intros N n hn,
  -- annoying special case n = 0
  rcases nat.eq_zero_or_pos n with (rfl | hn0), { simp, },
  -- annoying special case e = ∞
  rcases eq_top_or_lt_top e with (rfl | he), { simp, },
  -- using N just makes things more annoying. Why not just not define N at all?
  change ⌈ _ ⌉₊ ≤ n at hn,
  -- get rid of ceiling
  rw nat.ceil_le at hn,
  -- get rid of ennreal stuff in goal
  apply ennreal.of_real_le_of_le_to_real,
  -- clear denominators (will show they're positive later)
  rw div_le_iff at hn ⊢,
  { -- main goal now easy
    convert hn using 1,
    ring, },
  { -- positivity side goal: a bit annoying that I need to use theorems and not tactics here
    exact mul_pos (pow_pos hc 2) (by exact_mod_cast hn0), },
  { -- second positivity side goal: here we still have to deal with e
    refine mul_pos (pow_pos hc 2) _,
    rw ennreal.to_real_pos_iff,
    exact ⟨e_pos, he⟩, }
end

@Daniil Homza

[Daniil Homza]

Kevin Buzzard said:

theorem weak_law {X : ℕ → Ω → ℝ}  (hs : mem_ℒp (X 0) 2) (hint : integrable (X 0))
  (c:ℝ)(hc : 0 < c)
  (e:ℝ≥0∞)(e_pos: e > 0) :
  let N := ⌈Var[X 0] / (c ^ 2 * e.to_real)⌉₊ in ∀ (n: ℕ) (n_pos : n ≥ N),
    ennreal.of_real (Var[(X 0)]/(c^2*n)) ≤ e :=
begin
  intros N n hn,
  -- annoying special case n = 0
  rcases nat.eq_zero_or_pos n with (rfl | hn0), { simp, },
  -- annoying special case e = ∞
  rcases eq_top_or_lt_top e with (rfl | he), { simp, },
  -- using N just makes things more annoying. Why not just not define N at all?
  change ⌈ _ ⌉₊ ≤ n at hn,
  -- get rid of ceiling
  rw nat.ceil_le at hn,
  -- get rid of ennreal stuff in goal
  apply ennreal.of_real_le_of_le_to_real,
  -- clear denominators (will show they're positive later)
  rw div_le_iff at hn ⊢,
  { -- main goal now easy
    convert hn using 1,
    ring, },
  { -- positivity side goal: a bit annoying that I need to use theorems and not tactics here
    exact mul_pos (pow_pos hc 2) (by exact_mod_cast hn0), },
  { -- second positivity side goal: here we still have to deal with e
    refine mul_pos (pow_pos hc 2) _,
    rw ennreal.to_real_pos_iff,
    exact ⟨e_pos, he⟩, }
end

Daniil Homza

Dear Kevin,

Thank You so much, It works. It is look very smart and amazing to see how Lean work in real problems. I think it helps me a lot in Lean learning. Thank You!

@Kevin Buzzard