PhaseMetric: mathematical reading route

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.

def phaseQuadraticForm (kappa : ℝ) (z : E × E) : ℝ :=
  (1 / (2 * kappa) + 1 / 2) * ‖z.1‖ ^ 2 + inner ℝ z.1 z.2 + ‖z.2‖ ^ 2

Exact module and namespace context

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.

def phaseCost (kappa : ℝ) : (E × E) × (E × E) → ℝ≥0∞ :=
  fun z => ENNReal.ofReal (phaseQuadraticForm kappa (z.1 - z.2))

Exact module and namespace context

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.

def phaseWassersteinSq [MeasurableSpace E] (kappa : ℝ)
    (mu nu : Measure (E × E)) : ℝ≥0∞ :=
  Transport.transportCost (phaseCost (E := E) kappa) mu nu

Exact module and namespace context

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‖)]

Exact module and namespace context

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‖]

Exact module and namespace context

Pointwise quadratic comparison, monotone integration, near-optimal coupling, epsilon closure.

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

Exact module and namespace 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.

theorem phase_state_second_moment_of_phaseWasserstein
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (nu reference : Measure (E × E)) (xstar : E) {kappa r Mx Mp : ℝ}
    (hkappa : 1 ≤ kappa)
    (hX : Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2) reference)
    (hP : Integrable (fun z : E × E => ‖z.2‖ ^ 2) reference)
    (hXbound : (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 ∂reference) ≤ Mx)
    (hPbound : (∫ z : E × E, ‖z.2‖ ^ 2 ∂reference) ≤ Mp)
    (hW : phaseWassersteinSq kappa nu reference ≤ ENNReal.ofReal (r ^ 2)) :
    Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2) nu ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2 ∂nu) ≤
        2 * (Mx + Mp) + 24 * r ^ 2 := by
  have hsqrt : Real.sqrt 6 ^ 2 = 6 := Real.sq_sqrt (by norm_num)
  have hordinary : WassersteinSpace.wassersteinDistance nu reference ^ 2 ≤
      ENNReal.ofReal ((Real.sqrt 6 * r) ^ 2) := by
    refine (wassersteinDistance_sq_le_phaseWassersteinSq hkappa nu reference).trans ?_
    calc
      ENNReal.ofReal 6 * phaseWassersteinSq kappa nu reference ≤
          ENNReal.ofReal 6 * ENNReal.ofReal (r ^ 2) := by gcongr
      _ = ENNReal.ofReal ((Real.sqrt 6 * r) ^ 2) := by
        rw [← ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 6)]
        congr 1
        rw [mul_pow, hsqrt]
  have h := PhaseStateMoment.phase_state_second_moment_of_wasserstein
    nu reference xstar hX hP hXbound hPbound hordinary
  refine ⟨h.1, h.2.trans_eq ?_⟩
  rw [mul_pow, hsqrt]
  ring

end

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric

Exact module and namespace context