Actual constants in original closed-gradient domain
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradient · theorem · Teaching coverage
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.
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.
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=0Proof 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.
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.
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.
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
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.
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.WeightedC1GradientDomainSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Actual reflected fullspace PBPS conditional original-gradient/source score setting. | 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. | generalization | Explicit generic finite-mu C1/constant or C1 Gibbs prerequisite, with real source C2 alpha/beta eta cap/positive reflected law retained at actual consumer. |
| AppC1 density/closedness and noncompact score tests conceal actual graph-domain and constant converse. | 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. | source-implicit | Derive genuine first-order weighted cutoff quotient limits and actual constant-domain/full kernel; real scores transferred only via explicit normalized density equality. |
| Poincare/BL/centered residual/epsilon0/range/core and complete papers/composition. | 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. | unresolved | Only original first-order graph domain/constants/kernel/score membership admitted; no spectralgap/final certificate or joint measurable selector. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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)
- 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.