Samplinglib mathematical lesson

Same original Gibbs closed-gradient zero implies AE constant

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant · theorem · Teaching coverage

Read this first

Mathematical statement

For the SAME original Gibbs compact-gradient closure, EVERY domain element u with D.closure u=0 is weighted-AE ONE real constant. This is only one direction; constant-domain membership and full kernel equality are not asserted.

\[\forall u\in\operatorname{dom}\overline D,\quad\overline Du=0\Longrightarrow\exists c\in\mathbb R:\ u=c\quad\mu\text{-a.e.},\qquad\mu=Z^{-1}e^{-W}dx.\]

Lean statement · closed_gradient_zero_ae_constant

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 closed_gradient_zero_ae_constant (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ u : D.closure.domain, D.closure u = 0 →
        ∃ c : ℝ, (u : Lp ℝ 2 μ) =ᵐ[μ] (fun _ => c)

Exact module and namespace context

Proof roadmap

1Keep the SAME original closure graph and its actual representatives
Apply the accepted ordinary distributional theorem to (u,D.closure u) in the SAME original graph. It derives true local-volume integrability and legal C1 compact directional products/weak identity; no rough differentiability or final kernel characterization is supplied.
2Transfer the actual zero vector class in the correct direction
D.closure u=0 gives its actual AE representative zero under mu. Genuine exp(-W) integrability and strictly positive normalized density imply volume<<mu, so zero also holds volume-AE. The reverse absolute-continuity direction would not justify this step.
3Derive the legal ordinary zero weak derivative and one constant
Use actual integral congruence to turn the left weak-gradient integral into0, retaining the right product integrability. Apply the new ordinary weak-zero-gradient leaf to derive volume-AE ONE constant for this same u.
4Transfer constancy back to the actual Gibbs law and keep the one-way boundary
Since mu<<volume, the very same constant representative is mu-AE. This does not put constants into the original closure domain, identify the full kernel/range, prove centering/residual convergence, Poincare/BL or a paper main result.

Full assumptions and notation

All objects and hypotheses

Full finite real Hilbert/Borel E including0; W is C1 and exp(-W) is genuinely integrable. mu is exactly the normalized volume.tilted(-W) Gibbs probability, whose density is positive. No curvature or spectral gap is assumed.
Fix SAME original weighted-L2 real partial-linear gradient D with exact compact-C-infinity genuine gradient graph and closability before ALL u in D.closure.domain. Each queried u satisfies D.closure u=0 as an actual vector L2 class, not a pointwise derivative assertion or final kernel certificate.

Mathematical proof

1. Keep the SAME original closure graph and its actual representatives

Apply the accepted ordinary distributional theorem to (u,D.closure u) in the SAME original graph. It derives true local-volume integrability and legal C1 compact directional products/weak identity; no rough differentiability or final kernel characterization is supplied.

\[\int\psi\langle\overline Du,a\rangle dx=-\int uD_a\psi\,dx.\]

Corresponding Lean step

WeightedGradientDistribution.closed_gradient_distributional; LinearPMap.mem_graph

2. Transfer the actual zero vector class in the correct direction

D.closure u=0 gives its actual AE representative zero under mu. Genuine exp(-W) integrability and strictly positive normalized density imply volume<<mu, so zero also holds volume-AE. The reverse absolute-continuity direction would not justify this step.

\[dx\ll\mu,\quad\overline Du=0\ \mu\text{-a.e.}\Longrightarrow\overline Du=0\ dx\text{-a.e.}\]

Corresponding Lean step

absolutelyContinuous_tilted; Measure.AbsolutelyContinuous.ae_eq; Lp.coeFn_zero

3. Derive the legal ordinary zero weak derivative and one constant

Use actual integral congruence to turn the left weak-gradient integral into0, retaining the right product integrability. Apply the new ordinary weak-zero-gradient leaf to derive volume-AE ONE constant for this same u.

\[\int uD_a\psi\,dx=0\quad\forall\psi,a\Longrightarrow\exists c:\ u=c\ dx\text{-a.e.}\]

Corresponding Lean step

WeakGradientZero.ordinary_weak_zero_gradient_ae_constant; closed_gradient_zero_ae_constant

4. Transfer constancy back to the actual Gibbs law and keep the one-way boundary

Since mu<<volume, the very same constant representative is mu-AE. This does not put constants into the original closure domain, identify the full kernel/range, prove centering/residual convergence, Poincare/BL or a paper main result.

\[\mu\ll dx,\quad u=c\ dx\text{-a.e.}\Longrightarrow u=c\ \mu\text{-a.e.}\]

Corresponding Lean step

tilted_absolutelyContinuous; Measure.AbsolutelyContinuous.ae_eq; closed_gradient_zero_ae_constant

Lean verification

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

Lean proof · closed_gradient_zero_ae_constant

Keep the SAME original closure graph and its actual representatives; Transfer the actual zero vector class in the correct direction; Derive the legal ordinary zero weak derivative and one constant; Transfer constancy back to the actual Gibbs law and keep the one-way boundary

Download module (.lean)

theorem closed_gradient_zero_ae_constant (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ u : D.closure.domain, D.closure u = 0 →
        ∃ c : ℝ, (u : Lp ℝ 2 μ) =ᵐ[μ] (fun _ => c) := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph u hz
  obtain ⟨hu,hG,hweak⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientDistribution.closed_gradient_distributional
      W hW hI D hD hgraph (u : Lp ℝ 2 μ) (D.closure u) (D.closure.mem_graph u)
  have hzero : (fun x => D.closure u x) =ᵐ[μ] (fun _ => (0:E)) := by
    rw [hz]
    exact Lp.coeFn_zero E 2 μ
  have hvol : (fun x => D.closure u x) =ᵐ[volume] (fun _ => (0:E)) :=
    (absolutelyContinuous_tilted hI).ae_eq hzero
  obtain ⟨c,hc⟩ := AutoSamplingTheory.TechnicalLemmas.Analysis.WeakGradientZero.ordinary_weak_zero_gradient_ae_constant (fun x => (u : Lp ℝ 2 μ) x) hu (by
    intro ψ hψ hψc a
    obtain ⟨hi,hj,he⟩ := hweak ψ hψ hψc a
    refine ⟨hj,?_⟩
    have he0 : (∫ x, ψ x * inner ℝ (D.closure u x) a) = 0 := by
      calc
        _ = ∫ x : E, (0:ℝ) := integral_congr_ae (by
          filter_upwards [hvol] with x hx
          simp [hx])
        _ = 0 := by simp
    rw [he0] at he
    linarith)
  exact ⟨c,(tilted_absolutelyContinuous (volume : Measure E) (fun x => -W x)).ae_eq hc⟩

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel

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)

LinearPMap.mem_graph
absolutelyContinuous_tilted
tilted_absolutelyContinuous
Measure.AbsolutelyContinuous.ae_eq
Lp.coeFn_zero
integral_congr_ae

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.