Samplinglib mathematical lesson

C1 compact functions lie in the same closed gradient graph

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactC1GradientDomain.compact_c1_in_closed_gradient · theorem · Teaching coverage

Read this first

Mathematical statement

For every finite Borel measure mu, every closable partial gradient D whose original graph is exactly compact smooth scalar representatives and their genuine gradients, and every C1 compact scalar f, derive MemLp f 2 mu and MemLp (gradient f) 2 mu and prove the actual pair of their L2 classes lies in D.closure.graph. No graph-membership or approximation certificate is supplied.

\[\psi\in C_c^1(E)\Longrightarrow\psi,\nabla\psi\in L^2(\mu),\quad([\psi],[\nabla\psi])\in\overline{\operatorname{graph}D}=\operatorname{graph}(\overline D).\]

Lean statement · compact_c1_in_closed_gradient

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 compact_c1_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 φ)
    {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
    ∃ hp : MemLp f 2 μ, ∃ hq : MemLp (gradient f) 2 μ,
      (hp.toLp f,hq.toLp (gradient f)) ∈ D.closure.graph

Exact module and namespace context

Proof roadmap

1Construct genuine normalized compact mollifiers
Choose bump radii (n+1)^-1 and twice that value. Normalize the actual smooth compact nonnegative kernel against canonical volume; it has integral one and shrinking support. The approximation is the real convolution g_n=rho_n*f, not a supplied approximating sequence.
2Differentiate the actual convolution
Compact support and C1 regularity justify the right-variable derivative theorem. Actual g_n is compact smooth and its Frechet derivative is convolution with Df. This establishes a joint function/derivative sequence.
3Derive both squared L2 limits from bounded domination
Compact continuous f and its continuous compact derivative have bounded norms C and B. Kernel positivity/mass one bounds each convolution by the same constant. Pointwise mollifier convergence plus the integrable constant (2C)^2 or (2B)^2 under finite mu gives both genuine squared-error integral limits. No uniform-convergence or common-support premise is needed in this finite-measure argument.
4Convert derivative and integral convergence into true L2 topology
The Riesz isometry identifies gradient with the actual Frechet derivative and preserves norms of differences. The L2 inner-product norm formula identifies norm difference with square root of the actual squared-error integral. Both genuine L2 classes converge jointly.
5Use the original graph and its actual closure
Each pair belongs to the original exact compact smooth gradient graph by its representatives. Its joint L2 limit lies in the closed topological graph closure. Actual closability identifies that closure with D.closure.graph; the same operator is preserved.
6Keep the analytic boundary explicit
This derives C1 compact domain membership only. Noncompact constants/linear observables still need true tail cutoffs; local H2 and the generator core/global Bochner are separate. Zero dimension is included without a unit-vector assumption.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with Borel measurable structure and canonical volume, including dimension zero. mu is any finite measure; no absolute-continuity or Gibbs hypothesis on mu is required.
D is the same closable real-linear partial operator, with original graph iff actual C-infinity compact scalar representatives and their genuine gradients, both classes identified mu-a.e. This semantics comes from the existing gradient producer in the paper consumer.
The tested scalar f is only C1 and compactly supported. Its gradient, L2 integrability and actual closure membership are conclusions, not inputs.

Mathematical proof

1. Construct genuine normalized compact mollifiers

Choose bump radii (n+1)^-1 and twice that value. Normalize the actual smooth compact nonnegative kernel against canonical volume; it has integral one and shrinking support. The approximation is the real convolution g_n=rho_n*f, not a supplied approximating sequence.

\[\rho_n\ge0,\quad\int\rho_n dx=1,\quad r_n\to0,\quad g_n=\rho_n*\psi.\]

Corresponding Lean step

compact_c1_in_closed_gradient: phi,hphi; ContDiffBump.normed

2. Differentiate the actual convolution

Compact support and C1 regularity justify the right-variable derivative theorem. Actual g_n is compact smooth and its Frechet derivative is convolution with Df. This establishes a joint function/derivative sequence.

\[Dg_n=\rho_n*D\psi,\quad g_n\in C_c^\infty(E).\]

Corresponding Lean step

mollifier_fderiv; HasCompactSupport.hasFDerivAt_convolution_right

3. Derive both squared L2 limits from bounded domination

Compact continuous f and its continuous compact derivative have bounded norms C and B. Kernel positivity/mass one bounds each convolution by the same constant. Pointwise mollifier convergence plus the integrable constant (2C)^2 or (2B)^2 under finite mu gives both genuine squared-error integral limits. No uniform-convergence or common-support premise is needed in this finite-measure argument.

\[\int|g_n-\psi|^2d\mu\to0,\quad\int\|Dg_n-D\psi\|^2d\mu\to0.\]

Corresponding Lean step

mollifier_squared_error; compact_c1_approximation; tendsto_integral_of_dominated_convergence

4. Convert derivative and integral convergence into true L2 topology

The Riesz isometry identifies gradient with the actual Frechet derivative and preserves norms of differences. The L2 inner-product norm formula identifies norm difference with square root of the actual squared-error integral. Both genuine L2 classes converge jointly.

\[\|[g_n]-[\psi]\|_2\to0,\quad\|[\nabla g_n]-[\nabla\psi]\|_2\to0.\]

Corresponding Lean step

l2_convergence; L2.inner_def; toDual.symm.norm_map

5. Use the original graph and its actual closure

Each pair belongs to the original exact compact smooth gradient graph by its representatives. Its joint L2 limit lies in the closed topological graph closure. Actual closability identifies that closure with D.closure.graph; the same operator is preserved.

\[([g_n],[\nabla g_n])\in\operatorname{graph}D\Longrightarrow([\psi],[\nabla\psi])\in\operatorname{graph}\overline D.\]

Corresponding Lean step

hgraph; Submodule.isClosed_topologicalClosure; IsClosable.graph_closure_eq_closure_graph

6. Keep the analytic boundary explicit

This derives C1 compact domain membership only. Noncompact constants/linear observables still need true tail cutoffs; local H2 and the generator core/global Bochner are separate. Zero dimension is included without a unit-vector assumption.

\[C_c^1\subset\operatorname{dom}\overline D;\quad H^2,\ D^*D\text{ core},\ \mathrm{BL}\text{ remain open}.\]

Corresponding Lean step

compact_c1_in_closed_gradient; Tests.CompactC1GradientDomain

Lean verification

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

Lean proof · compact_c1_in_closed_gradient

Construct genuine normalized compact mollifiers; Differentiate the actual convolution; Derive both squared L2 limits from bounded domination; Convert derivative and integral convergence into true L2 topology; Use the original graph and its actual closure; Keep the analytic boundary explicit

Download module (.lean)

theorem compact_c1_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 φ)
    {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
    ∃ hp : MemLp f 2 μ, ∃ hq : MemLp (gradient f) 2 μ,
      (hp.toLp f,hq.toLp (gradient f)) ∈ D.closure.graph := by
  let φ : ℕ → ContDiffBump (0:E) := fun n =>
    { rIn := ((n:ℝ)+1)⁻¹, rOut := 2*((n:ℝ)+1)⁻¹,
      rIn_pos := by positivity,
      rIn_lt_rOut := by
        have h : 0<((n:ℝ)+1)⁻¹ := by positivity
        linarith }
  have hφ : Tendsto (fun n => (φ n).rOut) atTop (𝓝 0) := by
    have ht : Tendsto (fun n : ℕ => ((n:ℝ)+1)⁻¹) atTop (𝓝 0) :=
      tendsto_inv_atTop_zero.comp
        (tendsto_atTop_add_const_right atTop (1:ℝ) tendsto_natCast_atTop_atTop)
    simpa only [mul_zero] using ht.const_mul 2
  let g := fun n => (φ n).normed volume ⋆[lsmul ℝ ℝ, volume] f
  obtain ⟨hgi,hgf,hgd⟩ := compact_c1_approximation μ hf hc φ hφ
  have gradCont (a : E → ℝ) (ha : ContDiff ℝ 1 a) : Continuous (gradient a) :=
    (toDual ℝ E).symm.continuous.comp (ha.continuous_fderiv one_ne_zero)
  have gradComp (a : E → ℝ) (ha : HasCompactSupport a) : HasCompactSupport (gradient a) := by
    refine HasCompactSupport.of_support_subset_isCompact ha.isCompact ?_
    intro x hx
    by_contra hn
    exact hx (by simp [gradient,fderiv_of_notMem_tsupport ℝ hn])
  have hp := hf.continuous.memLp_of_hasCompactSupport (μ := μ) hc (p := 2)
  have hq := (gradCont f hf).memLp_of_hasCompactSupport (μ := μ) (gradComp f hc) (p := 2)
  have hgp (n) := (hgi n).1.continuous.memLp_of_hasCompactSupport (μ := μ) (hgi n).2 (p := 2)
  have hgq (n) := (gradCont (g n) (contDiff_infty.mp (hgi n).1 1)).memLp_of_hasCompactSupport
    (μ := μ) (gradComp (g n) (hgi n).2) (p := 2)
  have htq : Tendsto (fun n => ∫ x, ‖gradient (g n) x-gradient f x‖^2 ∂μ) atTop (𝓝 0) := by
    convert hgd using 1
    funext n
    apply integral_congr_ae
    filter_upwards [] with x
    simp only [gradient,← map_sub,(toDual ℝ E).symm.norm_map]
    rfl
  have htp := l2_convergence μ g f hgp hp hgf
  have htq' := l2_convergence μ (fun n => gradient (g n)) (gradient f) hgq hq htq
  refine ⟨hp,hq,?_⟩
  rw [← hD.graph_closure_eq_closure_graph]
  apply D.graph.isClosed_topologicalClosure.mem_of_tendsto (htp.prodMk_nhds htq')
  filter_upwards [] with n
  apply D.graph.le_topologicalClosure
  exact (hgraph _ _).mpr ⟨g n,(hgi n).1,(hgi n).2,(hgp n).coeFn_toLp,(hgq n).coeFn_toLp⟩


end
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactC1GradientDomain

Exact module and namespace context

Scope and omitted-condition boundaries

Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasCompactSupport.hasFDerivAt_convolution_right
ContDiffBump.convolution_tendsto_right_of_continuous
tendsto_integral_of_dominated_convergence
L2.inner_def
LinearPMap.IsClosable.graph_closure_eq_closure_graph

Mathematical sources

PBPS Appendix C.1 omitted analytic domain prerequisite — Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected 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.