## Stream: new members

### Topic: Dealing with finite series

#### Mantas Baksys (Apr 12 2021 at 22:12):

Hi, everyone! I was formalising Riemann integration as a side project and got really really stuck with this.

import data.real.basic
import data.finset.sort

open_locale big_operators
open set

noncomputable theory

structure dissection (a b : ℝ) (S : finset ℝ) :=
(to_right: a < b)
(mem_Icc: ∀ x ∈ S, a ≤  x ∧ x ≤ b)
(mem_endpoints : a ∈ S ∧ b ∈ S)

def dissection.N {a b: ℝ} {S:finset ℝ} (D: dissection a b S) : ℕ := S.card -1

def dissection.function {a b: ℝ} {S: finset ℝ} (D: dissection a b S): fin((D.N)+1) → ℝ :=
begin
intro x,
exact (S.sort (≤)).nth_le x sorry, --sorry is trivial, ommited to reduce length of mwe
end

def upper_Riemann_sum {a b : ℝ} {S:finset ℝ} (D: dissection a b S) (f: ℝ → ℝ ) (h: ∃(M:ℝ), ∀ (x:Icc a b), abs(f x) ≤ M):=
∑ i: fin (D.N), (D.function (i.succ) - D.function i)* Sup(set.range (set.restrict f (Icc (D.function i) (D.function (i.succ)))))

lemma refinement_upper_sum_le_singleton {S: finset ℝ} {f: ℝ → ℝ} (y: ℝ) {a b: ℝ} (h₁: ∃(M:ℝ), ∀ (x: Icc a b), abs(f x) ≤ M) (D₁ : dissection a b S)
(D₂: dissection a b (S∪{y})) : upper_Riemann_sum D₁ f h₁ ≤ upper_Riemann_sum D₂ f h₁ :=
begin
sorry,
end


The proof of this lemma is, of course, trivial, however I can't seem to come up with a way in Lean to essentially cancel D₁.N -1 terms on both sides and then prove an easy inequality, which I think will pose no problems. Does anybody have any ideas? Thanks in advance.

#### Mario Carneiro (Apr 12 2021 at 22:19):

where is the D₁.N -1 in your example?

#### Mario Carneiro (Apr 12 2021 at 22:20):

could you work out the sorry until you get stuck?

#### Mario Carneiro (Apr 12 2021 at 22:22):

One thing which will help a lot is to make dissection a Prop, since it's just a conjunction of Props

#### Mario Carneiro (Apr 12 2021 at 22:23):

Then, you can remove it as an argument from all the functions

#### Mario Carneiro (Apr 12 2021 at 22:29):

Your theorem is definitely not "trivial" due to the way it is stated. You have to prove statements about what sort does, using nth_le to turn a list into a function, and how finite sums over the range act

#### Mantas Baksys (Apr 13 2021 at 08:24):

Thanks @Mario Carneiro for the suggestion to turn dissection into Prop, will certainly do that.
The general idea, is to work under assumption that a<y<b and then find two elements, say x₁, x₂ ∈ S such that x₁ < y < x₂  and that they are closest to y (on the left and right respectively) . Then, I would like to argue that the inequality reduces to
 (x₁ - y)*Sup (set.range (set.restrict f (Icc x₁ y)) + (y-x₂)*Sup(set.range(set.restrict f (Icc y x₂))≤(x₁ - x₂)* Sup(set.range (set.restrict f (Icc x₁ x₂)) . However, as said before, that would require somehow proving that I can cancel D₁.N -1 terms on both sides that are the same.
I am sorry for not posting a longer attempt, it's all because I'm stuck at the 'idea' level still and can't seem to get past it for quite a while. Sorry if this is too vague...

#### Mario Carneiro (Apr 13 2021 at 08:26):

you might want to start with a simpler example if you haven't done many proofs in lean before. It's really easy to write a statement that is mathematically correct but way too hard to prove anything about

#### Mario Carneiro (Apr 13 2021 at 08:28):

Here's some partial progress on this based on that sketch

structure dissection (a b : ℝ) (S : finset ℝ) : Prop :=
(to_right: a < b)
(mem_Icc: ∀ x ∈ S, a ≤ x ∧ x ≤ b)
(mem_endpoints : a ∈ S ∧ b ∈ S)

def N (S : finset ℝ) : ℕ := S.card - 1

def func (S : finset ℝ) : fin (N S + 1) → ℝ :=
begin
intro x,
exact (S.sort (≤)).nth_le x sorry, --sorry is trivial, ommited to reduce length of mwe
end

def upper_Riemann_sum (S : finset ℝ) (f: ℝ → ℝ) : ℝ :=
∑ i : fin (N S), (func S i.succ - func S i) *
Sup (set.range (set.restrict f (Icc (func S i) (func S i.succ))))

lemma refinement_upper_sum_le_singleton {S : finset ℝ} {f : ℝ → ℝ} (y : ℝ) {a b : ℝ}
(h₁ : ∃ M : ℝ, ∀ (x : Icc a b), abs (f x) ≤ M)
(D₁ : dissection a b S) (D₂ : dissection a b (insert y S)) :
upper_Riemann_sum S f ≤ upper_Riemann_sum (insert y S) f :=
begin
by_cases y ∈ S, { rw finset.insert_eq_of_mem h },
cases e : S.card,
{ simp [finset.card_eq_zero.1 e],
sorry },
sorry,
end


#### Mario Carneiro (Apr 13 2021 at 08:29):

You really want to rewrite the sum as something over lists to make it easier to work with

#### Mario Carneiro (Apr 13 2021 at 08:33):

Here's an alternate definition that is much easier to prove things about but not obviously the same as the one you wrote

noncomputable def list.upper_Riemann_sum (f: ℝ → ℝ) : ℝ → list ℝ → ℝ
| a [] := 0
| a (b::l) := (b - a) * Sup (set.range (set.restrict f (Icc a b))) + list.upper_Riemann_sum b l

def upper_Riemann_sum (S : finset ℝ) (f: ℝ → ℝ) : ℝ :=
match S.sort (≤) with
| [] := 0
| (a::l) := list.upper_Riemann_sum f a l
end


#### Mantas Baksys (Apr 13 2021 at 09:03):

Thanks @Mario Carneiro , this is a really cool suggestion, will definitely play with the definitions you have suggested and will post again if I fail miserably :smiley:.

Last updated: May 15 2021 at 22:14 UTC