Samplinglib mathematical lesson

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa

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

Read this first

Mathematical statement

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa≥1 by the compiled comparisons.

\[Q_\kappa(x,p)=\left(\frac1{2\kappa}+\frac12\right)\|x\|^2+\langle x,p\rangle+\|p\|^2.\]

Lean statement · phaseQuadraticForm

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa>=1 by the compiled comparisons.

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 phaseQuadraticForm (kappa : ℝ) (z : E × E) : ℝ

Exact module and namespace context

Proof roadmap

1Evaluate the source block matrix
Both off-diagonal entries are1/2, so their sum is the cross inner product. This reuses the existing definition unchanged; public visibility enables the actual numerical contraction consumer.

Full assumptions and notation

All objects and hypotheses

Arbitrary real inner-product E, with no finite-dimension or measurability premise. Kappa≥1 for the comparisons; the total definition accepts every real kappa.

Construction and meaning

1. Evaluate the source block matrix

Both off-diagonal entries are1/2, so their sum is the cross inner product. This reuses the existing definition unchanged; public visibility enables the actual numerical contraction consumer.

\[\tfrac12\langle x,p\rangle+\tfrac12\langle p,x\rangle=\langle x,p\rangle.\]

Corresponding Lean step

phaseQuadraticForm

Lean verification

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

Lean construction · phaseQuadraticForm

Exact source form and compiled parent composition, with all source domains/constant absorption and zero cases explicit. Existing Q/comparison proofs unchanged.

Download module (.lean)

def phaseQuadraticForm (kappa : ℝ) (z : E × E) : ℝ :=
  (1 / (2 * kappa) + 1 / 2) * ‖z.1‖ ^ 2 + inner ℝ z.1 z.2 + ‖z.2‖ ^ 2

Exact module and namespace context

Scope and omitted-condition boundaries

Existing source Q/API promotion with unchanged proof, no separate mathematical progress credit. Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

SPHMC actual numerical contraction and M_kappa — Existing source Q/API promotion with unchanged proof, no separate mathematical progress credit. Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected 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.