One integral away from Euler's summation formula

Stream: maths

[Marc Masdeu]

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]

Have you tried using docs#measure_theory.integral_mono?

[Marc Masdeu]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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]

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

[Kevin Buzzard]

Well done @Marc Masdeu !

[Marc Masdeu]

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

[Johan Commelin]

Congrats!!

[Johan Commelin]

are you planning to PR it to mathlib?

[Marc Masdeu]

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]

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

[Johan Commelin]

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]

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]

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

[Heather Macbeth]

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]

@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]

@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]

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]

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]

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

[Marc Masdeu]

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