Samplinglib mathematical lesson

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

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

Read this first

Mathematical statement

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

\[Q_\kappa(x,p)\le\tfrac32(\|x\|^2+\|p\|^2).\]

Lean statement · phaseQuadraticForm_le_ordinary_energy

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

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 phaseQuadraticForm_le_ordinary_energy {kappa : ℝ} (hkappa : 1 ≤ kappa)
    (z : E × E) :
    phaseQuadraticForm kappa z ≤ (3 / 2 : ℝ) * (‖z.1‖ ^ 2 + ‖z.2‖ ^ 2)

Exact module and namespace context

Proof roadmap

1Use the upper cross-term Cauchy bound
kappa≥1 implies1/(2kappa)+1/2≤1. Bound the cross term by||x||||p||≤(||x||²+||p||²)/2. This is the unchanged existing proof made callable by the actual numerical contraction and later increment consumers.

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 upper cross-term Cauchy bound

kappa≥1 implies1/(2kappa)+1/2≤1. Bound the cross term by||x||||p||≤(||x||²+||p||²)/2. This is the unchanged existing proof made callable by the actual numerical contraction and later increment consumers.

\[\langle x,p\rangle\le\tfrac12(\|x\|^2+\|p\|^2),\quad\tfrac1{2\kappa}+\tfrac12\le1.\]

Corresponding Lean step

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 · phaseQuadraticForm_le_ordinary_energy

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 phaseQuadraticForm_le_ordinary_energy {kappa : ℝ} (hkappa : 1 ≤ kappa)
    (z : E × E) :
    phaseQuadraticForm kappa z ≤ (3 / 2 : ℝ) * (‖z.1‖ ^ 2 + ‖z.2‖ ^ 2) := by
  have hkappa0 : 0 < kappa := lt_of_lt_of_le zero_lt_one hkappa
  have hinv : 1 / kappa ≤ 1 := (div_le_one hkappa0).2 hkappa
  have hhalf : (1 / kappa) * (1 / 2 : ℝ) ≤ 1 / 2 := by
    simpa using mul_le_mul_of_nonneg_right hinv (by norm_num : (0 : ℝ) ≤ 1 / 2)
  have hcoef : 1 / (2 * kappa) + 1 / 2 ≤ (1 : ℝ) := by
    rw [one_div, mul_inv_rev, show (2 : ℝ)⁻¹ = 1 / 2 by norm_num]
    convert add_le_add_right hhalf (1 / 2) using 1 <;> norm_num <;> ring
  have hinner : inner ℝ z.1 z.2 ≤ ‖z.1‖ * ‖z.2‖ :=
    real_inner_le_norm z.1 z.2
  have hsquare : 2 * (‖z.1‖ * ‖z.2‖) ≤ ‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 := by
    nlinarith [sq_nonneg (‖z.1‖ - ‖z.2‖)]
  rw [phaseQuadraticForm]
  nlinarith [mul_nonneg (sub_nonneg.mpr hcoef) (sq_nonneg ‖z.1‖),
    sq_nonneg ‖z.1‖, sq_nonneg ‖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)

real_inner_le_norm
sq_nonneg
div_le_one

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.