Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

The exact SPHMC M-kappa phase cost

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseCost · def · Teaching coverage

Read this first

Mathematical statement

The cost between two phase points is the nonnegative-real embedding of their M-kappa quadratic displacement.

\[c_\kappa(z,z')=\operatorname{ofReal}\!\left[(\frac1{2\kappa}+\frac12)\|\Delta x\|^2+\langle\Delta x,\Delta p\rangle+\|\Delta p\|^2\right].\]
Lean statement · phaseCost

The definition is total for all real kappa; later comparison theorems assume kappa>=1.

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)
def phaseCost (kappa : ℝ) : (E × E) × (E × E) → ℝ≥0∞

Exact module and namespace context

Proof roadmap

  1. 1Expand the block matrix

    The two off-diagonal one-half blocks combine into one real inner product.

Full assumptions and notation

All objects and hypotheses

  • E is a real inner-product normed additive group.
  • kappa is a real parameter; positivity is imposed by later theorems.

Construction and meaning

1. Expand the block matrix

The two off-diagonal one-half blocks combine into one real inner product.

\[2(\tfrac12)\langle\Delta x,\Delta p\rangle=\langle\Delta x,\Delta p\rangle.\]
Corresponding Lean step

The private real quadratic form is embedded with ENNReal.ofReal.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · phaseCost

Definitional expansion of the paper matrix.

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)
def phaseCost (kappa : ℝ) : (E × E) × (E × E) → ℝ≥0∞ :=
  fun z => ENNReal.ofReal (phaseQuadraticForm kappa (z.1 - z.2))

Exact module and namespace context

Scope and omitted-condition boundaries
  • A pointwise extended-nonnegative cost only; no metric-space instance, contraction or transport estimate is asserted.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • ENNReal.ofReal
    • inner

    Mathematical sources

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