Actual ordinary weak zero-gradient is AE constant

Samplinglib authored full-space analytic prerequisite toward PBPS conditional Poincare and separate SPHMC BL; not a quoted numbered theorem or full kernel equality/paper result.

Complete source statement (Samplinglib restatement)

A genuine locally-volume-integrable rough real function whose every legal C1 compact directional weak derivative is zero is volume-AE ONE real constant, including0.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual ordinary weak zero-gradient is AE constant

AutoSamplingTheory.TechnicalLemmas.Analysis.WeakGradientZero.ordinary_weak_zero_gradient_ae_constant · theorem · Teaching coverage

Read this first

Mathematical statement

A genuine locally-volume-integrable rough real function whose every legal C1 compact directional weak derivative is zero is volume-AE ONE real constant, including0.

\[\left[\forall\psi\in C_c^1(E),a\in E:\ \int_EuD_a\psi\,dx=0\right]\Longrightarrow\exists c\in\mathbb R:\ u=c\quad dx\text{-a.e.}\]

Lean statement · ordinary_weak_zero_gradient_ae_constant

A genuine locally-volume-integrable rough real function whose every legal C1 compact directional weak derivative is zero is volume-AE ONE real constant, including0.

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 ordinary_weak_zero_gradient_ae_constant
    (u : E → ℝ) (hu : LocallyIntegrable u)
    (hweak : ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => u x * fderiv ℝ ψ x a) volume ∧
      (∫ x, u x * fderiv ℝ ψ x a) = 0) :
    ∃ c : ℝ, u =ᵐ[volume] (fun _ => c)

Exact module and namespace context

Proof roadmap

1Differentiate the true compact convolution
For a genuine compact C1 kernel phi and rough locally-integrable u, the actual convolution has a genuine Frechet derivative, given by convolution with Dphi through the real scalar bilinear map. This is actual HasFDerivAt, not totalized fderiv zero alone.
2Use the translated legal weak test with the minus sign
For fixed x/a take psi(y)=phi(x-y). A true subtraction homeomorphism preserves compact support, and the genuine chain rule gives D_a psi(y)=-Dphi(x-y)[a]. The legal zero weak integral therefore kills the convolution derivative; convolution_flip/precompR identify the actual bilinear integral, with scalar multiplication order checked.
3Choose actual normalized shrinking compact bumps
Set inner radius1/(n+1), outer radius2/(n+1). Both radii are positive, the outer radius tends to0, and their ratio is exactly2. Genuine normalized ContDiffBump kernels give actual almost-everywhere convolution convergence for locally integrable u; no global volume integrability is used.
4Apply mean-value constancy to genuine differentiable mollifications
Each actual mollification is differentiable with zero derivative at EVERY point, hence constant on the full real vector space. The connected full-space domain matters: a disconnected/open-domain replacement would only give component-wise constants.
5Extract ONE constant by true AE convergence
Nonzero canonical Haar volume makes the AE convergence set nonempty. Fix x0 in that set. The SAME constant sequence at every other AE convergence point has limits u(x) and u(x0); uniqueness of limits yields ONE real c=u(x0). Dimension0 is included with no division by dimension or Nontrivial assumption. The focused nonzero7 test is locally integrable yet not globally volume integrable.

Full assumptions and notation

All objects and hypotheses

E is a full finite real Hilbert/Borel space with its canonical full-space volume, including dimension0; its vector-space connectedness and nonzero Haar volume are used. Real u is genuinely LocallyIntegrable against volume; it need not be globally volume integrable.
For EVERY real C1 compactly supported test psi and EVERY direction a, u(x)*D_a psi(x) is genuinely integrable against volume and its integral is0. No classical derivative of the rough u is assumed.

Mathematical proof

1. Differentiate the true compact convolution

For a genuine compact C1 kernel phi and rough locally-integrable u, the actual convolution has a genuine Frechet derivative, given by convolution with Dphi through the real scalar bilinear map. This is actual HasFDerivAt, not totalized fderiv zero alone.

\[D(\phi*u)(x)[a]=\int u(y)D\phi(x-y)[a]\,dy.\]

Corresponding Lean step

HasCompactSupport.hasFDerivAt_convolution_left; convolution_derivative_zero

2. Use the translated legal weak test with the minus sign

For fixed x/a take psi(y)=phi(x-y). A true subtraction homeomorphism preserves compact support, and the genuine chain rule gives D_a psi(y)=-Dphi(x-y)[a]. The legal zero weak integral therefore kills the convolution derivative; convolution_flip/precompR identify the actual bilinear integral, with scalar multiplication order checked.

\[\psi_{x}(y)=\phi(x-y),\quad D_a\psi_x(y)=-D\phi(x-y)[a],\quad D(\phi*u)(x)=0.\]

Corresponding Lean step

convolution_derivative_zero; convolution_flip; convolution_precompR_apply

3. Choose actual normalized shrinking compact bumps

Set inner radius1/(n+1), outer radius2/(n+1). Both radii are positive, the outer radius tends to0, and their ratio is exactly2. Genuine normalized ContDiffBump kernels give actual almost-everywhere convolution convergence for locally integrable u; no global volume integrability is used.

\[\rho_n: r_{in}=1/(n+1),\ r_{out}=2/(n+1),\quad\rho_n*u\to u\quad dx\text{-a.e.}\]

Corresponding Lean step

ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable; ordinary_weak_zero_gradient_ae_constant

4. Apply mean-value constancy to genuine differentiable mollifications

Each actual mollification is differentiable with zero derivative at EVERY point, hence constant on the full real vector space. The connected full-space domain matters: a disconnected/open-domain replacement would only give component-wise constants.

\[(\rho_n*u)(x)=(\rho_n*u)(x_0)\quad\forall n,x,x_0.\]

Corresponding Lean step

is_const_of_fderiv_eq_zero; convolution_derivative_zero

5. Extract ONE constant by true AE convergence

Nonzero canonical Haar volume makes the AE convergence set nonempty. Fix x0 in that set. The SAME constant sequence at every other AE convergence point has limits u(x) and u(x0); uniqueness of limits yields ONE real c=u(x0). Dimension0 is included with no division by dimension or Nontrivial assumption. The focused nonzero7 test is locally integrable yet not globally volume integrable.

\[c=u(x_0),\qquad u(x)=c\quad dx\text{-a.e.}\]

Corresponding Lean step

Filter.Eventually.exists; tendsto_nhds_unique; Tests.WeakGradientZeroKernel.actual_noncompact_seven_weak_zero

Lean verification

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

Lean proof · ordinary_weak_zero_gradient_ae_constant

Differentiate the true compact convolution; Use the translated legal weak test with the minus sign; Choose actual normalized shrinking compact bumps; Apply mean-value constancy to genuine differentiable mollifications; Extract ONE constant by true AE convergence

Download module (.lean)

theorem ordinary_weak_zero_gradient_ae_constant
    (u : E → ℝ) (hu : LocallyIntegrable u)
    (hweak : ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => u x * fderiv ℝ ψ x a) volume ∧
      (∫ x, u x * fderiv ℝ ψ x a) = 0) :
    ∃ c : ℝ, u =ᵐ[volume] (fun _ => c) := by
  classical
  let ρ : ℕ → ContDiffBump (0 : E) := fun n =>
    {rIn := 1/((n:ℝ)+1), rOut := 2/((n:ℝ)+1),
      rIn_pos := by positivity,
      rIn_lt_rOut := by apply div_lt_div_of_pos_right (by norm_num) (by positivity)}
  have hρ : Tendsto (fun n => (ρ n).rOut) atTop (𝓝 0) :=
    (tendsto_atTop_add_const_right atTop (1:ℝ) tendsto_natCast_atTop_atTop).const_div_atTop 2
  have hratio : ∀ n, (ρ n).rOut ≤ 2*(ρ n).rIn := by intro n; dsimp [ρ]; field_simp; norm_num
  have ht := ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable
    (μ := (volume : Measure E)) hρ (Eventually.of_forall hratio) hu
  obtain ⟨x0,hx0⟩ := ht.exists
  refine ⟨u x0,?_⟩
  filter_upwards [ht] with x hx
  have he (n : ℕ) : ((ρ n).normed volume ⋆[lsmul ℝ ℝ] u) x =
      ((ρ n).normed volume ⋆[lsmul ℝ ℝ] u) x0 := by
    apply is_const_of_fderiv_eq_zero (𝕜 := ℝ)
    · intro y
      exact (convolution_derivative_zero u _ hu
        (contDiff_infty.mp (ρ n).contDiff_normed 1) (ρ n).hasCompactSupport_normed hweak y).differentiableAt
    · intro y
      exact (convolution_derivative_zero u _ hu
        (contDiff_infty.mp (ρ n).contDiff_normed 1) (ρ n).hasCompactSupport_normed hweak y).fderiv
  exact tendsto_nhds_unique hx ((tendsto_congr he).mpr hx0)

end AutoSamplingTheory.TechnicalLemmas.Analysis.WeakGradientZero

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source full-space reflected conditional gradient/Poincare route.	E is a full finite real Hilbert/Borel space with its canonical full-space volume, including dimension0; its vector-space connectedness and nonzero Haar volume are used. Real u is genuinely LocallyIntegrable against volume; it need not be globally volume integrable. For EVERY real C1 compactly supported test psi and EVERY direction a, u(x)*D_a psi(x) is genuinely integrable against volume and its integral is0. No classical derivative of the rough u is assumed.	generalization	Ordinary weak and generic C1 Gibbs prerequisite stated explicitly; source C2/curvature/eta/reflected law kept in the actual consumer, including0.
AppendixC.1 omits the actual ordinary weak-gradient-zero constant prerequisite and AE operator connection.	A genuine locally-volume-integrable rough real function whose every legal C1 compact directional weak derivative is zero is volume-AE ONE real constant, including0.	source-implicit	Derive true mollification/differentiability/AE constancy, then same-original distributional graph and correct BOTH AE transfers; no classical derivative of rough u or global-volume-L1 premise.
Full kernel equality, constants-domain, centered residual/Poincare/BL/main/composition.	Full finite real Hilbert/Borel E including0 and actual full-space volume. Genuine locally-volume-L1 u, all C1 compact directional tests with legal integrable products and zero weak derivative imply ONE real constant volume-AE. Actual normalized Gibbs W C1/exp(-W) integrable, SAME original exact compact-smooth graph D and closability give closed-gradient-zero implies weighted-AE constant. Actual PBPS common Gaussian J/R/S and original dense D_y precede ALL closure-domain u; source C2 curvature/eta cap/positive partitions retained but no additional curvature is needed by the generic kernel leaf. Only one direction; constants-domain converse, full kernel equality, centered residual/epsilon0/range/Poincare/BL/core and both main/composition remain open. No global-volume integrability of constants, classical differentiability of rough u, Nontrivial E, final kernel certificate, spectral gap or joint fiber selector. TV never transfers unbounded cost.	unresolved	Only zero closed gradient implies AE constant; reverse domain and later analytic/paper conclusions remain separate.

Full finite real Hilbert/Borel E including0 and actual full-space volume. Genuine locally-volume-L1 u, all C1 compact directional tests with legal integrable products and zero weak derivative imply ONE real constant volume-AE. Actual normalized Gibbs W C1/exp(-W) integrable, SAME original exact compact-smooth graph D and closability give closed-gradient-zero implies weighted-AE constant. Actual PBPS common Gaussian J/R/S and original dense D_y precede ALL closure-domain u; source C2 curvature/eta cap/positive partitions retained but no additional curvature is needed by the generic kernel leaf. Only one direction; constants-domain converse, full kernel equality, centered residual/epsilon0/range/Poincare/BL/core and both main/composition remain open. No global-volume integrability of constants, classical differentiability of rough u, Nontrivial E, final kernel certificate, spectral gap or joint fiber selector. TV never transfers unbounded cost.

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

Full finite real Hilbert/Borel E including0 and actual full-space volume. Genuine locally-volume-L1 u, all C1 compact directional tests with legal integrable products and zero weak derivative imply ONE real constant volume-AE. Actual normalized Gibbs W C1/exp(-W) integrable, SAME original exact compact-smooth graph D and closability give closed-gradient-zero implies weighted-AE constant. Actual PBPS common Gaussian J/R/S and original dense D_y precede ALL closure-domain u; source C2 curvature/eta cap/positive partitions retained but no additional curvature is needed by the generic kernel leaf. Only one direction; constants-domain converse, full kernel equality, centered residual/epsilon0/range/Poincare/BL/core and both main/composition remain open. No global-volume integrability of constants, classical differentiability of rough u, Nontrivial E, final kernel certificate, spectral gap or joint fiber selector. TV never transfers unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasCompactSupport.hasFDerivAt_convolution_left
convolution_flip
convolution_precompR_apply
ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable
is_const_of_fderiv_eq_zero
Filter.Eventually.exists
tendsto_nhds_unique

Mathematical sources

PBPS AppendixC.1 authored analytic prerequisite — Full finite real Hilbert/Borel E including0 and actual full-space volume. Genuine locally-volume-L1 u, all C1 compact directional tests with legal integrable products and zero weak derivative imply ONE real constant volume-AE. Actual normalized Gibbs W C1/exp(-W) integrable, SAME original exact compact-smooth graph D and closability give closed-gradient-zero implies weighted-AE constant. Actual PBPS common Gaussian J/R/S and original dense D_y precede ALL closure-domain u; source C2 curvature/eta cap/positive partitions retained but no additional curvature is needed by the generic kernel leaf. Only one direction; constants-domain converse, full kernel equality, centered residual/epsilon0/range/Poincare/BL/core and both main/composition remain open. No global-volume integrability of constants, classical differentiability of rough u, Nontrivial E, final kernel certificate, spectral gap or joint fiber selector. TV never transfers unbounded cost.

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

Actual ordinary weak zero-gradient is AE constant

Complete source statement (Samplinglib restatement)

Actual ordinary weak zero-gradient is AE constant

Read the formalized proofs

Actual ordinary weak zero-gradient is AE constant

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Differentiate the true compact convolution

2. Use the translated legal weak test with the minus sign

3. Choose actual normalized shrinking compact bumps

4. Apply mean-value constancy to genuine differentiable mollifications

5. Extract ONE constant by true AE convergence

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?