Euler number (Real.exp 1) is transcendental

Stream: new members

[Ilmārs Cīrulis]

Managed get sick (maybe flu, urgh), so next days will try proving that Euler number or Real.exp 1 is transcendental (using this proof on Wikipedia).

Will ask lots of basic questions about integrals in Mathlib etc, probably. :sweat_smile:

Learning by doing. :partying_face:

[Ruben Van de Velde]

You don't feel like picking up #6718, which has this as a consequence? :)

[Ilmārs Cīrulis]

Oo, will take a look. What happened to the PR?

[Kevin Buzzard]

It's still there, looks like some definitions need some docstrings and there's a preliminary PR which needs merging.

[Ilmārs Cīrulis]

The first step is to make changes suggested by Vierkantor at #18693, right?
Ok, will try my best.

[Ilmārs Cīrulis]

@Ruben Van de Velde How can I become contributor to the specific branch (from #18693)?
Do I need some invitation or smth from you?

[Aaron Liu]

You can just work on it the same as you would work on your own branch (but it's polite to ask for permission).

[Ilmārs Cīrulis]

When I go to the branch and then open file in VS Code (and try to edit it), I get this.

image.png

[Aaron Liu]

This happens when I click "open file" from a commit in VSCode. This happens because "go to file" goes to the file at that point in the commit history (not the current file), which can't be edited. Does it go back to normal if you navigate to the file from the file system?

[Ilmārs Cīrulis]

You are right! Thank you!

[Ilmārs Cīrulis]

So, I wanted to start work.

First, I got the message Imports are out of date and must be rebuilt; use the "Restart File" command in your editor

Then after the Restart File:

`c:\Users\ilmar\.elan\toolchains\leanprover--lean4---v4.14.0-rc2\bin\lake.exe setup-file C:/Users/ilmar/Documents/Mathlib4/Mathlib/FieldTheory/Minpoly/IsConjRoot.lean Init Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Adjoin Mathlib.FieldTheory.Normal` failed:

stderr:
✖ [10/1426] Building Mathlib.Tactic.Linter.Header
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\LeanSearchClient\.lake\build\lib;.\.\.lake/packages\plausible\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\ilmar\.elan\toolchains\leanprover--lean4---v4.14.0-rc2\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true .\.\.\.\Mathlib\Tactic\Linter\Header.lean -R .\.\.\. -o .\.\.lake\build\lib\Mathlib\Tactic\Linter\Header.olean -i .\.\.lake\build\lib\Mathlib\Tactic\Linter\Header.ilean -c .\.\.lake\build\ir\Mathlib\Tactic\Linter\Header.c --json
error: .\.\.\.\Mathlib\Tactic\Linter\Header.lean:6:0: object file '.\.\.lake/packages\batteries\.lake\build\lib\Lean\Elab\Command.olean' of module Lean.Elab.Command does not exist
error: Lean exited with code 1
✖ [11/1426] Building Batteries.Tactic.Lint.Basic
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\LeanSearchClient\.lake\build\lib;.\.\.lake/packages\plausible\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\ilmar\.elan\toolchains\leanprover--lean4---v4.14.0-rc2\bin\lean.exe -Dlinter.missingDocs=true .\.\.lake/packages\batteries\.\.\Batteries\Tactic\Lint\Basic.lean -R .\.\.lake/packages\batteries\.\. -o .\.\.lake/packages\batteries\.lake\build\lib\Batteries\Tactic\Lint\Basic.olean -i .\.\.lake/packages\batteries\.lake\build\lib\Batteries\Tactic\Lint\Basic.ilean -c .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint\Basic.c --json
error: .\.\.lake/packages\batteries\.\.\Batteries\Tactic\Lint\Basic.lean:6:0: object file '.\.\.lake/packages\batteries\.lake\build\lib\Lean\Structure.olean' of module Lean.Structure does not exist

etc

[Ilmārs Cīrulis]

I'm a bit braindead for now, apologies.
Probably I'm doing something in wrong way. :thinking:

[Junyan Xu]

lean4 v4.14 is quite old (last December). #6718 isn't that old (it merged master 3 weeks ago). What could be wrong?

[Ilmārs Cīrulis]

Removed repository and cloned it again from Github. It seems that everything builds okay after the Restart File.

[Ilmārs Cīrulis]

Made changes in #18693. All checks are green, except this one (Post PR summary comment / post-or-update-summary-comment (pull_request))

No idea what I should do to make it green.

[Michael Rothgang]

That CI error is strange: can you merge master and see whether that fixes it?

[Ruben Van de Velde]

I've pushed a merge

[Michael Rothgang]

And that CI step is fine; you just have a deprecation warning to fix.

[Ilmārs Cīrulis]

Thank you!

[Ilmārs Cīrulis]

Replied to all comments of Vierkantor on the PR. Now will wait for their responses.

[Ilmārs Cīrulis]

While waiting for progress on the PR and having fun with flu (or whatever it is), I decided to tinker a bit with the wikipedia proof that e is transcendental. Just to get some experience and etc.

So, how to prove this? (looks like provable to me :thinking:)

import Mathlib

theorem integrable_translation_smth (a: ℝ) (s: Set ℝ) (f:  ℝ → ℝ) (H: MeasureTheory.IntegrableOn f s):
    MeasureTheory.IntegrableOn (fun x => f (x - a)) ((fun x => x + a) '' s) := by
  sorry

I couldn't find anything like that in Mathlib. :(

[Ilmārs Cīrulis]

Of course, in this specific proof I only need this theorem for Set.Ici sets, and this case I have proved.

[Ilmārs Cīrulis]

If MeasurableSet s, then there's proof.

import Mathlib

theorem integrable_translation_smth (a: ℝ) (s: Set ℝ) (f: ℝ → ℝ)
    (Hs: MeasurableSet s) (H: MeasureTheory.IntegrableOn f s):
    MeasureTheory.IntegrableOn (fun x => f (x + a)) ((fun x => x - a) '' s) := by
  have H1: MeasurableSet ((fun x => x - a) '' s) := by
    refine MeasurableSet.image_of_continuousOn_injOn Hs ?_ ?_
    . apply Continuous.continuousOn
      exact continuous_sub_right a
    . intros x Hx y Hy H2; simp at H2; exact H2
  rw [<- MeasureTheory.integrable_indicator_iff Hs] at H
  rw [<- MeasureTheory.integrable_indicator_iff H1]
  convert (MeasureTheory.Integrable.comp_add_right H a) using 1; ext x
  rw [<- Set.indicator_comp_right]
  unfold Function.comp Set.indicator Set.image Set.preimage; simp; split_ifs <;> rename_i H2 H3
  . rfl
  . exfalso; apply H3; obtain ⟨a1, H4, H5⟩ := H2
    have H6: a1 = x + a := by linarith
    subst a1; exact H4
  . exfalso; apply H2; use (x + a); simp [H3]
  . rfl

[Jireh Loreaux]

You're looking for docs#MeasureTheory.integrableOn_map_equiv

[Ilmārs Cīrulis]

Thank you!

[Ilmārs Cīrulis]

Woohoo, another lemma proven. I used so much time on it. :sweat_smile: :D
Was there some better way? :thinking:

theorem aux0 (a: ℝ) (s: Set ℝ) (f: ℝ → ℝ) (H: MeasurableSet s):
    ∫ (x: ℝ) in s, f x = ∫ (x: ℝ) in ((fun x => x - a) '' s), f (x + a) := by
  have H1: MeasurableSet ((fun x => x - a) '' s) :=
    MeasurableEmbedding.measurableSet_image' (measurableEmbedding_addRight (-a)) H
  rw [<- MeasureTheory.integral_indicator H, <- MeasureTheory.integral_indicator H1]
  unfold Set.indicator; simp
  rw [<- MeasureTheory.integral_add_right_eq_self _ a]
  congr; ext x; split_ifs <;> rename_i H3 H4
  . rfl
  . exfalso; apply H4; use (x + a); simpa
  . exfalso; apply H3; simp only [Set.mem_image] at H4
    obtain ⟨x_1, H4, H5⟩ := H4; subst x; ring_nf; exact H4
  . rfl

[Ruben Van de Velde]

import Mathlib
theorem aux0 (a: ℝ) (s: Set ℝ) (f: ℝ → ℝ) (H: MeasurableSet s):
    ∫ (x: ℝ) in s, f x = ∫ (x: ℝ) in ((fun x => x - a) '' s), f (x + a) := by
  rw [MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul
    (f' := fun _ => .id ℝ ℝ) _ H _ sub_left_injective.injOn]
  · simp
  · intro x hx
    exact (hasFDerivWithinAt_id _ _).sub_const a