Blogging my result / experience as a noob

Stream: general

[Dominic Steinitz]

I finally finished my proof that the derivative of a function $f : M \longrightarrow \mathbb{R}$ being 0 ($df = 0$) is co-ordinate independent. I thought I would write it up as a blog. After a bit of faff, I am reasonably happy with the layout (although the syntax could do with some better highlighting).

If I load up the file in emacs, I was hoping that the sections beginning with ```lean4 would be "runnable" somehow. So question 1: is this possible?

If I load up the file in VS then same question (so question 2).

Here's an example bit of the source .md file (it's written in markdown).

Many thanks

---

date: 2024-12-23
title: Vanishing Derivatives

---

Suppose we have smooth $f : M \longrightarrow \mathbb{R}$.

$$
g=f \varphi_\alpha^{-1}=f \varphi_\beta^{-1} \varphi_\beta \varphi_\alpha^{-1}=h \varphi_\beta \varphi_\alpha^{-1}
$$

Transition Maps are Smooth

$$
g=f \varphi_\alpha^{-1}=f \varphi_\beta^{-1} \varphi_\beta \varphi_\alpha^{-1}=h \varphi_\beta \varphi_\alpha^{-1}
$$

import Mathlib.Geometry.Manifold.MFDeriv.Defs
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Geometry.Manifold.AnalyticManifold
import Mathlib.Geometry.Manifold.ContMDiff.Atlas
import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

open Manifold

open SmoothManifoldWithCorners

theorem mfderivWithin_congr_of_eq_on_open
  {m n : ℕ} {M N : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]
  [TopologicalSpace N]
  [ChartedSpace (EuclideanSpace ℝ (Fin n)) N]
  [SmoothManifoldWithCorners (𝓡 n) N]
  (f g : M → N) (s : Set M)
  (ho : IsOpen s)
  (he : ∀ x ∈ s, f x = g x) :
  ∀ x ∈ s, mfderivWithin (𝓡 m) (𝓡 n) f s x = mfderivWithin (𝓡 m) (𝓡 n) g s x := by
    intros x hy
    exact mfderivWithin_congr (IsOpen.uniqueMDiffWithinAt ho hy) he (he x hy)

[Mauricio Collares]

You might want to take a look at https://github.com/leanprover/verso, more specifically an example such as https://github.com/leanprover/verso/blob/main/examples/website/DemoSite/Blog/Conditionals.lean

[Mauricio Collares]

(But it would be nice to have native org-mode support for lean4!)