Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

ConditionalResolvent: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Solve the weak equation on the actual conditional gradient closure
ASTIS mathematical exposition

Solve the weak equation on the actual conditional gradient closure

AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent.conditional_weak_resolvent · theorem · Teaching coverage

Statement

For the actual Gibbs-Gaussian augmentation, retain common Markov kernels R,S with swapped-joint disintegration and reflected pushforward. Every S_y is the normalized exp(-W_y) law with W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), C2 potential and finite positive normalizer. Choose one genuine compact-test gradient D_y on scalar/vector L2(S_y), dense and closable with the exact almost-everywhere smooth-gradient graph. For this same D_y, every epsilon>0 and scalar L2 input f has a unique weak solution u in the domain of D_y.closure with the exact energy identity and epsilon^-1 norm and energy bounds.

\[\varepsilon\langle u,v\rangle_{L^2(S_y)}+\langle\overline D_yu,\overline D_yv\rangle_{L^2(S_y;E)}=\langle f,v\rangle_{L^2(S_y)},\quad v\in\operatorname{Dom}\overline D_y.\]

All objects and hypotheses

  • E is finite-dimensional real inner-product Borel, including dimension zero, and V is C2.
  • Explicit 0<alpha<=beta, genuine lower/upper Hessian quadratic-form bounds, eta>0 and beta eta<=1 are inherited from the actual kernel interface. They are not needed by the abstract closed-graph theorem.
  • Mu is the actual normalized tilt by -V. J is the pushforward of independent Gibbs X and standard Gaussian Z under (X,X+sqrt(eta)Z).
  • Common R,S precede every y; each D_y precedes every epsilon and f. The exact graph iff characterizes D_y, not every element of its closure.
  • Integrable exp(-W_y) and its positive normalizer are proved conclusions supplied by the same actual conditional law, not additional paper assumptions. No measurability of y-to-D_y or y-to-solution is asserted.

Mathematical proof

1. Preserve the same conditional probability and gradient

Use conditional_gradient_closable to obtain common R,S and, at each y, the actual normalized potential and one dense closable partial gradient. Retain its exact graph equivalence with smooth compact f and their genuine gradients. The operator is chosen before epsilon and f.

\[\operatorname{Graph}D_y=\{([g],[\nabla g]):g\in C_c^\infty(E)\},\qquad S_y=Z_y^{-1}e^{-W_y}\,du.\]
Corresponding Lean step

hfiber supplies hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph; every one is retained in the result.

2. Use the proved closed extension on the actual fiber

Take A=D_y.closure in the Hilbert spaces of scalar and vector L2(S_y). The parent theorem already proves that this closure has a closed graph. Thus the abstract theorem applies without assuming PI, domain coercivity or a classical differential equation.

\[H=L^2(S_y),\quad K=L^2(S_y;E),\quad A=\overline D_y,\quad\operatorname{Graph}A\ \text{closed}.\]
Corresponding Lean step

Instantiate ClosedGraphResolvent.weak_resolvent with D.closure and hClosed for each positive epsilon and each input f.

3. Retain uniqueness and constants without claiming regularity

The abstract result supplies the exact weak equation over every closed-domain test, energy identity, both explicit bounds and uniqueness on that same domain. This is an L2 domain statement. It does not justify substitution into compact-test Bochner or a pointwise PDE identity.

\[\|u\|_{L^2(S_y)}\le\varepsilon^{-1}\|f\|_{L^2(S_y)},\quad\varepsilon\|u\|^2+\|\overline D_yu\|^2\le\varepsilon^{-1}\|f\|^2.\]
Corresponding Lean step

All clauses are returned directly for the same D and actual S_y; generator core/regularity and the epsilon-to-zero step remain separate obligations.

Lean statement · conditional_weak_resolvent

Actual common conditional kernels, normalized C2 potential, dense closable exact gradient graph, then every positive-epsilon weak solution with exact energy, bounds and uniqueness.

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 conditional_weak_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β:ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β:ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
    let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
      ∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
        ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
        0 < (∫ u, Real.exp (-W y u)) ∧
        ∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
          Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
          (∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
            ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
              u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
          ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
            ∃ u : D.closure.domain,
              (∀ v : D.closure.domain, ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
                ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
              ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 = ⟪f, (u : Lp ℝ 2 (S y))⟫ ∧
              ‖(u : Lp ℝ 2 (S y))‖ ≤ ε⁻¹ * ‖f‖ ∧
              ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
              ∀ w : D.closure.domain,
                (∀ v : D.closure.domain, ε * ⟪(w : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
                  ⟪D.closure w, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) → w = u

Exact module and namespace context

Lean proof · conditional_weak_resolvent

The consumer uses the same parent kernels and operator; its only analytic application is the proved closed-graph weak resolvent.

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 conditional_weak_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β:ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β:ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
    let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
      ∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
        ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
        0 < (∫ u, Real.exp (-W y u)) ∧
        ∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
          Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
          (∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
            ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
              u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
          ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
            ∃ u : D.closure.domain,
              (∀ v : D.closure.domain, ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
                ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
              ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 = ⟪f, (u : Lp ℝ 2 (S y))⟫ ∧
              ‖(u : Lp ℝ 2 (S y))‖ ≤ ε⁻¹ * ‖f‖ ∧
              ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
              ∀ w : D.closure.domain,
                (∀ v : D.closure.domain, ε * ⟪(w : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
                  ⟪D.closure w, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) → w = u := by
  obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
    ConditionalGradient.conditional_gradient_closable hα hαβ hV hH hη hβη
  dsimp only
  refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
  intro y
  obtain ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph⟩ := hfiber y
  refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
  intro ε hε f
  exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent D.closure hClosed ε hε f

end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent

Exact module and namespace context

Scope and omitted-condition boundaries

  • Weak equation on the closed gradient domain only. No classical PDE regularity, identified maximal differential domain, D*D operator core, compact-test Bochner extension, epsilon-uniform estimate, Poincare, noncompact score variance, measurable parameter selection, process/error/cost or full-paper conclusion.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.