SPHMC Wasserstein-to-phase-state second moment

Approximate coupling, pointwise quadratic domination, marginal pushforward identities, then an epsilon closure argument.

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 of_wassersteinDistance_sq_le {mu nu : Measure E}
    {g : E → F} {b : ℝ≥0} {r : ℝ} (hg : LipschitzWith b g)
    (hi : Integrable (fun x => ‖g x‖ ^ 2) nu)
    (hw : WassersteinSpace.wassersteinDistance mu nu ^ 2 ≤ ENNReal.ofReal (r ^ 2)) :
    Integrable (fun x => ‖g x‖ ^ 2) mu ∧
      (∫ x, ‖g x‖ ^ 2 ∂mu) ≤
        2 * (∫ x, ‖g x‖ ^ 2 ∂nu) + 2 * (b : ℝ) ^ 2 * r ^ 2 := by
  have hall (s : ℝ) (hs : r ^ 2 < s) :
      Integrable (fun x => ‖g x‖ ^ 2) mu ∧
        (∫ x, ‖g x‖ ^ 2 ∂mu) ≤
          2 * (∫ x, ‖g x‖ ^ 2 ∂nu) + 2 * (b : ℝ) ^ 2 * s := by
    have hs0 : 0 < s := (sq_nonneg r).trans_lt hs
    have hcost : Transport.transportCost
        (WassersteinSpace.quadraticCost (E := E)) mu nu < ENNReal.ofReal s := by
      rw [← WassersteinSpace.wassersteinDistance_sq]
      exact hw.trans_lt ((ENNReal.ofReal_lt_ofReal_iff hs0).2 hs)
    obtain ⟨gamma, hgamma, hgammaCost⟩ :=
      Transport.exists_isCoupling_lintegral_lt_of_transportCost_lt
        (WassersteinSpace.quadraticCost (E := E)) mu nu hcost
    exact of_isCoupling hg hi hgamma hs0.le hgammaCost.le
  refine ⟨(hall (r ^ 2 + 1) (by linarith)).1, ?_⟩
  apply le_of_forall_pos_le_add
  intro epsilon hepsilon
  have hden : 0 < 2 * (b : ℝ) ^ 2 + 1 := by positivity
  have hdelta : 0 < epsilon / (2 * (b : ℝ) ^ 2 + 1) := div_pos hepsilon hden
  have hbound := (hall (r ^ 2 + epsilon / (2 * (b : ℝ) ^ 2 + 1)) (by linarith)).2
  have heq := div_mul_cancel₀ epsilon hden.ne'
  nlinarith

end

end AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinLipschitzMoment

Exact module and namespace context

Instantiate the shared observable theorem with the two phase projections and add the resulting integrable moments.

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_wasserstein
    (nu reference : Measure (E × E)) (xstar : E) {r Mx Mp : ℝ}
    (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 : WassersteinSpace.wassersteinDistance nu reference ^ 2 ≤
      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) + 4 * r ^ 2 := by
  have hXlip : LipschitzWith 1 (fun z : E × E => z.1 - xstar) := by
    refine LipschitzWith.of_dist_le_mul ?_
    intro a b
    rw [NNReal.coe_one, one_mul, Prod.dist_eq]
    simpa only [dist_eq_norm, sub_sub_sub_cancel_right] using
      (le_max_left (dist a.1 b.1) (dist a.2 b.2))
  have hPlip : LipschitzWith 1 (fun z : E × E => z.2) :=
    LipschitzWith.prod_snd
  have hXt := WassersteinLipschitzMoment.of_wassersteinDistance_sq_le hXlip hX hW
  have hPt := WassersteinLipschitzMoment.of_wassersteinDistance_sq_le hPlip hP hW
  refine ⟨hXt.1.add hPt.1, ?_⟩
  rw [integral_add hXt.1 hPt.1]
  norm_num at hXt hPt
  linarith

end

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseStateMoment

Exact module and namespace context