Samplinglib mathematical lesson

Actual constants in original closed-gradient domain

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradient · theorem · Teaching coverage

Read this first

Mathematical statement

For EVERY real c, produce u in SAME original D.closure.domain whose actual representative is mu-AE constant c and whose actual vector output is0.

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

Lean statement · constants_in_closed_gradient

For EVERY real c, produce u in SAME original D.closure.domain whose actual representative is mu-AE constant c and whose actual vector output is0.

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 constants_in_closed_gradient (μ : Measure E) [IsFiniteMeasure μ]
    (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ) (hD : D.IsClosable)
    (hgraph : ∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
      ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
        a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) (c : ℝ) :
    ∃ u : D.closure.domain, (u : Lp ℝ 2 μ) =ᵐ[μ] (fun _ => c) ∧ D.closure u=0

Exact module and namespace context

Proof roadmap

1Construct actual constant scalar and zero-gradient classes
Finite mu gives the scalar constant MemLp. Actual Frechet derivative of the C1 constant function is0, hence its genuine gradient is0 and vector MemLp. No ordinary-global L1 premise is used.
2Apply the new weighted C1 graph producer
Use the SAME original D and exact closable graph, with the actual constant scalar/vector classes. True graph membership is derived through cutoff approximation; a constant-domain certificate is not supplied.
3Recover the actual partial-operator domain witness
Use actual mem_graph_iff to obtain an element u of SAME D.closure.domain with the constant scalar class and zero output. Its actual AE representative is inherited from MemLp.toLp. This does not infer a spectral gap.

Full assumptions and notation

All objects and hypotheses

Full finite real Hilbert/Borel E including dimension0. Fix SAME original real weighted-L2 partial-linear gradient D with exact compact-C-infinity genuine gradient graph and closability BEFORE all queried functions or classes.
Actual finite mu and EVERY real constant c; scalar constant and genuine zero vector gradient are L2 by finite measure. No global ordinary-volume integrability or spatial moment is required.

Mathematical proof

1. Construct actual constant scalar and zero-gradient classes

Finite mu gives the scalar constant MemLp. Actual Frechet derivative of the C1 constant function is0, hence its genuine gradient is0 and vector MemLp. No ordinary-global L1 premise is used.

\[f(x)=c,\quad\nabla f(x)=0,\quad f,\nabla f\in L^2(\mu).\]

Corresponding Lean step

memLp_const; fderiv_const_apply; constants_in_closed_gradient

2. Apply the new weighted C1 graph producer

Use the SAME original D and exact closable graph, with the actual constant scalar/vector classes. True graph membership is derived through cutoff approximation; a constant-domain certificate is not supplied.

\[([c],0)\in\operatorname{graph}\overline D.\]

Corresponding Lean step

WeightedC1GradientDomain.c1_in_closed_gradient; Lp.ext

3. Recover the actual partial-operator domain witness

Use actual mem_graph_iff to obtain an element u of SAME D.closure.domain with the constant scalar class and zero output. Its actual AE representative is inherited from MemLp.toLp. This does not infer a spectral gap.

\[\exists u\in\operatorname{dom}\overline D:\ u=c\ \mu\text{-a.e.},\ \overline Du=0.\]

Corresponding Lean step

LinearPMap.mem_graph_iff; MemLp.coeFn_toLp; constants_in_closed_gradient

Lean verification

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

Lean proof · constants_in_closed_gradient

Construct actual constant scalar and zero-gradient classes; Apply the new weighted C1 graph producer; Recover the actual partial-operator domain witness

Download module (.lean)

theorem constants_in_closed_gradient (μ : Measure E) [IsFiniteMeasure μ]
    (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ) (hD : D.IsClosable)
    (hgraph : ∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
      ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
        a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) (c : ℝ) :
    ∃ u : D.closure.domain, (u : Lp ℝ 2 μ) =ᵐ[μ] (fun _ => c) ∧ D.closure u=0 := by
  have hp : MemLp (fun _ : E => c) 2 μ := memLp_const c
  have hg : gradient (fun _ : E => c) = (fun _ => (0:E)) := by
    funext x
    simp [gradient,fderiv_const_apply]
  have hq : MemLp (gradient (fun _ : E => c)) 2 μ := by rw [hg]; exact memLp_const (0:E)
  have hm := c1_in_closed_gradient μ D hD hgraph contDiff_const hp hq
  have hz : hq.toLp (gradient (fun _ : E => c)) = 0 := by
    apply Lp.ext
    filter_upwards [hq.coeFn_toLp,Lp.coeFn_zero (E:=E) (p:=2) (μ:=μ)] with x hx hy
    rw [hx,hy,hg]; rfl
  rw [hz] at hm
  obtain ⟨u,hu,huz⟩ := (D.closure.mem_graph_iff).mp hm
  refine ⟨u,?_,huz⟩
  rw [hu]
  exact hp.coeFn_toLp



end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain

Exact module and namespace context

Scope and omitted-condition boundaries

Actual finite real Hilbert/Borel E including0. Fix actual finite mu and SAME original closable exact compact-C-infinity gradient D BEFORE ALL C1 f with actual MemLp f2mu and MemLp gradientf2mu. Genuine smooth cutoff exhaustion/derivative-product/weighted L2 limits put actual class pair into SAME closure graph, without compact support or extra spatial moment. Finite mu constants are genuinely in original closure domain with outputzero. For actual C1 Gibbs W/exp(-W) integrable, combine actual constants-domain with accepted one-way implication for full zero-output iff AEconstant on SAME D. Actual PBPS common Gaussian J/R/S/Sdensity/positive partitions/sourceC2 alpha beta eta cap and original D_y beforeALL constants/u/directions; real unnormalized y-score C1/L2/boundedgradient from accepted score producer transfers along ONLY explicit reflected density equality S2_y=S_y and enters SAME original closed graph. No R2=R or alternateD equality, global ordinary L1, C-infinity potential, gradient of rough representative, Nontrivial E, spatial moment, supplied domain/fullkernel/spectralgap/Poincare certificate, epsilon0/range/centering/measurablejointselector/core/BL/main/composition. TV never transfers unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.c1_in_closed_gradient

Mathlib API called (external library)

memLp_const
fderiv_const_apply
LinearPMap.mem_graph_iff
MemLp.coeFn_toLp

Mathematical sources

PBPS AppC1 authored original-gradient domain prerequisite — Actual finite real Hilbert/Borel E including0. Fix actual finite mu and SAME original closable exact compact-C-infinity gradient D BEFORE ALL C1 f with actual MemLp f2mu and MemLp gradientf2mu. Genuine smooth cutoff exhaustion/derivative-product/weighted L2 limits put actual class pair into SAME closure graph, without compact support or extra spatial moment. Finite mu constants are genuinely in original closure domain with outputzero. For actual C1 Gibbs W/exp(-W) integrable, combine actual constants-domain with accepted one-way implication for full zero-output iff AEconstant on SAME D. Actual PBPS common Gaussian J/R/S/Sdensity/positive partitions/sourceC2 alpha beta eta cap and original D_y beforeALL constants/u/directions; real unnormalized y-score C1/L2/boundedgradient from accepted score producer transfers along ONLY explicit reflected density equality S2_y=S_y and enters SAME original closed graph. No R2=R or alternateD equality, global ordinary L1, C-infinity potential, gradient of rough representative, Nontrivial E, spatial moment, supplied domain/fullkernel/spectralgap/Poincare certificate, epsilon0/range/centering/measurablejointselector/core/BL/main/composition. 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.