Dealing with finite series

Stream: new members

[Mantas Baksys]

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]

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

[Mario Carneiro]

could you work out the sorry until you get stuck?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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:.