Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

WeakGradientZero: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual ordinary weak zero-gradient is AE constant
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

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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

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) := 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

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.