Samplinglib mathematical lesson

Almost-everywhere equality does not determine classical gradients

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence.not_gradient_ae_congr_for_arbitrary_measure · theorem · Teaching coverage

Read this first

Mathematical statement

It is false that, for every measure mu and every two real functions f and g, f=g mu-almost everywhere forces their classical Mathlib gradients to agree mu-almost everywhere.

\[\neg\,\forall \mu,f,g,\quad f=g\ \mu\text{-a.e.}\Longrightarrow \nabla f=\nabla g\ \mu\text{-a.e.}\]

Lean statement · not_gradient_ae_congr_for_arbitrary_measure

The theorem negates a universal implication over all real measures and all pairs of real functions. It uses an explicit Dirac counterexample rather than an axiom or meta-level warning.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem not_gradient_ae_congr_for_arbitrary_measure :
    ¬ ∀ (μ : Measure ℝ) (f g : ℝ → ℝ),
      f =ᵐ[μ] g → ∀ᵐ x ∂μ, gradient f x = gradient g x

Exact module and namespace context

Proof roadmap

1Choose two representatives that agree at the atom
Let mu be the Dirac measure at zero, f be the zero function, and g(x)=x. Almost-everywhere equality for a Dirac measure means equality at its atom, where both functions have value zero.
2Compute the two classical gradients
The zero function has gradient zero. The identity function has derivative and hence gradient one at zero.
3Contradict the proposed a.e. gradient congruence
If the unrestricted rule existed, applying it to these representatives would force 0=1 at the atom, a contradiction.

Full assumptions and notation

All objects and hypotheses

No regularity assumptions are imposed because the statement refutes an unrestricted congruence rule.
The counterexample uses the Dirac probability measure at zero.
The gradients are Mathlib's total classical gradients, not Sobolev weak gradients.

Mathematical proof

1. Choose two representatives that agree at the atom

Let mu be the Dirac measure at zero, f be the zero function, and g(x)=x. Almost-everywhere equality for a Dirac measure means equality at its atom, where both functions have value zero.

\[\mu=\delta_0,\qquad f(x)=0,\qquad g(x)=x,\qquad f(0)=g(0)=0.\]

Corresponding Lean step

The proof rewrites the a.e. filter with ae_dirac_eq.

2. Compute the two classical gradients

The zero function has gradient zero. The identity function has derivative and hence gradient one at zero.

\[\nabla f(0)=0,\qquad \nabla g(0)=1.\]

Corresponding Lean step

gradient_fun_const and hasDerivAt_id.hasGradientAt.gradient provide the two computations.

3. Contradict the proposed a.e. gradient congruence

If the unrestricted rule existed, applying it to these representatives would force 0=1 at the atom, a contradiction.

\[f=g\ \delta_0\text{-a.e.}\quad\text{but}\quad\nabla f\ne\nabla g\ \delta_0\text{-a.e.}\]

Corresponding Lean step

The claimed gradient a.e. equality is again reduced to its value at zero with ae_dirac_eq.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · not_gradient_ae_congr_for_arbitrary_measure

Instantiate the universal rule with delta_0, the zero function and the identity; reduce both a.e. propositions to the atom and compute the two gradients.

Download module (.lean)

theorem not_gradient_ae_congr_for_arbitrary_measure :
    ¬ ∀ (μ : Measure ℝ) (f g : ℝ → ℝ),
      f =ᵐ[μ] g → ∀ᵐ x ∂μ, gradient f x = gradient g x := by
  intro h
  let f : ℝ → ℝ := fun _ => 0
  let g : ℝ → ℝ := fun x => x
  have hfg : f =ᵐ[Measure.dirac 0] g := by
    rw [ae_dirac_eq]
    rfl
  have hgrad := h (Measure.dirac 0) f g hfg
  have hgrad0 : gradient f 0 = gradient g 0 := by
    rw [ae_dirac_eq] at hgrad
    exact hgrad
  have hf0 : gradient f 0 = 0 := by
    simp [f]
  have hg0 : gradient g 0 = 1 := by
    exact (hasDerivAt_id (𝕜 := ℝ) 0).hasGradientAt.gradient
  rw [hf0, hg0] at hgrad0
  norm_num at hgrad0

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem does not say the paper's explicit smooth score calculation is invalid.
It does not say Mathlib's particular llr has an incorrect gradient.
It does not rule out a full-support or absolutely-continuous result under added regularity, gradient transport from pointwise/local equality, an RGO-specific adapter, or Sobolev weak gradients.
It does not prove LSI, T2, Fisher evaluation, Wasserstein contraction or a main result.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.ae_dirac_eq
gradient_fun_const
hasDerivAt_id
HasDerivAt.hasGradientAt

Mathematical sources

Chen, Chewi, Lu and Zhang, SPHMC v1, Lemma 4.17 — The lemma states the restricted-Gaussian contraction and cites the prior relative-score proof; the obstruction concerns only the formal representative adapter.
Lee, Shen and Tian, Lemma 2, equation (11) — Direct source for differentiating the explicit normalized density ratio and obtaining the affine score (y-y')/eta.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.