AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianMixture

- An actual bounded-displacement coupling controls the actual Gaussian smoothed RN power moment, its integrability and its normalized logarithm.

theorem bounded_displacement_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (γ : Measure (E × E))
    (hγ : Transport.IsCoupling γ P Q)
    (τ q t : ℝ) (hτ : 0 < τ) (hq : 1 < q) (ht : 0 ≤ t)
    (hdisp : ∀ᵐ c ∂γ, ‖c.1-c.2‖ ≤ t) :
    let H := fun μ : Measure E => GaussianSmoothing.gaussianSmoothing μ (Real.sqrt τ)
    H P ≪ H Q ∧
      (∫⁻ z, ((H P).rnDeriv (H Q) z)^q ∂H Q) ≤ ENNReal.ofReal (Real.exp (q*(q-1)*t^2/(2*τ))) ∧
      Integrable (fun z => ((H P).rnDeriv (H Q) z).toReal^q) (H Q) ∧
      (∫ z, ((H P).rnDeriv (H Q) z).toReal^q ∂H Q) ≤ Real.exp (q*(q-1)*t^2/(2*τ)) ∧
      Real.log (∫ z, ((H P).rnDeriv (H Q) z).toReal^q ∂H Q)/(q-1) ≤ q*t^2/(2*τ) := by
  let gd := fun (τ : ℝ) (a z : E) => ENNReal.ofReal
    (((Real.sqrt (2*Real.pi*τ))⁻¹)^Module.finrank ℝ E * Real.exp (-‖z-a‖^2/(2*τ)))
  have gd_law (a : E) (τ : ℝ) (hτ : 0 < τ) :
      (stdGaussian E).map (fun z => a+Real.sqrt τ • z) =
        (volume : Measure E).withDensity (gd τ a) := by
    have hmap : (stdGaussian E).map (fun z => a + Real.sqrt τ • z) =
        ((stdGaussian E).map (fun z : E => Real.sqrt τ • z)).map (MeasurableEquiv.addLeft a) := by
      rw [Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    rw [hmap,IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity τ hτ,
      RadonNikodym.measurableEquiv_map_withDensity (MeasurableEquiv.addLeft a) _ (by fun_prop)]
    have hvol : (volume : Measure E).map (MeasurableEquiv.addLeft a) = volume :=
      Measure.IsAddLeftInvariant.map_add_left_eq_self a
    rw [hvol]
    congr 1
    funext z
    simp [gd,MeasurableEquiv.addLeft,sub_eq_add_neg,add_comm]
  have mix_density (μ : Measure E) [IsProbabilityMeasure μ] (τ : ℝ) (hτ : 0 < τ) :
      (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt τ • p.2) =
        (volume : Measure E).withDensity (fun z => ∫⁻ a, gd τ a z ∂μ) := by
    have hg : Measurable (fun p : E × E => gd τ p.1 p.2) := by unfold gd; fun_prop
    have hmix : Measurable (fun z => ∫⁻ a, gd τ a z ∂μ) := hg.lintegral_prod_left'
    apply Measure.ext_of_lintegral
    intro f hf
    rw [lintegral_map hf (by fun_prop),lintegral_prod _ (by fun_prop),
      lintegral_withDensity_eq_lintegral_mul _ hmix hf]
    calc
      (∫⁻ a, ∫⁻ z, f (a+Real.sqrt τ • z) ∂stdGaussian E ∂μ) =
          ∫⁻ a, ∫⁻ z, gd τ a z * f z ∂volume ∂μ := by
        apply lintegral_congr
        intro a
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianMixture.lean:26published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.