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
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.
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.
theorem phaseQuadraticForm_le_ordinary_energy {kappa : ℝ} (hkappa : 1 ≤ kappa)
(z : E × E) :
phaseQuadraticForm kappa z ≤ (3 / 2 : ℝ) * (‖z.1‖ ^ 2 + ‖z.2‖ ^ 2)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.
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.
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 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‖]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 exact source Q is bounded by3/2 times the true coordinate energy. | 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)
- 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.