AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransport

- One actual proxy and coupling simultaneously satisfy eventwise TV, bounded displacement and all positive-time Gaussian RN moment/log bounds.

theorem proxy_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (p r δ : ℝ) (hp : 2 ≤ p) (hr : 0 ≤ r) (hδ : 0 < δ) (hδ1 : δ < 1)
    (hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^p)) P Q ≤ ENNReal.ofReal (r^p)) :
    ∃ Pdag : Measure E, ∃ Γ : Measure (E × E),
      IsProbabilityMeasure Pdag ∧ IsProbabilityMeasure Γ ∧ Transport.IsCoupling Γ Pdag Q ∧
      (∀ B, MeasurableSet B → |P.real B-Pdag.real B| ≤ δ) ∧
      (∀ᵐ z ∂Γ, ‖z.1-z.2‖ ≤ r*δ^(-1/p)) ∧
      ∀ τ : ℝ, 0 < τ → ∀ q : ℝ, 1 < q →
        let H := fun μ : Measure E => GaussianSmoothing.gaussianSmoothing μ (Real.sqrt τ)
        H Pdag ≪ H Q ∧
          (∫⁻ z, ((H Pdag).rnDeriv (H Q) z)^q ∂H Q) ≤
            ENNReal.ofReal (Real.exp (q*(q-1)*r^2/(2*τ*δ^(2/p)))) ∧
          Integrable (fun z => ((H Pdag).rnDeriv (H Q) z).toReal^q) (H Q) ∧
          (∫ z, ((H Pdag).rnDeriv (H Q) z).toReal^q ∂H Q) ≤
            Real.exp (q*(q-1)*r^2/(2*τ*δ^(2/p))) ∧
          Real.log (∫ z, ((H Pdag).rnDeriv (H Q) z).toReal^q ∂H Q)/(q-1) ≤
            q*r^2/(2*τ*δ^(2/p)) := by
  obtain ⟨γ,hγ,hcouple,hopt,hT,hPdag,hΓ,hΓcouple,hdisp,hTV⟩ :=
    Truncation.truncated_proxy P Q p r δ hp hr hδ hδ1 hcost
  let T := fun z : E × E => if ‖z.1-z.2‖ ≤ r*δ^(-1/p) then z.1 else z.2
  refine ⟨γ.map T,γ.map (fun z => (T z,z.2)),hPdag,hΓ,hΓcouple,hTV,hdisp,?_⟩
  intro τ hτ q hq
  let : IsProbabilityMeasure (γ.map T) := hPdag
  have ht : 0 ≤ r*δ^(-1/p) := mul_nonneg hr (Real.rpow_nonneg hδ.le _)
  have h := GaussianMixture.bounded_displacement_reverse_transport
    (γ.map T) Q (γ.map (fun z => (T z,z.2))) hΓcouple τ q (r*δ^(-1/p)) hτ hq ht hdisp
  have he : (r*δ^(-1/p))^2 = r^2 / δ^(2/p) := by
    rw [mul_pow]
    have hd : (δ^(-1/p))^2 = (δ^(2/p))⁻¹ := by
      rw [← Real.rpow_natCast,← Real.rpow_mul hδ.le]
      change δ^((-1/p)*(2 : ℝ)) = (δ^(2/p))⁻¹
      have hex : (-1/p)*(2 : ℝ) = -(2/p) := by ring
      rw [hex,Real.rpow_neg hδ.le]
    rw [hd]
    exact (div_eq_mul_inv _ _).symm
  have hc1 : q*(q-1)*(r*δ^(-1/p))^2/(2*τ) = q*(q-1)*r^2/(2*τ*δ^(2/p)) := by
    rw [he]
    ring
  have hc2 : q*(r*δ^(-1/p))^2/(2*τ) = q*r^2/(2*τ*δ^(2/p)) := by
    rw [he]
    ring
  dsimp only at h ⊢
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ProxyReverseTransport.lean:29published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.