The paper's exact twisted phase transport cost controls ordinary phase transport and therefore transfers reference position/momentum moments to an incoming law.
Real inner-product phase space.
kappa>=1.
Explicit reference second moments for the final adapter.
Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.
The definition is total for all real kappa; later comparison theorems assume kappa>=1.
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.
The private real quadratic form is embedded with ENNReal.ofReal.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · phaseCost
Definitional expansion of the paper matrix.
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.
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
A pointwise extended-nonnegative cost only; no metric-space instance, contraction or transport estimate is asserted.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
The value is ENNReal and therefore retains infinite costs.
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.
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · phaseWassersteinSq
Definition by the shared Kantorovich API.
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.
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
Raw Kantorovich infimum; optimizer existence is not included.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
M-kappa transport controls ordinary phase transport
The ENNReal conclusion includes infinite-cost laws without a separate branch in the statement.
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.
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 wassersteinDistance_sq_le_phaseWassersteinSq
[MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
{kappa : ℝ} (hkappa : 1 ≤ kappa) (mu nu : Measure (E × E)) :
WassersteinSpace.wassersteinDistance mu nu ^ 2 ≤
ENNReal.ofReal 6 * phaseWassersteinSq kappa mu nu := by
rw [WassersteinSpace.wassersteinDistance_sq]
apply ENNReal.le_of_forall_pos_le_add
intro epsilon hepsilon hfinite
let A : ℝ≥0∞ := ENNReal.ofReal 6
let C : ℝ≥0∞ := phaseWassersteinSq kappa mu nu
have hA0 : A ≠ 0 := by
simp [A]
have hAtop : A ≠ ⊤ := ENNReal.ofReal_ne_top
have hCtop : C < ⊤ := by
rcases ENNReal.mul_lt_top_iff.mp hfinite with h | h | h
· exact h.2
· exact (hA0 h).elim
· simpa [C, h]
let delta : ℝ≥0∞ := (epsilon : ℝ≥0∞) / A
have hdelta0 : delta ≠ 0 := by
have hepsilon0 : (epsilon : ℝ≥0∞) ≠ 0 := by exact_mod_cast hepsilon.ne'
exact (ENNReal.div_pos hepsilon0 hAtop).ne'
have hstrict : C < C + delta :=
ENNReal.lt_add_right hCtop.ne hdelta0
obtain ⟨gamma, hgamma, hgammaCost⟩ :=
Transport.exists_isCoupling_lintegral_lt_of_transportCost_lt
(phaseCost (E := E) kappa) mu nu hstrict
have hphaseMeas : Measurable (phaseCost (E := E) kappa) := by
unfold phaseCost phaseQuadraticForm
fun_prop
calc
Transport.transportCost (WassersteinSpace.quadraticCost (E := E × E)) mu nu ≤
∫⁻ z, WassersteinSpace.quadraticCost (E := E × E) z ∂gamma :=
Transport.transportCost_le_lintegral_of_isCoupling _ mu nu gamma hgamma
_ ≤ ∫⁻ z, A * phaseCost (E := E) kappa z ∂gamma := by
apply lintegral_mono
intro z
exact quadraticCost_le_phaseCost hkappa z
_ = A * ∫⁻ z, phaseCost (E := E) kappa z ∂gamma := by
exact lintegral_const_mul _ hphaseMeas
_ ≤ A * (C + delta) := by
gcongr
_ = A * C + (epsilon : ℝ≥0∞) := by
rw [mul_add, show A * delta = (epsilon : ℝ≥0∞) by
exact ENNReal.mul_div_cancel hA0 hAtop]
_ = ENNReal.ofReal 6 * phaseWassersteinSq kappa mu nu +
(epsilon : ℝ≥0∞) := rfl
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
One-way comparison with explicit kappa-uniform factor 6; no contraction or (D.3).
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
Twisted SPHMC transport gives the phase-state second moment
All reference integrability and moment assumptions remain visible.
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.
Metric comparison followed by the already audited general moment adapter.
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.
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
Consumes a twisted transport bound; does not prove the paper's (D.3), history estimate, D.7 or D.8.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Which proof obligations and prerequisites are covered?
TODO — not closed by these contributions Exact M-kappa point cost
TODO — not closed by these contributions Twisted Kantorovich value
TODO — not closed by these contributions Explicit ordinary/twisted transport comparison
TODO — not closed by these contributions Twisted-transport phase-state moment
TODO — not closed by these contributions Equation (D.3) actual phase history (remaining)
TODO — not closed by these contributions All actual query-center moments (remaining)
TODO — not closed by these contributions Total expected gradient cost (remaining)