Samplinglib mathematical lesson

Actual weighted C1 pair in original gradient closure

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

Read this first

Mathematical statement

Every actual C1 f with genuine weighted scalar and gradient L2 classes has its actual pair (f,gradientf) in SAME original compact-smooth D.closure.graph, with no compact-support premise.

\[f\in C^1(E),\ f,\nabla f\in L^2(\mu)\Longrightarrow([f],[\nabla f])\in\operatorname{graph}\overline D.\]

Lean statement · c1_in_closed_gradient

Every actual C1 f with genuine weighted scalar and gradient L2 classes has its actual pair (f,gradientf) in SAME original compact-smooth D.closure.graph, with no compact-support premise.

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 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)
    (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

1Choose actual smooth expanding compact cutoffs
Fix R_n=n+1 and genuine radialSmoothCutoff chi_n. Positive scales give genuine smoothness/compact support,0≤chi_n≤1 and pointwise chi_n→1, including dimension0. The first derivative bound needs no Nontrivial premise.
2Prove weighted quotient L2 cutoff convergence
Actual MemLp-backed scalar/vector coefficient products converge to their original classes. Dominated square integrals use |chi_n-1|≤1 and actual L2 norm-square/sqrt conversion; representative convergence alone is insufficient.
3Control the genuine product derivative remainder
The actual cutoff gradient tends0 and is uniformly bounded by C because R_n≥1. Genuine weighted dominated convergence of norm(f*gradientchi_n)^2 proves its vector L2 class tends0. Domination is by C^2|f|^2, so no norm(x)*f moment is used.
4Use a genuine C1 product rule
Each chi_n*f is actual C1 compact. Actual differentiability precedes the Frechet product derivative; the Riesz map identifies its genuine gradient as the two factors whose classes have just been controlled.
5Apply the actual compact-C1 producer in the SAME original graph
For each n, accepted joint compact mollification puts the actual function/gradient classes into SAME D.closure.graph. Actual AE quotient extensionality identifies those classes with the cutoff scalar and vector-sum classes. No common support or supplied density/domain certificate is assumed.
6Pass by actual closed graph and product L2 convergence
Closable D has closure graph equal to topological closure of its original graph. Genuine scalar/vector L2 limits and graph closedness admit the actual limiting pair. This is first-order domain membership, not generator-core, rough Hessian, Poincare or BL.

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, actual C1 f, scalar MemLp f2mu and vector MemLp(gradient f)2mu. These are genuine weighted classes; finite probability alone does not make unbounded f L2.

Mathematical proof

1. Choose actual smooth expanding compact cutoffs

Fix R_n=n+1 and genuine radialSmoothCutoff chi_n. Positive scales give genuine smoothness/compact support,0≤chi_n≤1 and pointwise chi_n→1, including dimension0. The first derivative bound needs no Nontrivial premise.

\[R_n=n+1,\quad0\le\chi_n\le1,\quad\chi_n\to1,\quad\|\nabla\chi_n\|\le C/R_n.\]

Corresponding Lean step

radialSmoothCutoff_contDiff; radialSmoothCutoff_hasCompactSupport; radialSmoothCutoff_fderiv_bound

2. Prove weighted quotient L2 cutoff convergence

Actual MemLp-backed scalar/vector coefficient products converge to their original classes. Dominated square integrals use |chi_n-1|≤1 and actual L2 norm-square/sqrt conversion; representative convergence alone is insufficient.

\[[(\chi_n-1)f]\to0,\quad[(\chi_n-1)\nabla f]\to0\quad\text{in }L^2(\mu).\]

Corresponding Lean step

bounded_coefficient_memLp; norm_sq_integral; bounded_coefficient_tendsto_zero; actual_cutoff_function_convergence

3. Control the genuine product derivative remainder

The actual cutoff gradient tends0 and is uniformly bounded by C because R_n≥1. Genuine weighted dominated convergence of norm(f*gradientchi_n)^2 proves its vector L2 class tends0. Domination is by C^2|f|^2, so no norm(x)*f moment is used.

\[\|f\nabla\chi_n\|\le C|f|,\quad[f\nabla\chi_n]\to0\quad L^2(\mu).\]

Corresponding Lean step

dominated_L2_tendsto_zero; radialSmoothCutoff_fderiv_bound; c1_in_closed_gradient

4. Use a genuine C1 product rule

Each chi_n*f is actual C1 compact. Actual differentiability precedes the Frechet product derivative; the Riesz map identifies its genuine gradient as the two factors whose classes have just been controlled.

\[\nabla(\chi_nf)=\chi_n\nabla f+f\nabla\chi_n.\]

Corresponding Lean step

fderiv_fun_mul; toDual; c1_in_closed_gradient

5. Apply the actual compact-C1 producer in the SAME original graph

For each n, accepted joint compact mollification puts the actual function/gradient classes into SAME D.closure.graph. Actual AE quotient extensionality identifies those classes with the cutoff scalar and vector-sum classes. No common support or supplied density/domain certificate is assumed.

\[([\chi_nf],[\chi_n\nabla f+f\nabla\chi_n])\in\operatorname{graph}\overline D.\]

Corresponding Lean step

CompactC1GradientDomain.compact_c1_in_closed_gradient; Lp.ext

6. Pass by actual closed graph and product L2 convergence

Closable D has closure graph equal to topological closure of its original graph. Genuine scalar/vector L2 limits and graph closedness admit the actual limiting pair. This is first-order domain membership, not generator-core, rough Hessian, Poincare or BL.

\[([f],[\nabla f])=\lim_n([\chi_nf],[\nabla(\chi_nf)])\in\operatorname{graph}\overline D.\]

Corresponding Lean step

LinearPMap.IsClosable.graph_closure_eq_closure_graph; IsClosed.mem_of_tendsto; c1_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 · c1_in_closed_gradient

Choose actual smooth expanding compact cutoffs; Prove weighted quotient L2 cutoff convergence; Control the genuine product derivative remainder; Use a genuine C1 product rule; Apply the actual compact-C1 producer in the SAME original graph; Pass by actual closed graph and product L2 convergence

Download module (.lean)

theorem 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)
    (hp : MemLp f 2 μ) (hq : MemLp (gradient f) 2 μ) :
    (hp.toLp f,hq.toLp (gradient f)) ∈ D.closure.graph := by
  classical
  let χ := fun n : ℕ =>
    (AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff
      ((n:ℝ)+1) : E → ℝ)
  have hχ (n : ℕ) : ContDiff ℝ 1 (χ n) :=
    (AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_contDiff
      (by positivity : (0:ℝ)<(n:ℝ)+1)).of_le
        (WithTop.coe_le_coe.mpr (le_top : (1:ℕ∞)≤⊤))
  have hc (n : ℕ) : HasCompactSupport (χ n) :=
    AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_hasCompactSupport
      (by positivity)
  obtain ⟨hfn,hfnt⟩ := actual_cutoff_function_convergence μ f hp
  obtain ⟨hGn,hGnt⟩ := actual_cutoff_function_convergence μ (gradient f) hq
  obtain ⟨C,hC,hCb⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_fderiv_bound
      (E := E)
  have hgrad (n : ℕ) : Continuous (gradient (χ n)) :=
    (toDual ℝ E).symm.continuous.comp ((hχ n).continuous_fderiv one_ne_zero)
  have hgb (n : ℕ) (x : E) : ‖gradient (χ n) x‖ ≤ C/((n:ℝ)+1) := by
    simpa only [gradient, LinearIsometryEquiv.norm_map] using
      hCb ((n:ℝ)+1) (by positivity) x
  have hgradt (x : E) : Tendsto (fun n => gradient (χ n) x) atTop (𝓝 0) := by
    apply tendsto_zero_iff_norm_tendsto_zero.mpr
    apply squeeze_zero (fun n => norm_nonneg _) (fun n => hgb n x)
    simpa only [div_eq_mul_inv,mul_zero,Function.comp_def] using
      (tendsto_inv_atTop_zero.comp
        (tendsto_atTop_add_const_right atTop (1:ℝ) tendsto_natCast_atTop_atTop)).const_mul C
  obtain ⟨hen,hent⟩ := dominated_L2_tendsto_zero μ
    (fun n x => f x • gradient (χ n) x) f
    (fun n => hf.continuous.aestronglyMeasurable.smul (hgrad n).aestronglyMeasurable)
    hp C hC.le (fun n => Eventually.of_forall (fun x => by
      rw [norm_smul]
      have hb : C/((n:ℝ)+1) ≤ C := by
        apply (div_le_iff₀ (by positivity : (0:ℝ)<(n:ℝ)+1)).mpr
        nlinarith [Nat.cast_nonneg (α:=ℝ) n]
      calc ‖f x‖*‖gradient (χ n) x‖ ≤ ‖f x‖*C :=
             mul_le_mul_of_nonneg_left ((hgb n x).trans hb) (norm_nonneg _)
           _ = C*‖f x‖ := mul_comm _ _))
    (Eventually.of_forall (fun x => by
      simpa only [smul_zero] using (hgradt x).const_smul (f x)))
  let hqn := fun n => (hGn n).add (hen n)
  have hqnt : Tendsto (fun n => (hqn n).toLp _) atTop (𝓝 (hq.toLp (gradient f))) := by
    change Tendsto (fun n => (hGn n).toLp _+(hen n).toLp _)
      atTop (𝓝 (hq.toLp (gradient f)))
    simpa only [add_zero] using hGnt.add hent
  have hproduct (n : ℕ) (x : E) :
      gradient (fun z => χ n z*f z) x = χ n x • gradient f x+f x • gradient (χ n) x := by
    rw [gradient, fderiv_fun_mul ((hχ n).differentiable_one x) (hf.differentiable_one x)]
    simp only [map_add,map_smul,gradient]
  have hgn (n : ℕ) : ((hfn n).toLp _,(hqn n).toLp _) ∈ D.closure.graph := by
    obtain ⟨hnp,hnq,hn⟩ :=
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactC1GradientDomain.compact_c1_in_closed_gradient
        μ D hD hgraph ((hχ n).mul hf) (hc n).mul_right
    have hidp : hnp.toLp (fun z => χ n z*f z) = (hfn n).toLp _ := by
      apply Lp.ext
      filter_upwards [hnp.coeFn_toLp,(hfn n).coeFn_toLp] with x hx hy
      rw [hx,hy]; rfl
    have hidq : hnq.toLp (gradient (fun z => χ n z*f z)) = (hqn n).toLp _ := by
      apply Lp.ext
      filter_upwards [hnq.coeFn_toLp,(hqn n).coeFn_toLp] with x hx hy
      rw [hx,hy,hproduct]; rfl
    rwa [hidp,hidq] at hn
  have hclosed : IsClosed (D.closure.graph : Set (Lp ℝ 2 μ × Lp E 2 μ)) := by
    rw [← hD.graph_closure_eq_closure_graph]
    exact D.graph.isClosed_topologicalClosure
  exact hclosed.mem_of_tendsto (hfnt.prodMk_nhds hqnt) (Eventually.of_forall hgn)

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

Mathlib API called (external library)

tendsto_integral_of_dominated_convergence
memLp_two_iff_integrable_sq_norm
L2.inner_def
Lp.ext
fderiv_fun_mul
IsClosed.mem_of_tendsto
LinearPMap.IsClosable.graph_closure_eq_closure_graph

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.