Almost-everywhere equality does not determine classical gradients
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence.not_gradient_ae_congr_for_arbitrary_measure · theorem · Teaching coverage
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.
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.
theorem not_gradient_ae_congr_for_arbitrary_measure :
¬ ∀ (μ : Measure ℝ) (f g : ℝ → ℝ),
f =ᵐ[μ] g → ∀ᵐ x ∂μ, gradient f x = gradient g xProof 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.
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.
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.
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.
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.
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.GradientAECongruenceSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Lee--Shen--Tian differentiate an explicit pointwise smooth normalized log-density ratio and obtain (y-y')/eta. | Mathlib's llr is a specific Radon--Nikodym-based function, but its available identification with the explicit smooth ratio is only almost everywhere; the bound theorem rules out using that fact alone to transport classical gradients. | API-limitation | Classical derivatives depend on local pointwise behavior, not only on a measure-theoretic equivalence class. |
Rules out one unsound canonical-score adapter only; no SPHMC analytic conclusion is promoted.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.