AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL

- Actual ENNReal KL smoothing bound from the genuine quadratic transport budget.

theorem gaussian_kl_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (r τ : ℝ) (_hr : 0 ≤ r) (hτ : 0 < τ)
    (hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) P Q ≤
      ENNReal.ofReal (r^2)) :
    InformationTheory.klDiv (GaussianSmoothing.gaussianSmoothing P (Real.sqrt τ))
      (GaussianSmoothing.gaussianSmoothing Q (Real.sqrt τ)) ≤ ENNReal.ofReal (r^2/(2*τ)) := by
  have crossMoment (γ : Measure (E × E)) [IsProbabilityMeasure γ]
      (h2 : Integrable (fun c : E × E => ‖c.1-c.2‖^2) γ) :
      Integrable (fun z : (E × E) × E => inner ℝ (z.1.1-z.1.2) z.2)
        (γ.prod (stdGaussian E)) ∧
      (∫ z : (E × E) × E, inner ℝ (z.1.1-z.1.2) z.2 ∂γ.prod (stdGaussian E)) = 0 := by
    have hd : Integrable (fun c : E × E => c.1-c.2) γ := by
      apply Integrable.mono' ((integrable_const (1 : ℝ)).add h2) (by fun_prop)
      filter_upwards [] with c
      change ‖c.1-c.2‖ ≤ 1 + ‖c.1-c.2‖^2
      have hn := norm_nonneg (c.1-c.2)
      nlinarith [sq_nonneg (‖c.1-c.2‖-1)]
    have hz : Integrable (fun z : E => z) (stdGaussian E) := IsGaussian.integrable_id
    have hi : Integrable (fun z : (E × E) × E => inner ℝ (z.1.1-z.1.2) z.2)
        (γ.prod (stdGaussian E)) :=
      hd.op_fst_snd (by fun_prop) ⟨1, by intro x y; simpa using abs_real_inner_le_norm x y⟩ hz
    refine ⟨hi, ?_⟩
    rw [integral_prod _ hi]
    have hm (c : E × E) : (∫ z : E, inner ℝ (c.1-c.2) z ∂stdGaussian E) = 0 := by
      change (∫ z : E, (innerSL ℝ (c.1-c.2)) z ∂stdGaussian E) = 0
      rw [(innerSL ℝ (c.1-c.2)).integral_comp_comm hz]
      simp [integral_id_stdGaussian]
    simp_rw [hm]
    simp
  have jointLikelihood (γ : Measure (E × E)) [IsProbabilityMeasure γ]
      (a b : E × E → E) (ha : Measurable a) (hb : Measurable b)
      (τ : ℝ) (hτ : 0 < τ) :
      let A := (γ.prod (stdGaussian E)).map (fun w => (w.1,a w.1+Real.sqrt τ • w.2))
      let B := (γ.prod (stdGaussian E)).map (fun w => (w.1,b w.1+Real.sqrt τ • w.2))
      let L := fun w : (E × E) × E => ENNReal.ofReal (Real.exp
        (inner ℝ (a w.1-b w.1) (w.2-b w.1)/τ-‖a w.1-b w.1‖^2/(2*τ)))
      Measurable L ∧ A = B.withDensity L := by
    dsimp only
    let L := fun w : (E × E) × E => ENNReal.ofReal (Real.exp
      (inner ℝ (a w.1-b w.1) (w.2-b w.1)/τ-‖a w.1-b w.1‖^2/(2*τ)))
    have hL : Measurable L := by unfold L; fun_prop
    refine ⟨hL, ?_⟩
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianKL.lean:28published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.