AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.Truncation

- A finite infimum p-cost budget produces an actual optimal coupling and an explicit truncated proxy within delta in eventwise total variation, coupled to Q at displacement at most r * delta^(-1/p).

theorem truncated_proxy {E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    [SecondCountableTopology 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)) :
    ∃ γ : Measure (E × E), IsProbabilityMeasure γ ∧ Transport.IsCoupling γ P Q ∧
      (∫⁻ z, ENNReal.ofReal (‖z.1-z.2‖ ^ p) ∂γ) =
        Transport.transportCost (fun z => ENNReal.ofReal (‖z.1-z.2‖ ^ p)) P Q ∧
      let t := r * δ ^ (-1 / p)
      let T := fun z : E × E => if ‖z.1-z.2‖ ≤ t then z.1 else z.2
      Measurable T ∧ IsProbabilityMeasure (γ.map T) ∧
        IsProbabilityMeasure (γ.map (fun z => (T z,z.2))) ∧
        Transport.IsCoupling (γ.map (fun z => (T z,z.2))) (γ.map T) Q ∧
        (∀ᵐ z ∂(γ.map (fun z => (T z,z.2))), ‖z.1-z.2‖ ≤ t) ∧
        ∀ B, MeasurableSet B → |P.real B - (γ.map T).real B| ≤ δ := by
  have truncation_coupling
      (γ : Measure (E × E)) [IsProbabilityMeasure γ] (t : ℝ) (ht : 0 ≤ t) :
      let T := fun z : E × E => if ‖z.1-z.2‖ ≤ t then z.1 else z.2
      Measurable T ∧ IsProbabilityMeasure (γ.map T) ∧
        IsProbabilityMeasure (γ.map (fun z => (T z,z.2))) ∧
        Transport.IsCoupling (γ.map (fun z => (T z,z.2))) (γ.map T) γ.snd ∧
        (∀ᵐ z ∂(γ.map (fun z => (T z,z.2))), ‖z.1-z.2‖ ≤ t) ∧
        ∀ B, MeasurableSet B → |γ.fst.real B - (γ.map T).real B| ≤ γ.real {z | t < ‖z.1-z.2‖} := by
    classical
    dsimp only
    let T := fun z : E × E => if ‖z.1-z.2‖ ≤ t then z.1 else z.2
    have hT : Measurable T :=
      Measurable.ite (measurableSet_le (measurable_fst.sub measurable_snd).norm measurable_const)
        measurable_fst measurable_snd
    have hp : Measurable (fun z : E × E => (T z,z.2)) := hT.prodMk measurable_snd
    have hbound (z : E × E) : ‖T z-z.2‖ ≤ t := by
      dsimp only [T]
      split_ifs with hz
      · exact hz
      · simpa using ht
    refine ⟨hT,γ.isProbabilityMeasure_map hT.aemeasurable,
      γ.isProbabilityMeasure_map hp.aemeasurable,?_,?_,?_⟩
    · constructor
      · rw [Measure.fst,Measure.map_map measurable_fst hp]
        rfl
      · rw [Measure.snd,Measure.map_map measurable_snd hp]
        rfl
    · exact (ae_map_iff hp.aemeasurable (measurableSet_le
        (measurable_fst.sub measurable_snd).norm measurable_const)).2 (Filter.Eventually.of_forall hbound)
-- Source excerpt truncated; follow the exact source link.

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

Excerpt truncated; the exact source link is authoritative.