Actual same-original Gibbs zero-gradient kernel equality
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEquality.closed_gradient_zero_iff_ae_constant · theorem · Teaching coverage
Mathematical statement
For EVERY u in SAME original Gibbs closed-gradient domain, D.closure u=0 IFF its weighted representative is AE ONE real constant. True domain converse is proved from the new constant producer. No spectral-gap/range/Poincare claim.
Lean statement · closed_gradient_zero_iff_ae_constant
For EVERY u in SAME original Gibbs closed-gradient domain, D.closure u=0 IFF its weighted representative is AE ONE real constant. True domain converse is proved from the new constant producer. No spectral-gap/range/Poincare claim.
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 closed_gradient_zero_iff_ae_constant
(W : E → ℝ) (hW : ContDiff ℝ 1 W)
(hI : Integrable (fun x => Real.exp (-W x)))
(D : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)) →ₗ.[ℝ]
Lp E 2 ((volume : Measure E).tilted (fun x => -W x))) (hD : D.IsClosable)
(hgraph : ∀ (a : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
(H : Lp E 2 ((volume : Measure E).tilted (fun x => -W x))), (a,H) ∈ D.graph ↔
∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
a =ᵐ[(volume : Measure E).tilted (fun x => -W x)] φ ∧
H =ᵐ[(volume : Measure E).tilted (fun x => -W x)] gradient φ)
(u : D.closure.domain) :
D.closure u=0 ↔ ∃ c : ℝ, (u : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
=ᵐ[(volume : Measure E).tilted (fun x => -W x)] (fun _ => c)Proof roadmap
- 1Retain the accepted zero-output implies constant direction
Actual C1 Gibbs W/partition integrability and the SAME original closable exact D feed the accepted ordinary weak/mollifier and BOTH AE-transfer producer. No new rough derivative or kernel premise is introduced.
- 2Produce a real constant-domain witness for the reverse direction
Given actual AE constant c, the new finite-measure constant producer gives v in SAME original domain, with v=c AE and output0. Normalized tilted Gibbs is genuinely finite.
- 3Identify actual quotient and domain elements
The two representatives are AE equal, so Lp extensionality and subtype extensionality give u=v. Their actual partial outputs agree. This gives full constant kernel equality only; centered residual/range/Poincare and BL remain separate.
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.
- mu is exactly volume.tilted(-W); W is C1 and exp(-W) is genuinely integrable against canonical full-space volume. Positive normalized density and both AE transfer directions come from the accepted one-way theorem.
- u is in SAME D.closure.domain. Constant-domain converse is produced, not assumed as a final kernel certificate.
Mathematical proof
1. Retain the accepted zero-output implies constant direction
Actual C1 Gibbs W/partition integrability and the SAME original closable exact D feed the accepted ordinary weak/mollifier and BOTH AE-transfer producer. No new rough derivative or kernel premise is introduced.
Corresponding Lean step
GibbsGradientKernel.closed_gradient_zero_ae_constant
2. Produce a real constant-domain witness for the reverse direction
Given actual AE constant c, the new finite-measure constant producer gives v in SAME original domain, with v=c AE and output0. Normalized tilted Gibbs is genuinely finite.
Corresponding Lean step
WeightedC1GradientDomain.constants_in_closed_gradient
3. Identify actual quotient and domain elements
The two representatives are AE equal, so Lp extensionality and subtype extensionality give u=v. Their actual partial outputs agree. This gives full constant kernel equality only; centered residual/range/Poincare and BL remain separate.
Corresponding Lean step
Lp.ext; Subtype.ext; closed_gradient_zero_iff_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_iff_ae_constant
Retain the accepted zero-output implies constant direction; Produce a real constant-domain witness for the reverse direction; Identify actual quotient and domain elements
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 closed_gradient_zero_iff_ae_constant
(W : E → ℝ) (hW : ContDiff ℝ 1 W)
(hI : Integrable (fun x => Real.exp (-W x)))
(D : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)) →ₗ.[ℝ]
Lp E 2 ((volume : Measure E).tilted (fun x => -W x))) (hD : D.IsClosable)
(hgraph : ∀ (a : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
(H : Lp E 2 ((volume : Measure E).tilted (fun x => -W x))), (a,H) ∈ D.graph ↔
∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
a =ᵐ[(volume : Measure E).tilted (fun x => -W x)] φ ∧
H =ᵐ[(volume : Measure E).tilted (fun x => -W x)] gradient φ)
(u : D.closure.domain) :
D.closure u=0 ↔ ∃ c : ℝ, (u : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
=ᵐ[(volume : Measure E).tilted (fun x => -W x)] (fun _ => c) := by
constructor
· exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant
W hW hI D hD hgraph u
· rintro ⟨c,hc⟩
obtain ⟨v,hv,hvz⟩ := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradient _ D hD hgraph c
have he : u=v := Subtype.ext (Lp.ext (hc.trans hv.symm))
rwa [he]
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEqualitySource 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. mu is exactly volume.tilted(-W); W is C1 and exp(-W) is genuinely integrable against canonical full-space volume. Positive normalized density and both AE transfer directions come from the accepted one-way theorem. u is in SAME D.closure.domain. Constant-domain converse is produced, not assumed as a final kernel certificate. | 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 u in SAME original Gibbs closed-gradient domain, D.closure u=0 IFF its weighted representative is AE ONE real constant. True domain converse is proved from the new constant producer. No spectral-gap/range/Poincare claim. | 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
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradientAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant
Mathlib API called (external library)
- Lp.ext
- Subtype.ext
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.