Help Needed: Proving Smoothness of a Bump Function in Lean

Stream: maths

[Travis Morphy]

Hi everyone,

I’m currently working on formalizing aspects of the calculus of variations in Lean, specifically focusing on the Fundamental Lemma of the Calculus of Variations. A key part of this involves proving that a certain bump function is -smooth. Here’s the Lean code I’m dealing with:

import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Data.Complex.Exponential

open Set

example (t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) (x : Ioo t₀ t₁) (δ : ℝ)
  (hδ : δ = (min (x - t₀) (t₁ - x)) / 2) (posδ : δ > 0)
  (a : ℝ) (ha : a = x - δ) (b : ℝ) (hb : b = x + δ)
  (g : ℝ → ℝ) (hg : g = fun t => if t ∈ Ioo a b then Real.exp (1 / ((t - a) * (t - b))) else 0) :
  ContDiffOn ℝ 2 g (Icc t₀ t₁) :=
by
  sorry

I’ve tried several approaches to prove the smoothness of the function g, including:

• Decomposing g into a composition of functions.

• Proving the smoothness pointwise.

• Utilizing the fun_prop tactic.

Unfortunately, none of these attempts have been successful. I’m now considering expressing g as the product of two transition functions, whose smoothness properties are established in Lean’s mathlib, as detailed here. However, this approach seems quite complex.

Given that establishing the smoothness of g is relatively straightforward mathematically, I’m concerned that I might be overlooking a simpler method. I would greatly appreciate any guidance or suggestions on how to approach this proof in Lean. If anyone is interested in experimenting with the code, it can be run locally on any computer.

Thank you for your time and assistance.

[Sébastien Gouëzel]

Not answering your question directly, but we already have the fundamental lemma you're mentioning, if I understand correctly, under the name docs#IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero
The proof uses a bump function, of course. It is not defined exactly as yours, but the specifics of the definition are certainly irrelevant. If you want to do your own proof, you could start from docs#Real.smoothTransition and/or see how this one is used to define smooth bump functions in docs#ContDiffBumpBase.ofInnerProductSpace

[Travis Morphy]

Thank you for this!