Calculus counterexamples

Stream: Is there code for X?

[Snir Broshi]

Well known (undergrad) counterexamples in calculus/analysis:

• Weierstrass function
• Dirichlet function
• Thomae's function
• Volterra's function
• Cantor function
• Non-analytic smooth function
• Fabius function
• Conway's base 13 function

[Snir Broshi]

IMO these are a bit tedious to define and prove properties about, but not having them seems weird, like not having TopologistsSineCurve

[Weiyi Wang]

I was just thinking about writing Weierstrass function for fun yesterday

[Yongxi Lin (Aaron)]

I do want to see a proof of * Non-analytic smooth function, as I used the function listed in the wikipedia page in my tychonoff example: #mathlib4 > Tychonov's Counterexample for the Heat Equation

[Michael Rothgang]

@Moritz Doll Could/should this be added to the list of undergrad topics on github?

[Moritz Doll]

I think the undergrad list was compiled by @Patrick Massot from the French curriculum, so I don't think we should add anything to it. On the other hand I think we should at some point start to think how to better organise "well-known" theorems, one idea that was thrown around was to have 2-way book mathlib references (i.e., in a mathlib theorem a reference to that theorem in Bourbaki and a list of the theorems in Bourbaki and how they are formalised in mathlib), but maybe the people at MI have some better idea.

[Moritz Doll]

Btw we have the bump function in mathlib and of course every smooth compactly supported function is not analytic. Or is the question specifically about $e^{-1/x}$? Might also be there, but I am not sure

[Moritz Doll]

Here is a very tangible undergrad project: get a copy of "counterexamples in analysis" and formalise your favourite example from there

[Kenny Lau]

I would assume that you would need some function like that to construct any bump function in the first place

[Kenny Lau]

aha, found the function Real.smoothTransition after like 1000 layers of abstraction

[Kenny Lau]

image.png

[Kenny Lau]

which uses exp(-1/x) which is called expNegInvGlue

[Kenny Lau]

so it only remains to show that this function is not analytic at 0

[Moritz Doll]

Created an issue: #31209

[Snir Broshi]

Moritz Doll said:

Btw we have the bump function in mathlib and of course every smooth compactly supported function is not analytic. Or is the question specifically about $e^{-1/x}$? Might also be there, but I am not sure

Non-analytic at a point is also a good counterexample but I was referring to the smooth but analytic-nowhere example

[Weiyi Wang]

I just had some fun with Weierstrass function at #31954. If we want to have this in mathlib, does the original loose bound (1 + 3/2*pi < a * b) by Weierstrass with short proof suffice (as written in the draft PR), or we want to have Hardy's sharp bound (1 ≤ a * b) with longer proof?

[metakuntyyy]

I proved something related to filters about Dirichlet's function.

import Mathlib

open Classical in
noncomputable def dirichletFunc : ℝ → ℝ :=
  fun x => if Irrational x then 0 else 1


open Classical in
example (x:ℝ) : Filter.map dirichletFunc (nhds x) = Filter.principal {0,1}:= by
  ext y
  simp only [Filter.mem_map,
    Metric.mem_nhds_iff,Real.ball_eq_Ioo]
  simp[Filter.mem_principal]

  have ara : dirichletFunc = fun x =>if Irrational x then 0 else 1 := rfl
  rw[ara]
  constructor
  · intro haa
    have ⟨ a, ⟨ ha, hb ⟩ ⟩ :=haa
    clear haa

    have ⟨ eh, ⟨ el, hexir⟩⟩  : ∃ r ∈ Set.Ioo (x-a) (x+a), Irrational r :=by
      rw[Set.Ioo]
      simp only [Set.mem_setOf_eq]
      have hh : x-a < x+a := by grind
      have dd := exists_irrational_btwn hh
      grind
    have ⟨ eh2, ⟨ el2, hexr⟩⟩  : ∃ r ∈ Set.Ioo (x-a) (x+a), ¬ Irrational r := by
      rw[Set.Ioo]
      simp only [Set.mem_setOf_eq]
      have hh : x-a < x+a := by grind
      have ⟨ dd, hdd⟩  := exists_rat_btwn hh
      use dd
      simp
      grind
    rw[← Set.image_subset_iff] at hb
    have y0 : 0 ∈ y :=by grind
    have y0 : 1 ∈ y :=by grind
    grind
  · intro h
    use 1
    simp only [zero_lt_one, true_and]
    apply Set.Subset.trans (b:=Set.univ) (by grind)
    simp
    apply Set.Subset.trans ?_ h
    apply Eq.subset
    ext dd
    simp only [Set.mem_range, Set.mem_insert_iff, Set.mem_singleton_iff]
    constructor
    · intro hb
      have ⟨ bb, hbb ⟩ := hb
      by_cases hs: Irrational bb
      repeat grind
    · intro hc
      apply Or.elim hc
      · intro hir
        use Real.sqrt 2
        have hirr := irrational_sqrt_two
        grind
      · intro h0
        use 0
        rw[h0]
        simp

[Snir Broshi]

metakuntyyy said:

import Mathlib

open Classical in
noncomputable def dirichletFunc : ℝ → ℝ :=
  fun x => if Irrational x then 0 else 1

Not sure if this is better but you can avoid open Classical and a double negative and instead lean into Dirichlet being an indicator function:

import Mathlib

noncomputable def dirichletFunc : ℝ → ℝ :=
  Set.range ((↑) : ℚ → ℝ) |>.indicator 1

[metakuntyyy]

I think your suggestion is better. The open Classical annoyed me anyways.

[Weiyi Wang]

:partying_face: The nowhere differentiable Weierstrass function is now at https://leanprover-community.github.io/mathlib4_docs/Counterexamples/NowhereDifferentiable.html . I don't plan to touch anything else on the list any time soon, but I think these all will be fun small project, whether we get them in mathlib or not

[Weiyi Wang]

:upside_down: and I just realized there is a broken doc string