Samplinglib mathematical lesson

For every real inner-product E, kappa>=1 and phase point z, the true coordinate energy is bounded by6 times the exact source Q

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.ordinary_energy_le_phaseQuadraticForm · theorem · Teaching coverage

Read this first

Mathematical statement

For every real inner-product E, kappa≥1 and phase point z, the true coordinate energy is bounded by6 times the exact source Q.

\[\|x\|^2+\|p\|^2\le6Q_\kappa(x,p).\]

Lean statement · ordinary_energy_le_phaseQuadraticForm

For every real inner-product E, kappa>=1 and phase point z, the true coordinate energy is bounded by6 times the exact source Q.

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)

theorem ordinary_energy_le_phaseQuadraticForm {kappa : ℝ} (hkappa : 1 ≤ kappa)
    (z : E × E) :
    ‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 ≤ 6 * phaseQuadraticForm kappa z

Exact module and namespace context

Proof roadmap

1Use the lower cross-term Cauchy bound
inner(x,p)≥-||x||||p||. The coefficient1/(2kappa) is nonnegative; expand6Q-energy and use the square(2||x||-3||p||)². The unchanged existing proof gives the uniform constant6, including zero displacement and dimension.

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.

Mathematical proof

1. Use the lower cross-term Cauchy bound

inner(x,p)≥-||x||||p||. The coefficient1/(2kappa) is nonnegative; expand6Q-energy and use the square(2||x||-3||p||)². The unchanged existing proof gives the uniform constant6, including zero displacement and dimension.

\[\langle x,p\rangle\ge-\|x\|\|p\|,\quad(2\|x\|-3\|p\|)^2\ge0.\]

Corresponding Lean step

abs_real_inner_le_norm; sq_nonneg; nlinarith

Lean verification

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

Lean proof · ordinary_energy_le_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)

theorem ordinary_energy_le_phaseQuadraticForm {kappa : ℝ} (hkappa : 1 ≤ kappa)
    (z : E × E) :
    ‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 ≤ 6 * phaseQuadraticForm kappa z := by
  have hkappa0 : 0 < kappa := lt_of_lt_of_le zero_lt_one hkappa
  have hinner : -(‖z.1‖ * ‖z.2‖) ≤ inner ℝ z.1 z.2 :=
    (abs_le.mp (abs_real_inner_le_norm z.1 z.2)).1
  have hcoef0 : 0 ≤ 1 / (2 * kappa) := by positivity
  rw [phaseQuadraticForm]
  nlinarith [mul_nonneg hcoef0 (sq_nonneg ‖z.1‖),
    sq_nonneg (2 * ‖z.1‖ - 3 * ‖z.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

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseQuadraticForm

Mathlib API called (external library)

abs_real_inner_le_norm
sq_nonneg
mul_nonneg

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.