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
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.
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.
theorem ordinary_energy_le_phaseQuadraticForm {kappa : ℝ} (hkappa : 1 ≤ kappa)
(z : E × E) :
‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 ≤ 6 * phaseQuadraticForm kappa zProof 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.
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.
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.
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‖)]Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Finite Euclidean source domain with the exact M_kappa block form. | Arbitrary real inner-product E, with no finite-dimension or measurability premise. Kappa>=1 for the comparisons; the total definition accepts every real kappa. | generalization | Real inner-product presentation preserves the exact source form. Background comparisons need neither finite dimension nor measurable structure; nonlinear algorithm uses complete finite E and BorelSpace. |
| Universal c and C in the source Proposition4.7 step/contraction. | For every real inner-product E, kappa>=1 and phase point z, the true coordinate energy is bounded by6 times the exact source Q. | source-implicit | Explicit conservative c=1/65536 is proved using the actual C8 algorithm remainder and source drift. Q/API definitions and comparison proofs are unchanged, with no extra completed-paper credit. |
| Actual V_eta from Lemma4.1. | Genuine global C2 f with explicit normalized curvature for the nonlinear consumer. | unresolved | The source smoothing/C2/curvature producer must be joined before claiming Proposition4.7 at V_eta or the full main result. Definitions and energy comparisons are already exact and independent of that producer. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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)
- 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.