## Stream: maths

### Topic: One integral away from Euler's summation formula

#### Marc Masdeu (Dec 22 2020 at 18:54):

Hi,

I have been working on formalizing Euler's summation formula (#14 in Freek's list) and I am just missing this lemma:

import measure_theory.interval_integral
import measure_theory.lebesgue_measure
import measure_theory.set_integral
import analysis.calculus.deriv

noncomputable theory
open_locale classical
open_locale big_operators
open interval_integral
open real

theorem integral_strictly_pos_of_cont (f : ℝ → ℝ) (a b : ℝ)
(hf : continuous f)
(hab : a < b)
(h : ∀ (x : ℝ), a ≤ x → x ≤ b → 0 ≤ f x)
(hneq: ∃ x, a ≤ x ∧ x ≤ b ∧ 0 < f x) :
0 < ∫ x in a..b, f x :=
begin
sorry
end


I can prove that continuous -> integrable, but I am having trouble converting hypotheses like h into something usable. As a warm-up exercise, I am having trouble formalizing

theorem integral_nonneg_of_cont (f : ℝ → ℝ) (a b : ℝ)
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(hab : a ≤ b)
(h : ∀ (x : ℝ), a ≤ x → x ≤ b → 0 ≤ f x) :
0 ≤ ∫ x in a..b, f x := sorry


which looks a lot easier. Any help would be appreciated :-).

#### Heather Macbeth (Dec 22 2020 at 19:57):

Have you tried using docs#measure_theory.integral_mono?

#### Marc Masdeu (Dec 22 2020 at 20:52):

Thanks! I'll try, I guess that I need to construct functions which extend by 0 f and g outside the interval (a,b). Because directly it doesn't apply. But to be honest I hadn't been able to find that one. This is how I had started the first of the two (the one I'm ultimately interested in):

lemma integrable_of_cont {f : ℝ → ℝ} (a b : ℝ) (h : continuous f):
interval_integrable f measure_theory.measure_space.volume a b :=
begin
have hmeas : measurable f := continuous.measurable h,
have hconton : continuous_on f (set.interval a b) := continuous.continuous_on h,
apply continuous_on.interval_integrable hconton hmeas,
exact real.locally_finite_volume,
end

theorem integral_strictly_pos_of_cont (f : ℝ → ℝ) (a b : ℝ)
(hf : continuous f)
(hab : a < b)
(h : ∀ (x : ℝ), a ≤ x → x ≤ b → 0 ≤ f x)
(hneq: ∃ x, a ≤ x ∧ x ≤ b ∧ 0 < f x) :
0 < ∫ x in a..b, f x :=
begin
rw integral_pos_iff_support_of_nonneg_ae',
{
split, assumption,
simp only,
sorry
},
{
sorry
},
exact integrable_of_cont a b hf,
end


#### Sebastien Gouezel (Dec 22 2020 at 21:26):

Your strategy looks good to me. One sorry less:

lemma self_mem_ae_restrict {α : Type*} [measurable_space α] {μ : measure α}
{s : set α} (hs : is_measurable s):
s ∈ (μ.restrict s).ae :=
begin
rw ae_restrict_eq hs,
simp only [exists_prop, filter.mem_principal_sets, filter.mem_inf_sets],
exact ⟨univ, filter.univ_mem_sets, s, by simp⟩,
end

theorem integral_strictly_pos_of_cont (f : ℝ → ℝ) (a b : ℝ)
(hf : continuous f)
(hab : a < b)
(h : ∀ (x : ℝ), a ≤ x → x ≤ b → 0 ≤ f x)
(hneq: ∃ x, a ≤ x ∧ x ≤ b ∧ 0 < f x) :
0 < ∫ x in a..b, f x :=
begin
apply (integral_pos_iff_support_of_nonneg_ae' _ _).2,
{ sorry },
{ have : Ioc b a = ∅ := Ioc_eq_empty hab.le,
simp only [this, union_empty],
exact filter.eventually_of_mem
(self_mem_ae_restrict is_measurable_Ioc) (λ x hx, h x hx.1.le hx.2) },
{ exact integrable_of_cont a b hf }
end


#### Sebastien Gouezel (Dec 22 2020 at 21:56):

No sorry left:

import measure_theory.interval_integral
import measure_theory.lebesgue_measure
import measure_theory.set_integral
import analysis.calculus.deriv

noncomputable theory
open_locale classical
open_locale big_operators
open_locale topological_space
open interval_integral
open real
open measure_theory
open set

lemma integrable_of_cont {f : ℝ → ℝ} (a b : ℝ) (h : continuous f):
interval_integrable f measure_theory.measure_space.volume a b :=
begin
have hmeas : measurable f := continuous.measurable h,
have hconton : continuous_on f (set.interval a b) := continuous.continuous_on h,
apply continuous_on.interval_integrable hconton hmeas,
exact real.locally_finite_volume,
end

lemma self_mem_ae_restrict {α : Type*} [measurable_space α] {μ : measure α}
{s : set α} (hs : is_measurable s):
s ∈ (μ.restrict s).ae :=
begin
rw ae_restrict_eq hs,
simp only [exists_prop, filter.mem_principal_sets, filter.mem_inf_sets],
exact ⟨univ, filter.univ_mem_sets, s, by simp⟩,
end

lemma nonempty_inter_of_nonempty_inter_closure {α : Type*} [topological_space α] {s t : set α}
(hs : is_open s) (h : (s ∩ closure t).nonempty) : (s ∩ t).nonempty :=
let ⟨x, xs, xt⟩ := h in _root_.mem_closure_iff.1 xt s hs xs

lemma real.volume_pos_of_is_open_of_nonempty {s : set ℝ} (h : is_open s) (h' : s.nonempty) :
0 < volume s :=
begin
rcases h' with ⟨x, hx⟩,
have : ∀ᶠ (y : ℝ) in 𝓝 x, y ∈ s := filter.eventually_of_mem (mem_nhds_sets h hx) (λ y H, H),
exact filter.eventually.volume_pos_of_nhds_real this,
end

theorem integral_strictly_pos_of_cont (f : ℝ → ℝ) (a b : ℝ)
(hf : continuous f)
(hab : a < b)
(h : ∀ (x : ℝ), a ≤ x → x ≤ b → 0 ≤ f x)
(hneq: ∃ x, a ≤ x ∧ x ≤ b ∧ 0 < f x) :
0 < ∫ x in a..b, f x :=
begin
rw integral_pos_iff_support_of_nonneg_ae',
{ refine ⟨hab, _⟩,
let s := {b : ℝ | 0 < f b},
have s_open : is_open s := is_open_lt continuous_const hf,
have : (s ∩ closure (Ioo a b)).nonempty,
{ rw closure_Ioo hab,
rcases hneq with ⟨x, ax, xb, fxpos⟩,
have : x ∈ s ∩ Icc a b := ⟨fxpos, ax, xb⟩,
exact nonempty_of_mem this },
have : (s ∩ Ioo a b).nonempty := nonempty_inter_of_nonempty_inter_closure s_open this,
have : 0 < volume (s ∩ Ioo a b) :=
real.volume_pos_of_is_open_of_nonempty (is_open_inter s_open is_open_Ioo) this,
refine this.trans_le (measure_mono (λ x hx, _)),
split,
{ exact ne_of_gt (show 0 < f x, from hx.1) },
{ exact ⟨hx.2.1, hx.2.2.le⟩ } },
{ have : Ioc b a = ∅ := Ioc_eq_empty hab.le,
simp only [this, union_empty],
exact filter.eventually_of_mem
(self_mem_ae_restrict is_measurable_Ioc) (λ x hx, h x hx.1.le hx.2) },
{ exact integrable_of_cont a b hf }
end


#### Marc Masdeu (Dec 22 2020 at 22:16):

Thanks, that's great! Tomorrow I'll post the complete proof on GitHub

#### Yury G. Kudryashov (Dec 22 2020 at 22:34):

A version of integrable_of_cont is a part of branch#ftc2 #4945

#### Heather Macbeth (Dec 22 2020 at 22:37):

Actually (although that branch adds new versions) I put in the basic version docs#continuous.interval_integrable a couple of weeks ago #5288

#### Yury G. Kudryashov (Dec 22 2020 at 22:38):

@Heather Macbeth Sure, I'm sorry for a wrong reference.

#### Kevin Buzzard (Dec 22 2020 at 22:38):

Well done @Marc Masdeu !

#### Marc Masdeu (Dec 23 2020 at 16:01):

The proof is there. One more down from Freek's list :smile:
https://github.com/mmasdeu/euler

Congrats!!

#### Johan Commelin (Dec 23 2020 at 16:02):

are you planning to PR it to mathlib?

#### Marc Masdeu (Dec 23 2020 at 16:05):

If there is interest, I could try. But I'd rather work on another project, this was just a fun exercise. It would be good to have zeta(2k) in there, and I hoped that I would be able to reuse some of what I learned to give that a try.

#### Johan Commelin (Dec 23 2020 at 16:17):

If it doesn't get PRd, then it won't compile with mathlib of 2 months from now.

#### Johan Commelin (Dec 23 2020 at 16:17):

If you PR it, then other people will keep your code compatible. This will be helpful even for you yourself, if you plan on reusing parts of it.

#### Heather Macbeth (Dec 23 2020 at 16:25):

It looks like there is a lot of useful material in there, in addition to the headline result! You prove integration by parts, it'd be very nice to have this in mathlib.

#### Heather Macbeth (Dec 23 2020 at 16:25):

If PR'ing the whole thing is overwhelming, maybe you could do that as a test case.

#### Heather Macbeth (Dec 23 2020 at 16:30):

You prove your own FTC-2 too, since as you correctly gathered, it is not in mathlib currently. But it should be soon (#4945) which would shorten the "path" of new material on the way to integration by parts.

#### Marc Masdeu (Dec 23 2020 at 18:57):

@Johan Commelin I know there are very solid pros to PRing many theorems to mathlib, but there are some cons, like the extra effort it requires. The argument about having other people maintain the code since it's in mathlib is correct, but if you see how SageMath has been evoling over the years, you see that the fact that there is so much intertwinned code makes it hard to develop new stuff, and eventually all tickets / PRs are about refactoring and the maths parts stops improving.
Still, I think that mathlib is far from that stage now, and that most of what I've written should be in mathlib, so I'm not saying no to PRing in this particular case!

#### Marc Masdeu (Dec 23 2020 at 19:01):

@Heather Macbeth thanks for the encouragement! I started this as I was aware that FTC2 was on its way, and I put it up as a black-box from which to get an immediate application. So what's in integrals.lean was originally a bunch of sorry's. But then I couldn't resist the urge to try to fill them in... By the way, I took ftc1 from https://github.com/jjaassoonn/transcendental and there is a lot of interesting stuff in there as well!

#### Heather Macbeth (Dec 23 2020 at 20:13):

By the way, that version of FTC-1 has several unnecessary hypotheses! You can leave out hf, h, hf3, hx0:

import measure_theory.interval_integral

lemma ftc1 {f : ℝ -> ℝ} (hf2 : continuous f) (a b : ℝ) (x0 : ℝ) :
has_deriv_at (λ (b : ℝ), ∫ (x : ℝ) in a..b, f x) (f x0) x0 :=
interval_integral.integral_has_deriv_at_right (hf2.interval_integrable _ _) hf2.continuous_at


But I agree that it would be very nice to add this variant of FTC-1 to mathlib, the use case (i.e., when f is continuous) is very common.

#### Alex J. Best (Jan 02 2021 at 19:31):

Marc Masdeu said:

The proof is there. One more down from Freek's list :smile:
https://github.com/mmasdeu/euler

You should make a PR to add it to the 100 theorems list at least :smile: https://github.com/leanprover-community/mathlib/blob/master/docs/100.yaml there are a few other examples there (like number 18) that link to a non-mathlib repo for the result!

#### Johan Commelin (Jan 07 2021 at 10:20):

#5655 @Marc Masdeu I added this to the list 100.yaml

#### Marc Masdeu (Jan 07 2021 at 12:11):

I should have done this but I still need even to ask permissions... Thanks a lot @Johan Commelin !

Last updated: May 19 2021 at 02:10 UTC