AutoSamplingTheory.SALD.saldPiVelocityNormDependencyContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.PiVelocityNormDependencyContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def saldPiVelocityNormDependencyContract : PiVelocityNormDependencyContract

Construction and field-by-field explanation

Construct a data record from explicit fields and the audited defaults shown below.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldPiVelocityNormSource — audited data reference, not expanded and not a compiled dependency edge

piDefinition : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

appendix.tex:86-94 defines PI by Var_mu(phi) <= C_PI^{-1} * integral ||nabla phi||^2 dmu for all smooth phi.

weightedSobolevSpace : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

appendix.tex:96-106 introduces dot H^1(mu) as the mean-zero weighted Sobolev space with gradient inner product.

meanZeroInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

For psi in dot H^1(mu), the proof uses E_mu[psi]=0 so ||psi||_{L2(mu)}^2=Var_mu[psi].

normEquivalence : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

PI gives ||psi||_{L2(mu)} <= C_PI^{-1/2} ||psi||_{dot H^1(mu)}, and hence equivalence with the weighted H^1 norm on the mean-zero subspace; SALD.piVelocityNormMeanZeroH1UpperScalar records only the resulting real upper-bound algebra.

weakPdeStatement : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

For g in dot H^1(mu), solve div(mu*v)=-g*mu with v=nabla phi through the weak form <phi,psi>_{dot H^1}=int psi*g dmu.

boundedFunctionalStep : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Cauchy-Schwarz plus PI bounds T_mu(psi)=int psi*g dmu by C_PI^{-1/2}||psi||_{dot H^1(mu)}||g||_{L2(mu)}; SALD.piVelocityNormBoundedFunctionalScalar formalizes only this scalar order propagation after the analytic hypotheses are supplied.

rieszRepresentationStep : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Riesz representation on dot H^1(mu) yields phi solving the weak PDE; Lean must provide the Hilbert-space and quotient/mean-zero backend.

velocityBound : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The source conclusion is ||v||_{L2(mu)}=||nabla phi||_{L2(mu)} <= C_PI^{-1/2}||g||_{L2(mu)}.

downstreamComplexityBounds : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. For moving targets, use g=partial_t log pi_t to bound A_0(pi,v).
2. For guided paths, use g_t=partial_t f_t+nabla f_t^T u_t and the centered term g_t-E_{pi_t}[g_t] to bound A_0(pi,w).

dependencies : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. PIContract
2. variance vocabulary
3. weighted Sobolev space
4. SALD.piVelocityNormMeanZeroH1UpperScalar
5. SALD.piVelocityNormBoundedFunctionalScalar
6. Riesz representation theorem

sourceGaps : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. the source does not spell out the Hilbert-space completion and mean-zero quotient details for dot H^1(mu)
2. the cycle 25 lower scalar helpers still require Lean instances of the mean-zero variance identity, L2 pairing/Cauchy-Schwarz bound, nonnegative L2 norms, and the PI square-root norm bound
3. the weak PDE existence step requires boundary/regularity assumptions for div(mu*nabla phi)
4. the displayed proof says v=nabla phi but initially writes psi in the solution ansatz; Lean should normalize this notation before proof search

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def saldPiVelocityNormDependencyContract : PiVelocityNormDependencyContract where
  sourceBlock := saldPiVelocityNormSource
  piDefinition := "appendix.tex:86-94 defines PI by Var_mu(phi) <= C_PI^{-1} * integral ||nabla phi||^2 dmu for all smooth phi."
  weightedSobolevSpace := "appendix.tex:96-106 introduces dot H^1(mu) as the mean-zero weighted Sobolev space with gradient inner product."
  meanZeroInterface := "For psi in dot H^1(mu), the proof uses E_mu[psi]=0 so ||psi||_{L2(mu)}^2=Var_mu[psi]."
  normEquivalence := "PI gives ||psi||_{L2(mu)} <= C_PI^{-1/2} ||psi||_{dot H^1(mu)}, and hence equivalence with the weighted H^1 norm on the mean-zero subspace; SALD.piVelocityNormMeanZeroH1UpperScalar records only the resulting real upper-bound algebra."
  weakPdeStatement := "For g in dot H^1(mu), solve div(mu*v)=-g*mu with v=nabla phi through the weak form <phi,psi>_{dot H^1}=int psi*g dmu."
  boundedFunctionalStep := "Cauchy-Schwarz plus PI bounds T_mu(psi)=int psi*g dmu by C_PI^{-1/2}||psi||_{dot H^1(mu)}||g||_{L2(mu)}; SALD.piVelocityNormBoundedFunctionalScalar formalizes only this scalar order propagation after the analytic hypotheses are supplied."
  rieszRepresentationStep := "Riesz representation on dot H^1(mu) yields phi solving the weak PDE; Lean must provide the Hilbert-space and quotient/mean-zero backend."
  velocityBound := "The source conclusion is ||v||_{L2(mu)}=||nabla phi||_{L2(mu)} <= C_PI^{-1/2}||g||_{L2(mu)}."
  downstreamComplexityBounds := [
    "For moving targets, use g=partial_t log pi_t to bound A_0(pi,v).",
    "For guided paths, use g_t=partial_t f_t+nabla f_t^T u_t and the centered term g_t-E_{pi_t}[g_t] to bound A_0(pi,w)."
  ]
  dependencies := ["PIContract", "variance vocabulary", "weighted Sobolev space", "SALD.piVelocityNormMeanZeroH1UpperScalar", "SALD.piVelocityNormBoundedFunctionalScalar", "Riesz representation theorem"]
  sourceGaps := [
    "the source does not spell out the Hilbert-space completion and mean-zero quotient details for dot H^1(mu)",
    "the cycle 25 lower scalar helpers still require Lean instances of the mean-zero variance identity, L2 pairing/Cauchy-Schwarz bound, nonnegative L2 norms, and the PI square-root norm bound",
    "the weak PDE existence step requires boundary/regularity assumptions for div(mu*nabla phi)",
    "the displayed proof says v=nabla phi but initially writes psi in the solution ansatz; Lean should normalize this notation before proof search"
  ]
  status := ProofStatus.obligation